let s be natural Number ; :: thesis: s ! is Element of NAT
A0: s is Nat by TARSKI:1;
defpred S₁[ Nat] means $1 ! is Element of NAT ;

A1: now :: thesis: for s being Nat st S₁[s] holds
S₁[s + 1]

let s be Nat; :: thesis: ( S₁[s] implies S₁[s + 1] )
assume S₁[s] ; :: thesis: S₁[s + 1]
then reconsider k = s ! as Element of NAT ;
(s + 1) ! = (s + 1) * k by Th15;
hence S₁[s + 1] ; :: thesis: verum

end;

A2: S₁[ 0 ] by RVSUM_1:94;
for s being Nat holds S₁[s] from NAT_1:sch 2(A2, A1);
hence s ! is Element of NAT by A0; :: thesis: verum