∀ n, (!n) = (bigop ((n+1) - 1 ) (λi. true) 1 times (λi. i + 1 ))

Theorem eq_fact_pi_p : forall (n:nat.nat), logic.eq (nat.nat) (fact.fact n) (bigops.bigop (nat.nat) (nat.minus (nat.S n) (nat.S nat.O)) (fun (i:nat.nat) => bool.true) (nat.S nat.O) nat.times (fun (i:nat.nat) => nat.plus i (nat.S nat.O))).

theorem eq_fact_pi_p : \forall (n:nat). (eq) (nat) ((fact) n) ((bigop) (nat) ((minus) ((S) n) ((S) (O) )) (\lambda i : nat. (true) ) ((S) (O) ) (times) (\lambda i : nat. (plus) i ((S) (O) ))).

theorem eq_fact_pi_p : forall (n:nat.nat) , (((logic.eq_) (nat.nat)) (((fact.fact) ) (n))) (((((((bigops.bigop) (nat.nat)) ((((nat.minus) ) (((nat.S) ) (n))) (((nat.S) ) ((nat.O) )))) (fun (i : nat.nat) , (bool.true) )) (((nat.S) ) ((nat.O) ))) ((nat.times) )) (fun (i : nat.nat) , (((nat.plus) ) (i)) (((nat.S) ) ((nat.O) )))).

eq_fact_pi_p : LEMMA (FORALL(n:nat_sttfa_th.sttfa_nat):logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](fact_sttfa_th.sttfa_fact(n))(bigops_sttfa_th.bigop[nat_sttfa_th.sttfa_nat](nat_sttfa_th.minus(nat_sttfa_th.sttfa_S(n))(nat_sttfa_th.sttfa_S(nat_sttfa_th.sttfa_O)))((LAMBDA(i:nat_sttfa_th.sttfa_nat):bool_sttfa_th.sttfa_true))(nat_sttfa_th.sttfa_S(nat_sttfa_th.sttfa_O))(nat_sttfa_th.times)((LAMBDA(i:nat_sttfa_th.sttfa_nat):nat_sttfa_th.plus(i)(nat_sttfa_th.sttfa_S(nat_sttfa_th.sttfa_O))))))

Printing for OpenTheory is not working at the moment.