let C be Function of [:COMPLEX,COMPLEX:],COMPLEX; :: thesis: for G being Function of [:REAL,REAL:],REAL

for x1, y1 being FinSequence of COMPLEX

for x2, y2 being FinSequence of REAL st x1 = x2 & y1 = y2 & len x1 = len y2 & ( for i being Element of NAT st i in dom x1 holds

C . ((x1 . i),(y1 . i)) = G . ((x2 . i),(y2 . i)) ) holds

C .: (x1,y1) = G .: (x2,y2)

let G be Function of [:REAL,REAL:],REAL; :: thesis: for x1, y1 being FinSequence of COMPLEX

for x2, y2 being FinSequence of REAL st x1 = x2 & y1 = y2 & len x1 = len y2 & ( for i being Element of NAT st i in dom x1 holds

C . ((x1 . i),(y1 . i)) = G . ((x2 . i),(y2 . i)) ) holds

C .: (x1,y1) = G .: (x2,y2)

let x1, y1 be FinSequence of COMPLEX ; :: thesis: for x2, y2 being FinSequence of REAL st x1 = x2 & y1 = y2 & len x1 = len y2 & ( for i being Element of NAT st i in dom x1 holds

C . ((x1 . i),(y1 . i)) = G . ((x2 . i),(y2 . i)) ) holds

C .: (x1,y1) = G .: (x2,y2)

let x2, y2 be FinSequence of REAL ; :: thesis: ( x1 = x2 & y1 = y2 & len x1 = len y2 & ( for i being Element of NAT st i in dom x1 holds

C . ((x1 . i),(y1 . i)) = G . ((x2 . i),(y2 . i)) ) implies C .: (x1,y1) = G .: (x2,y2) )

assume that

A1: x1 = x2 and

A2: y1 = y2 and

A3: len x1 = len y2 and

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

C . ((x1 . i),(y1 . i)) = G . ((x2 . i),(y2 . i)) ; :: thesis: C .: (x1,y1) = G .: (x2,y2)

A5: len (G .: (x2,y2)) = len x1 by A1, A3, FINSEQ_2:72;

for x1, y1 being FinSequence of COMPLEX

for x2, y2 being FinSequence of REAL st x1 = x2 & y1 = y2 & len x1 = len y2 & ( for i being Element of NAT st i in dom x1 holds

C . ((x1 . i),(y1 . i)) = G . ((x2 . i),(y2 . i)) ) holds

C .: (x1,y1) = G .: (x2,y2)

let G be Function of [:REAL,REAL:],REAL; :: thesis: for x1, y1 being FinSequence of COMPLEX

for x2, y2 being FinSequence of REAL st x1 = x2 & y1 = y2 & len x1 = len y2 & ( for i being Element of NAT st i in dom x1 holds

C . ((x1 . i),(y1 . i)) = G . ((x2 . i),(y2 . i)) ) holds

C .: (x1,y1) = G .: (x2,y2)

let x1, y1 be FinSequence of COMPLEX ; :: thesis: for x2, y2 being FinSequence of REAL st x1 = x2 & y1 = y2 & len x1 = len y2 & ( for i being Element of NAT st i in dom x1 holds

C . ((x1 . i),(y1 . i)) = G . ((x2 . i),(y2 . i)) ) holds

C .: (x1,y1) = G .: (x2,y2)

let x2, y2 be FinSequence of REAL ; :: thesis: ( x1 = x2 & y1 = y2 & len x1 = len y2 & ( for i being Element of NAT st i in dom x1 holds

C . ((x1 . i),(y1 . i)) = G . ((x2 . i),(y2 . i)) ) implies C .: (x1,y1) = G .: (x2,y2) )

assume that

A1: x1 = x2 and

A2: y1 = y2 and

A3: len x1 = len y2 and

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

C . ((x1 . i),(y1 . i)) = G . ((x2 . i),(y2 . i)) ; :: thesis: C .: (x1,y1) = G .: (x2,y2)

A5: len (G .: (x2,y2)) = len x1 by A1, A3, FINSEQ_2:72;

now :: thesis: for i being Nat st 1 <= i & i <= len (C .: (x1,y1)) holds

(C .: (x1,y1)) . i = (G .: (x2,y2)) . i

hence
C .: (x1,y1) = G .: (x2,y2)
by A5, A2, A3, FINSEQ_2:72; :: thesis: verum(C .: (x1,y1)) . i = (G .: (x2,y2)) . i

let i be Nat; :: thesis: ( 1 <= i & i <= len (C .: (x1,y1)) implies (C .: (x1,y1)) . i = (G .: (x2,y2)) . i )

assume that

A6: 1 <= i and

A7: i <= len (C .: (x1,y1)) ; :: thesis: (C .: (x1,y1)) . i = (G .: (x2,y2)) . i

A8: i <= len x1 by A2, A3, A7, FINSEQ_2:72;

then A9: i in dom x1 by A6, FINSEQ_3:25;

A10: i in dom (G .: (x2,y2)) by A5, A6, A8, FINSEQ_3:25;

i in dom (C .: (x1,y1)) by A6, A7, FINSEQ_3:25;

hence (C .: (x1,y1)) . i = C . ((x1 . i),(y1 . i)) by FUNCOP_1:22

.= G . ((x2 . i),(y2 . i)) by A4, A9

.= (G .: (x2,y2)) . i by A10, FUNCOP_1:22 ;

:: thesis: verum

end;assume that

A6: 1 <= i and

A7: i <= len (C .: (x1,y1)) ; :: thesis: (C .: (x1,y1)) . i = (G .: (x2,y2)) . i

A8: i <= len x1 by A2, A3, A7, FINSEQ_2:72;

then A9: i in dom x1 by A6, FINSEQ_3:25;

A10: i in dom (G .: (x2,y2)) by A5, A6, A8, FINSEQ_3:25;

i in dom (C .: (x1,y1)) by A6, A7, FINSEQ_3:25;

hence (C .: (x1,y1)) . i = C . ((x1 . i),(y1 . i)) by FUNCOP_1:22

.= G . ((x2 . i),(y2 . i)) by A4, A9

.= (G .: (x2,y2)) . i by A10, FUNCOP_1:22 ;

:: thesis: verum