∀ f g n, bijn f n ⇒ bijn g n ⇒ bijn (λp. f (g p)) n

Theorem bijn_fg : forall (f:(nat.nat -> nat.nat)), forall (g:(nat.nat -> nat.nat)), forall (n:nat.nat), (bijn f n) -> (bijn g n) -> bijn (fun (p:nat.nat) => f (g p)) n.

theorem bijn_fg : \forall (f:nat -> nat). \forall (g:nat -> nat). \forall (n:nat). ((bijn) f n) -> ((bijn) g n) -> (bijn) (\lambda p : nat. f (g p)) n.

theorem bijn_fg : forall (f:(nat.nat) -> nat.nat) , forall (g:(nat.nat) -> nat.nat) , forall (n:nat.nat) , ((((permutation.bijn) ) (f)) (n)) -> ((((permutation.bijn) ) (g)) (n)) -> (((permutation.bijn) ) (fun (p : nat.nat) , (f) ((g) (p)))) (n).

bijn_fg : 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):(permutation_sttfa.bijn(f)(n) => (permutation_sttfa.bijn(g)(n) => permutation_sttfa.bijn((LAMBDA(p:nat_sttfa_th.sttfa_nat):f(g(p))))(n))))))

Printing for OpenTheory is not working at the moment.