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_{1}[ Nat] means (power F_Complex) . (x,$1) is Integer;

_{1}[ 0 ]
by COMPLFLD:8, GROUP_1:def 7;

for k being Nat holds S_{1}[k]
from NAT_1:sch 2(A3, A2);

hence (power F_Complex) . (x,n) is Integer ; :: thesis: verum

(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

A2: now :: thesis: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]

A3:
SS

reconsider i1 = x as Integer by A1;

let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

reconsider kk = k as Element of NAT by ORDINAL1:def 12;

assume S_{1}[k]
; :: thesis: S_{1}[k + 1]

then reconsider i2 = (power F_Complex) . (x,k) as Integer ;

((power F_Complex) . (x,kk)) * x = i1 * i2 ;

hence S_{1}[k + 1]
by GROUP_1:def 7; :: thesis: verum

end;let k be Nat; :: thesis: ( S

reconsider kk = k as Element of NAT by ORDINAL1:def 12;

assume S

then reconsider i2 = (power F_Complex) . (x,k) as Integer ;

((power F_Complex) . (x,kk)) * x = i1 * i2 ;

hence S

for k being Nat holds S

hence (power F_Complex) . (x,n) is Integer ; :: thesis: verum