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 A1: ( a1 = a2 & y1 = y2 & 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) )
assume i in dom y1 ; :: thesis: (a1 multcomplex ) . (y1 . i) = (a2 multreal ) . (y2 . i)
A2: (a1 * y1) . i = a1 * (y1 . i) by Th16
.= multcomplex . a1,(y1 . i) by BINOP_2:def 5
.= multcomplex . a1,((id COMPLEX ) . (y1 . i)) by FUNCT_1:35
.= (multcomplex [;] a1,(id COMPLEX )) . (y1 . i) by FUNCOP_1:66
.= (a1 multcomplex ) . (y1 . i) by COMPLSP1:def 5 ;
(a2 * y2) . i = a2 * (y2 . i) by RVSUM_1:66
.= multreal . a2,(y2 . i) by BINOP_2:def 11
.= multreal . a2,((id REAL ) . (y2 . i)) by FUNCT_1:35
.= (multreal [;] a2,(id REAL )) . (y2 . i) by FUNCOP_1:66
.= (a2 multreal ) . (y2 . i) by RVSUM_1:def 3 ;
hence (a1 multcomplex ) . (y1 . i) = (a2 multreal ) . (y2 . i) by A1, A2; :: thesis: verum

end;

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