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

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

let n be 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:6
.= (((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:75
.= (cos ((n + 1) * x)) + ((sin ((n + 1) * x)) * <i>) by SIN_COS:75 ;
hence S₁[n + 1] ; :: thesis: verum

end;

A2: S₁[ 0 ] by NEWTON:4, SIN_COS:31;
thus for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A1); :: thesis: verum