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

proof

let i be Element of NAT ; :: thesis: ( i in dom x1 implies multcomplex . (x1 . i),(y1 . i) = multreal . (x2 . i),(y2 . i) )
(x1 . i) * (y1 . i) = multcomplex . (x1 . i),(y1 . i) by BINOP_2:def 5;
hence ( i in dom x1 implies multcomplex . (x1 . i),(y1 . i) = multreal . (x2 . i),(y2 . i) ) by A1, A2, BINOP_2:def 11; :: thesis: verum

end;

hence multcomplex .: x1,y1 = multreal .: x2,y2 by A1, A2, A3, COMPLSP2:45; :: thesis: verum