let cF be complex-valued XFinSequence; :: thesis: ( cF is real-valued implies Product cF = multreal "**" cF )
assume A1: cF is real-valued ; :: thesis: Product cF = multreal "**" cF

per cases ( len cF = 0 or len cF >= 1 ) by NAT_1:14;

suppose A2: len cF = 0 ; :: thesis: Product cF = multreal "**" cF

hence multreal "**" cF = the_unity_wrt multcomplex by BINOP_2:6, BINOP_2:7, AFINSQ_2:def 8, A1
.= Product cF by AFINSQ_2:def 8, A2 ;
:: thesis: verum

end;

suppose A3: len cF >= 1 ; :: thesis: Product cF = multreal "**" cF

A4: REAL = REAL /\ COMPLEX by MEMBERED:1, XBOOLE_1:28;

now :: thesis: for x, y being object st x in REAL & y in REAL holds
( multreal . (x,y) = multcomplex . (x,y) & multreal . (x,y) in REAL )

let x, y be object ; :: thesis: ( x in REAL & y in REAL implies ( multreal . (x,y) = multcomplex . (x,y) & multreal . (x,y) in REAL ) )
assume ( x in REAL & y in REAL ) ; :: thesis: ( multreal . (x,y) = multcomplex . (x,y) & multreal . (x,y) in REAL )
then reconsider X = x, Y = y as Element of REAL ;
multreal . (x,y) = X * Y by BINOP_2:def 11;
hence ( multreal . (x,y) = multcomplex . (x,y) & multreal . (x,y) in REAL ) by BINOP_2:def 5, XREAL_0:def 1; :: thesis: verum

end;

hence Product cF = multreal "**" cF by AFINSQ_2:47, A3, A4, A1; :: thesis: verum

end;

end;