let s be Nat; :: thesis: (s + 1) ! = (s ! ) * (s + 1)
set r1 = s + 1;
(s + 1) ! = (s ! ) * (s + 1)

proof

idseq (s + 1) = (idseq s) ^ <*(s + 1)*> by FINSEQ_2:60;
hence (s + 1) ! = (s ! ) * (s + 1) by RVSUM_1:126; :: thesis: verum

end;

hence (s + 1) ! = (s ! ) * (s + 1) ; :: thesis: verum