let n be Element of NAT ; :: thesis: for x being Element of F_Complex st x is Integer holds
(power F_Complex) . (x,n) is Integer
let x be Element of F_Complex; :: thesis: ( x is Integer implies (power F_Complex) . (x,n) is Integer )
assume A1: x is Integer ; :: thesis: (power F_Complex) . (x,n) is Integer
defpred S₁[ Nat] means (power F_Complex) . (x,$1) is Integer;

A2: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

reconsider i1 = x as Integer by A1;
let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
reconsider kk = k as Element of NAT by ORDINAL1:def 12;
assume S₁[k] ; :: thesis: S₁[k + 1]
then reconsider i2 = (power F_Complex) . (x,k) as Integer ;
((power F_Complex) . (x,kk)) * x = i1 * i2 ;
hence S₁[k + 1] by GROUP_1:def 7; :: thesis: verum

end;

A3: S₁[ 0 ] by COMPLFLD:8, GROUP_1:def 7;
for k being Nat holds S₁[k] from NAT_1:sch 2(A3, A2);
hence (power F_Complex) . (x,n) is Integer ; :: thesis: verum