let x1, y1 be FinSequence of COMPLEX ; for x2, y2 being FinSequence of REAL st x1 = x2 & y1 = y2 & len x1 = len y2 holds
addcomplex .: (x1,y1) = addreal .: (x2,y2)
let x2, y2 be FinSequence of REAL ; ( x1 = x2 & y1 = y2 & len x1 = len y2 implies addcomplex .: (x1,y1) = addreal .: (x2,y2) )
assume that
A1:
( x1 = x2 & y1 = y2 )
and
A2:
len x1 = len y2
; addcomplex .: (x1,y1) = addreal .: (x2,y2)
for i being Element of NAT st i in dom x1 holds
addcomplex . ((x1 . i),(y1 . i)) = addreal . ((x2 . i),(y2 . i))
hence
addcomplex .: (x1,y1) = addreal .: (x2,y2)
by A1, A2, Th38; verum