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

diffcomplex .: (x1,y1) = diffreal .: (x2,y2)

let x2, y2 be FinSequence of REAL ; :: thesis: ( x1 = x2 & y1 = y2 & len x1 = len y2 implies diffcomplex .: (x1,y1) = diffreal .: (x2,y2) )

assume that

A1: ( x1 = x2 & y1 = y2 ) and

A2: len x1 = len y2 ; :: thesis: diffcomplex .: (x1,y1) = diffreal .: (x2,y2)

for i being Element of NAT st i in dom x1 holds

diffcomplex . ((x1 . i),(y1 . i)) = diffreal . ((x2 . i),(y2 . i))

diffcomplex .: (x1,y1) = diffreal .: (x2,y2)

let x2, y2 be FinSequence of REAL ; :: thesis: ( x1 = x2 & y1 = y2 & len x1 = len y2 implies diffcomplex .: (x1,y1) = diffreal .: (x2,y2) )

assume that

A1: ( x1 = x2 & y1 = y2 ) and

A2: len x1 = len y2 ; :: thesis: diffcomplex .: (x1,y1) = diffreal .: (x2,y2)

for i being Element of NAT st i in dom x1 holds

diffcomplex . ((x1 . i),(y1 . i)) = diffreal . ((x2 . i),(y2 . i))

proof

hence
diffcomplex .: (x1,y1) = diffreal .: (x2,y2)
by A1, A2, Th38; :: thesis: verum
let i be Element of NAT ; :: thesis: ( i in dom x1 implies diffcomplex . ((x1 . i),(y1 . i)) = diffreal . ((x2 . i),(y2 . i)) )

(x1 . i) - (y1 . i) = diffcomplex . ((x1 . i),(y1 . i)) by BINOP_2:def 4;

hence ( i in dom x1 implies diffcomplex . ((x1 . i),(y1 . i)) = diffreal . ((x2 . i),(y2 . i)) ) by A1, BINOP_2:def 10; :: thesis: verum

end;(x1 . i) - (y1 . i) = diffcomplex . ((x1 . i),(y1 . i)) by BINOP_2:def 4;

hence ( i in dom x1 implies diffcomplex . ((x1 . i),(y1 . i)) = diffreal . ((x2 . i),(y2 . i)) ) by A1, BINOP_2:def 10; :: thesis: verum