let cF be complex-valued XFinSequence; ( cF is real-valued implies Product cF = multreal "**" cF )
assume A1:
cF is real-valued
; Product cF = multreal "**" cF
per cases
( len cF = 0 or len cF >= 1 )
by NAT_1:14;
suppose A3:
len cF >= 1
;
Product cF = multreal "**" cFA4:
REAL = REAL /\ COMPLEX
by MEMBERED:1, XBOOLE_1:28;
now 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 ;
( 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 )
;
( 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;
verum end; hence
Product cF = multreal "**" cF
by AFINSQ_2:47, A3, A4, A1;
verum end; end;