let F be FinSequence of REAL ; :: thesis: Product F = multreal $$ F
rng F c= COMPLEX by NUMBERS:11, XBOOLE_1:1;
then reconsider f = F as FinSequence of COMPLEX by FINSEQ_1:def 4;
set g = multreal ;
set h = multcomplex ;
consider n being Nat such that
A1: dom f = Seg n by FINSEQ_1:def 2;
A2: multreal $$ F = multreal $$ (finSeg n),([#] F,(the_unity_wrt multreal )) by A1, SETWOP_2:def 2;
A3: multcomplex $$ f = multcomplex $$ (finSeg n),([#] f,(the_unity_wrt multcomplex )) by A1, SETWOP_2:def 2;
defpred S₁[ Nat] means multreal $$ (finSeg $1),([#] F,(the_unity_wrt multreal )) = multcomplex $$ (finSeg $1),([#] f,(the_unity_wrt multcomplex ));
A4: Seg 0 = {}. NAT ;
A5: S₁[ 0 ]

proof

multreal $$ (finSeg 0 ),([#] F,(the_unity_wrt multreal )) = the_unity_wrt multcomplex by A4, BINOP_2:6, BINOP_2:7, SETWISEO:40
.= multcomplex $$ (finSeg 0 ),([#] f,(the_unity_wrt multcomplex )) by A4, SETWISEO:40 ;
hence S₁[ 0 ] ; :: thesis: verum

end;

A6: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A7: S₁[k] ; :: thesis: S₁[k + 1]
set i = [#] F,(the_unity_wrt multreal );
set j = [#] f,(the_unity_wrt multcomplex );
A8: ([#] F,(the_unity_wrt multreal )) . (k + 1) = ([#] f,(the_unity_wrt multcomplex )) . (k + 1)

proof

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

suppose A9: k + 1 in dom f ; :: thesis: ([#] F,(the_unity_wrt multreal )) . (k + 1) = ([#] f,(the_unity_wrt multcomplex )) . (k + 1)

then ([#] f,(the_unity_wrt multcomplex )) . (k + 1) = F . (k + 1) by SETWOP_2:22
.= ([#] F,(the_unity_wrt multreal )) . (k + 1) by A9, SETWOP_2:22 ;
hence ([#] F,(the_unity_wrt multreal )) . (k + 1) = ([#] f,(the_unity_wrt multcomplex )) . (k + 1) ; :: thesis: verum

end;

suppose A10: not k + 1 in dom f ; :: thesis: ([#] F,(the_unity_wrt multreal )) . (k + 1) = ([#] f,(the_unity_wrt multcomplex )) . (k + 1)

then ([#] f,(the_unity_wrt multcomplex )) . (k + 1) = the_unity_wrt multcomplex by SETWOP_2:22
.= ([#] F,(the_unity_wrt multreal )) . (k + 1) by A10, BINOP_2:6, BINOP_2:7, SETWOP_2:22 ;
hence ([#] F,(the_unity_wrt multreal )) . (k + 1) = ([#] f,(the_unity_wrt multcomplex )) . (k + 1) ; :: thesis: verum

end;

end;

end;

A11: not k + 1 in Seg k by FINSEQ_3:9;
reconsider k = k as Element of NAT by ORDINAL1:def 13;
multreal $$ (finSeg (k + 1)),([#] F,(the_unity_wrt multreal )) = multreal $$ ((finSeg k) \/ {.(k + 1).}),([#] F,(the_unity_wrt multreal )) by FINSEQ_1:11
.= multreal . (multreal $$ (finSeg k),([#] F,(the_unity_wrt multreal ))),(([#] F,(the_unity_wrt multreal )) . (k + 1)) by A11, SETWOP_2:4
.= (multreal $$ (finSeg k),([#] F,(the_unity_wrt multreal ))) * (([#] F,(the_unity_wrt multreal )) . (k + 1)) by BINOP_2:def 11
.= multcomplex . (multcomplex $$ (finSeg k),([#] f,(the_unity_wrt multcomplex ))),(([#] f,(the_unity_wrt multcomplex )) . (k + 1)) by A7, A8, BINOP_2:def 5
.= multcomplex $$ ((finSeg k) \/ {.(k + 1).}),([#] f,(the_unity_wrt multcomplex )) by A11, SETWOP_2:4
.= multcomplex $$ (finSeg (k + 1)),([#] f,(the_unity_wrt multcomplex )) by FINSEQ_1:11 ;
hence S₁[k + 1] ; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A5, A6);
then multreal $$ F = multcomplex $$ f by A2, A3;
hence Product F = multreal $$ F by Def14; :: thesis: verum