∀ f g n, ∀ i, i ≤ n ⇒ (f i) = (g i) ⇒ bijn f n ⇒ bijn g n

Theorem eq_to_bijn : forall (f:(nat.nat -> nat.nat)), forall (g:(nat.nat -> nat.nat)), forall (n:nat.nat), (forall (i:nat.nat), (nat.le i n) -> logic.eq (nat.nat) (f i) (g i)) -> (bijn f n) -> bijn g n.

theorem eq_to_bijn : \forall (f:nat -> nat). \forall (g:nat -> nat). \forall (n:nat). (\forall (i:nat). ((le) i n) -> (eq) (nat) (f i) (g i)) -> ((bijn) f n) -> (bijn) g n.

theorem eq_to_bijn : forall (f:(nat.nat) -> nat.nat) , forall (g:(nat.nat) -> nat.nat) , forall (n:nat.nat) , (forall (i:nat.nat) , ((((nat.le_) ) (i)) (n)) -> (((logic.eq_) (nat.nat)) ((f) (i))) ((g) (i))) -> ((((permutation.bijn) ) (f)) (n)) -> (((permutation.bijn) ) (g)) (n).

eq_to_bijn : LEMMA (FORALL(f:[nat_sttfa_th.sttfa_nat -> nat_sttfa_th.sttfa_nat]):(FORALL(g:[nat_sttfa_th.sttfa_nat -> nat_sttfa_th.sttfa_nat]):(FORALL(n:nat_sttfa_th.sttfa_nat):((FORALL(i:nat_sttfa_th.sttfa_nat):(nat_sttfa_th.le(i)(n) => logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](f(i))(g(i)))) => (permutation_sttfa.bijn(f)(n) => permutation_sttfa.bijn(g)(n))))))

Printing for OpenTheory is not working at the moment.