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₁[ Element of NAT ] means (power F_Complex) . (x,$1) is Integer;

A2: now

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

end;

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