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
() * 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
() * 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
() * y1 = (a2 multreal) * y2

let y2 be FinSequence of REAL ; :: thesis: ( a1 = a2 & y1 = y2 & len y1 = len y2 implies () * y1 = (a2 multreal) * y2 )
assume that
A1: ( a1 = a2 & y1 = y2 ) and
A2: len y1 = len y2 ; :: thesis: () * y1 = (a2 multreal) * y2
for i being Element of NAT st i in dom y1 holds
() . (y1 . i) = (a2 multreal) . (y2 . i)
proof
let i be Element of NAT ; :: thesis: ( i in dom y1 implies () . (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: () . (y1 . i) = (a2 multreal) . (y2 . i)
A3: (a2 * y2) . i = a2 * (y2 . i) by RVSUM_1:44
.= multreal . (a2,(() . y2i)) by BINOP_2:def 11
.= (multreal [;] (a2,())) . y2i by FUNCOP_1:53
.= (a2 multreal) . (y2 . i) by RVSUM_1:def 3 ;
(a1 * y1) . i = a1 * (y1 . i) by Th12
.= multcomplex . (a1,(() . (y1 . i))) by BINOP_2:def 5
.= (multcomplex [;] (a1,())) . (y1 . i) by FUNCOP_1:53
.= () . (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 ; :: thesis: verum