for C being 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)