let s be natural Number ; :: thesis: (s + 1) ! = (s !) * (s + 1)
idseq (s + 1) = (idseq s) ^ <*(s + 1)*> by FINSEQ_2:51;
hence (s + 1) ! = (s !) * (s + 1) by RVSUM_1:96; :: thesis: verum