let C be Function of [:COMPLEX,COMPLEX:],COMPLEX; 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; 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 ; 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 ; ( 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))
; C .: (x1,y1) = G .: (x2,y2)
A5:
len (G .: (x2,y2)) = len x1
by A1, A3, FINSEQ_2:72;
now for i being Nat st 1 <= i & i <= len (C .: (x1,y1)) holds
(C .: (x1,y1)) . i = (G .: (x2,y2)) . ilet i be
Nat;
( 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))
;
(C .: (x1,y1)) . i = (G .: (x2,y2)) . iA8:
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
;
verum end;
hence
C .: (x1,y1) = G .: (x2,y2)
by A5, A2, A3, FINSEQ_2:72; verum