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 A1: ( 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) ) ) ; :: thesis: C .: x1,y1 = G .: x2,y2
then A2: len (C .: x1,y1) = len x1 by FINSEQ_2:86;
A3: len (G .: x2,y2) = len x1 by A1, FINSEQ_2:86;

now

let i be Nat; :: thesis: ( 1 <= i & i <= len (C .: x1,y1) implies (C .: x1,y1) . i = (G .: x2,y2) . i )
assume A4: ( 1 <= i & i <= len (C .: x1,y1) ) ; :: thesis: (C .: x1,y1) . i = (G .: x2,y2) . i
then A5: ( 1 <= i & i <= len x1 ) by A1, FINSEQ_2:86;
then A6: i in dom x1 by FINSEQ_3:27;
A7: i in dom (G .: x2,y2) by A3, A5, FINSEQ_3:27;
i in dom (C .: x1,y1) by A4, FINSEQ_3:27;
hence (C .: x1,y1) . i = C . (x1 . i),(y1 . i) by FUNCOP_1:28
.= G . (x2 . i),(y2 . i) by A1, A6
.= (G .: x2,y2) . i by A7, FUNCOP_1:28 ;
:: thesis: verum

end;

hence C .: x1,y1 = G .: x2,y2 by A2, A3, FINSEQ_1:18; :: thesis: verum