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₁[ Nat] means $1 * z = $1 * e;
A2: S₁[ 0 ] by COMPLFLD:7, BINOM:12;
A3: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A4: S₁[i] ; :: thesis: S₁[i + 1]
(i + 1) * e = e + (i * e) by BINOM:def 3
.= z + (i * z) by A1, A4 ;
hence S₁[i + 1] ; :: thesis: verum

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A2, A3);
hence n * z = n * e ; :: thesis: verum