let n be Element of NAT ; :: thesis: ( 0 !c = 1 & n !c <> 0 & (n + 1) !c = (n !c ) * (n + 1) )
defpred S₁[ Element of NAT ] means $1 !c <> 0 ;
thus 0 !c = 1 by Def4; :: thesis: ( n !c <> 0 & (n + 1) !c = (n !c ) * (n + 1) )
A1: S₁[ 0 ] by Def4;

A2: now

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: S₁[n] ; :: thesis: S₁[n + 1]
(n + 1) !c = (n !c ) * ((n + 1) + (0 * <i> )) by Def4;
hence S₁[n + 1] by A3; :: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A1, A2);
hence n !c <> 0 ; :: thesis: (n + 1) !c = (n !c ) * (n + 1)
thus (n + 1) !c = (n !c ) * (n + 1) by Def4; :: thesis: verum