let s, t be Nat; :: thesis: ex r being Nat st (1 + s) |^ t = ((1 + (t * s)) + ((t choose 2) * (s ^2))) + (r * (s ^3))
defpred S₁[ Nat] means ex r being Nat st (1 + s) |^ $1 = ((1 + ($1 * s)) + (($1 choose 2) * (s ^2))) + (r * (s ^3));
A1: for t being Nat st S₁[t] holds
S₁[t + 1]

proof

let t be Nat; :: thesis: ( S₁[t] implies S₁[t + 1] )
assume S₁[t] ; :: thesis: S₁[t + 1]
then consider r1 being Nat such that
A2: (1 + s) |^ t = ((1 + (t * s)) + ((t choose 2) * (s ^2))) + (r1 * (s ^3)) ;
(1 + s) |^ (t + 1) = (((1 + (t * s)) + ((t choose 2) * (s ^2))) + (r1 * (s ^3))) * (1 + s) by A2, NEWTON:6
.= ((((1 + ((t + 1) * s)) + ((t + (t choose 2)) * (s ^2))) + (r1 * (s ^3))) + (((t choose 2) * (s ^2)) * s)) + ((r1 * (s ^3)) * s)
.= ((((1 + ((t + 1) * s)) + ((t + ((t * (t - 1)) / 2)) * (s ^2))) + (r1 * (s ^3))) + (((t choose 2) * (s ^2)) * s)) + ((r1 * (s ^3)) * s) by STIRL2_1:51
.= ((((1 + ((t + 1) * s)) + ((((t + 1) * ((t + 1) - 1)) / 2) * (s ^2))) + (r1 * (s ^3))) + (((t choose 2) * (s ^2)) * s)) + ((r1 * (s ^3)) * s)
.= ((((1 + ((t + 1) * s)) + (((t + 1) choose 2) * (s ^2))) + (r1 * (s ^3))) + ((t choose 2) * (s ^3))) + ((r1 * (s ^3)) * s) by STIRL2_1:51
.= ((1 + ((t + 1) * s)) + (((t + 1) choose 2) * (s ^2))) + (((r1 + (t choose 2)) + (r1 * s)) * (s ^3)) ;
hence S₁[t + 1] ; :: thesis: verum

end;

A3: S₁[ 0 ]

proof

reconsider z = 0 as Element of NAT ;
take r = 0 ; :: thesis: (1 + s) |^ 0 = ((1 + (0 * s)) + ((0 choose 2) * (s ^2))) + (r * (s ^3))
((1 + (z * s)) + ((z choose 2) * (s ^2))) + (r * (s ^3)) = ((1 + (z * s)) + (z * (s ^2))) + (r * (s ^3)) by NEWTON:def 3
.= (1 + s) |^ z by NEWTON:4 ;
hence (1 + s) |^ 0 = ((1 + (0 * s)) + ((0 choose 2) * (s ^2))) + (r * (s ^3)) ; :: thesis: verum

end;

for t being Nat holds S₁[t] from NAT_1:sch 2(A3, A1);
hence ex r being Nat st (1 + s) |^ t = ((1 + (t * s)) + ((t choose 2) * (s ^2))) + (r * (s ^3)) ; :: thesis: verum