let a1 be Element of COMPLEX ; :: thesis: for y1 being FinSequence of COMPLEX
for a2 being Element of REAL
for y2 being FinSequence of REAL st a1 = a2 & y1 = y2 & len y1 = len y2 holds
(a1 multcomplex) * y1 = (a2 multreal) * y2
let y1 be FinSequence of COMPLEX ; :: thesis: for a2 being Element of REAL
for y2 being FinSequence of REAL st a1 = a2 & y1 = y2 & len y1 = len y2 holds
(a1 multcomplex) * y1 = (a2 multreal) * y2
let a2 be Element of REAL ; :: thesis: for y2 being FinSequence of REAL st a1 = a2 & y1 = y2 & len y1 = len y2 holds
(a1 multcomplex) * y1 = (a2 multreal) * y2
let y2 be FinSequence of REAL ; :: thesis: ( a1 = a2 & y1 = y2 & len y1 = len y2 implies (a1 multcomplex) * y1 = (a2 multreal) * y2 )
assume that
A1: ( a1 = a2 & y1 = y2 ) and
A2: len y1 = len y2 ; :: thesis: (a1 multcomplex) * y1 = (a2 multreal) * y2
for i being Element of NAT st i in dom y1 holds
(a1 multcomplex) . (y1 . i) = (a2 multreal) . (y2 . i)

proof

let i be Element of NAT ; :: thesis: ( i in dom y1 implies (a1 multcomplex) . (y1 . i) = (a2 multreal) . (y2 . i) )
reconsider y2i = y2 . i as Element of REAL by XREAL_0:def 1;
assume i in dom y1 ; :: thesis: (a1 multcomplex) . (y1 . i) = (a2 multreal) . (y2 . i)
A3: (a2 * y2) . i = a2 * (y2 . i) by RVSUM_1:44
.= multreal . (a2,((id REAL) . y2i)) by BINOP_2:def 11
.= (multreal [;] (a2,(id REAL))) . y2i by FUNCOP_1:53
.= (a2 multreal) . (y2 . i) by RVSUM_1:def 3 ;
(a1 * y1) . i = a1 * (y1 . i) by Th12
.= multcomplex . (a1,((id COMPLEX) . (y1 . i))) by BINOP_2:def 5
.= (multcomplex [;] (a1,(id COMPLEX))) . (y1 . i) by FUNCOP_1:53
.= (a1 multcomplex) . (y1 . i) by SEQ_4:def 4 ;
hence (a1 multcomplex) . (y1 . i) = (a2 multreal) . (y2 . i) by A1, A3; :: thesis: verum

end;

hence (a1 multcomplex) * y1 = (a2 multreal) * y2 by A2, Th46; :: thesis: verum