defpred S₁[ Nat] means (power F_Complex) . (r,r) is real ;
(power F_Complex) . (r,0) = 1_ F_Complex by GROUP_1:def 7;
then A1: S₁[ 0 ] by COMPLFLD:8, COMPLEX1:6;
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
(power F_Complex) . (r,(k + 1)) = ((power F_Complex) . (r,k)) * r by GROUP_1:def 7;
hence ( S₁[k] implies S₁[k + 1] ) ; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A2);
hence (power F_Complex) . (r,n) is real ; :: thesis: verum