let x be real number ; :: thesis: for n being Element of NAT holds ((cos x) + ((sin x) * <i> )) |^ n = (cos (n * x)) + ((sin (n * x)) * <i> )
defpred S₁[ Element of NAT ] means ((cos x) + ((sin x) * <i> )) |^ $1 = (cos ($1 * x)) + ((sin ($1 * x)) * <i> );

A1: now

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume S₁[n] ; :: thesis: S₁[n + 1]
then ((cos x) + ((sin x) * <i> )) |^ (n + 1) = ((cos (n * x)) + ((sin (n * x)) * <i> )) * ((cos x) + ((sin x) * <i> )) by NEWTON:11
.= (((cos (n * x)) * (cos x)) - ((sin (n * x)) * (sin x))) + ((((cos (n * x)) * (sin x)) + ((cos x) * (sin (n * x)))) * <i> )
.= (cos ((n * x) + x)) + ((((cos (n * x)) * (sin x)) + ((cos x) * (sin (n * x)))) * <i> ) by SIN_COS:80
.= (cos ((n + 1) * x)) + ((sin ((n + 1) * x)) * <i> ) by SIN_COS:80 ;
hence S₁[n + 1] ; :: thesis: verum

end;

A2: S₁[ 0 ] by NEWTON:9, SIN_COS:34;
thus for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A2, A1); :: thesis: verum