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

proof

let i be Element of NAT ; :: thesis: ( i in dom y1 implies compcomplex . (y1 . i) = compreal . (y2 . i) )
assume i in dom y1 ; :: thesis: compcomplex . (y1 . i) = compreal . (y2 . i)
- (y1 . i) = compcomplex . (y1 . i) by BINOP_2:def 1;
hence compcomplex . (y1 . i) = compreal . (y2 . i) by A1, BINOP_2:def 7; :: thesis: verum

end;

hence compcomplex * y1 = compreal * y2 by A2, Th46; :: thesis: verum