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)

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

hence
compcomplex * y1 = compreal * y2
by A2, Th46; :: thesis: verum
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;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