A1: 0. F_Complex = 0 by COMPLFLD:def 1;
defpred S₁[ Nat] means $1 '*' (1_ F_Complex) = $1;
A2: S₁[ 0 ] by A1, RING_3:59;
A3: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A4: S₁[n] ; :: thesis: S₁[n + 1]
thus (n + 1) '*' (1_ F_Complex) = (n '*' (1_ F_Complex)) + (1 '*' (1_ F_Complex)) by RING_3:62
.= n + 1 by A4, COMPLEX1:def 4, COMPLFLD:8, RING_3:60 ; :: thesis: verum

end;

A5: for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A3);
let i be Integer; :: thesis: i '*' (1_ F_Complex) = i
consider k being Nat such that
A6: ( i = k or i = - k ) by INT_1:2;

per cases ( i = k or i = - k ) by A6;

suppose i = k ; :: thesis: i '*' (1_ F_Complex) = i

hence i '*' (1_ F_Complex) = i by A5; :: thesis: verum

end;

suppose A7: i = - k ; :: thesis: i '*' (1_ F_Complex) = i

hence i '*' (1_ F_Complex) = - (k '*' (1_ F_Complex)) by RING_3:63
.= i by A7, A5, COMPLFLD:2 ;
:: thesis: verum

end;

end;