∀ n f, permut f n ⇒ bijn f n

Theorem permut_to_bijn : forall (n:nat.nat), forall (f:(nat.nat -> nat.nat)), (permut f n) -> bijn f n.

theorem permut_to_bijn : \forall (n:nat). \forall (f:nat -> nat). ((permut) f n) -> (bijn) f n.

theorem permut_to_bijn : forall (n:nat.nat) , forall (f:(nat.nat) -> nat.nat) , ((((permutation.permut) ) (f)) (n)) -> (((permutation.bijn) ) (f)) (n).

permut_to_bijn : LEMMA (FORALL(n:nat_sttfa_th.sttfa_nat):(FORALL(f:[nat_sttfa_th.sttfa_nat -> nat_sttfa_th.sttfa_nat]):(permutation_sttfa.permut(f)(n) => permutation_sttfa.bijn(f)(n))))

Printing for OpenTheory is not working at the moment.