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 S1[ Nat] means $1 * z = $1 * e;
A2: S1[ 0 ] by COMPLFLD:7, BINOM:12;
A3: for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be Nat; :: thesis: ( S1[i] implies S1[i + 1] )
assume A4: S1[i] ; :: thesis: S1[i + 1]
(i + 1) * e = e + (i * e) by BINOM:def 3
.= z + (i * z) by A1, A4 ;
hence S1[i + 1] ; :: thesis: verum
end;
for i being Nat holds S1[i] from NAT_1:sch 2(A2, A3);
 hence n * z = n * e ; :: thesis: verum