let n be Nat; :: thesis: for z being Complex

for e being Element of F_Complex st z = e holds

n * z = n * e

let z be Complex; :: thesis: for e being Element of F_Complex st z = e holds

n * z = n * e

let e be Element of F_Complex; :: thesis: ( z = e implies n * z = n * e )

assume A1: z = e ; :: thesis: n * z = n * e

defpred S_{1}[ Nat] means $1 * z = $1 * e;

A2: S_{1}[ 0 ]
by COMPLFLD:7, BINOM:12;

A3: for i being Nat st S_{1}[i] holds

S_{1}[i + 1]
_{1}[i]
from NAT_1:sch 2(A2, A3);

hence n * z = n * e ; :: thesis: verum

for e being Element of F_Complex st z = e holds

n * z = n * e

let z be Complex; :: thesis: for e being Element of F_Complex st z = e holds

n * z = n * e

let e be Element of F_Complex; :: thesis: ( z = e implies n * z = n * e )

assume A1: z = e ; :: thesis: n * z = n * e

defpred S

A2: S

A3: for i being Nat st S

S

proof

for i being Nat holds S
let i be Nat; :: thesis: ( S_{1}[i] implies S_{1}[i + 1] )

assume A4: S_{1}[i]
; :: thesis: S_{1}[i + 1]

(i + 1) * e = e + (i * e) by BINOM:def 3

.= z + (i * z) by A1, A4 ;

hence S_{1}[i + 1]
; :: thesis: verum

end;assume A4: S

(i + 1) * e = e + (i * e) by BINOM:def 3

.= z + (i * z) by A1, A4 ;

hence S

hence n * z = n * e ; :: thesis: verum