set mc = multcomplex ;
consider f being FinSequence of COMPLEX such that
A1: f = F and
A2: Product F = multcomplex $$ f by Def13;
set g = [#] (f,(the_unity_wrt multcomplex));
defpred S₁[ Nat] means multcomplex $$ ((finSeg F),([#] (f,(the_unity_wrt multcomplex)))) is real ;
A3: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: S₁[k] ; :: thesis: S₁[k + 1]
reconsider k = k as Element of NAT by ORDINAL1:def 12;
([#] (f,(the_unity_wrt multcomplex))) . (k + 1) is real

proof

per cases ( k + 1 in dom f or not k + 1 in dom f ) ;

suppose k + 1 in dom f ; :: thesis: ([#] (f,(the_unity_wrt multcomplex))) . (k + 1) is real

then ([#] (f,(the_unity_wrt multcomplex))) . (k + 1) = f . (k + 1) by SETWOP_2:20;
hence ([#] (f,(the_unity_wrt multcomplex))) . (k + 1) is real by A1; :: thesis: verum

end;

suppose not k + 1 in dom f ; :: thesis: ([#] (f,(the_unity_wrt multcomplex))) . (k + 1) is real

hence ([#] (f,(the_unity_wrt multcomplex))) . (k + 1) is real by BINOP_2:6, SETWOP_2:20; :: thesis: verum

end;

end;

end;

then reconsider a = ([#] (f,(the_unity_wrt multcomplex))) . (k + 1), b = multcomplex $$ ((finSeg k),([#] (f,(the_unity_wrt multcomplex)))) as Real by A4;
not k + 1 in Seg k by FINSEQ_3:8;
then multcomplex $$ (((finSeg k) \/ {.(In ((k + 1),NAT)).}),([#] (f,(the_unity_wrt multcomplex)))) = multcomplex . ((multcomplex $$ ((finSeg k),([#] (f,(the_unity_wrt multcomplex))))),(([#] (f,(the_unity_wrt multcomplex))) . (k + 1))) by SETWOP_2:2
.= b * a by BINOP_2:def 5 ;
hence S₁[k + 1] by FINSEQ_1:9; :: thesis: verum

end;

A5: ( multcomplex $$ f = multcomplex $$ ((findom f),([#] (f,(the_unity_wrt multcomplex)))) & ex n being Nat st dom f = Seg n ) by FINSEQ_1:def 2, SETWOP_2:def 2;
Seg 0 = {}. NAT ;
then A6: S₁[ 0 ] by BINOP_2:6, SETWISEO:31;
for n being Nat holds S₁[n] from NAT_1:sch 2(A6, A3);
hence Product F is real by A2, A5; :: thesis: verum