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]
A4: (n + 1) !c = (n !c ) * ((n + 1) + (0 * <i> )) by Def4;
thus S₁[n + 1] by A3, A4; :: thesis: verum

end;

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