let f, g be Function of [:REAL,REAL:],COMPLEX; :: thesis: ( ( for p being Element of [:REAL,REAL:]
for a, b being Element of REAL st a = p `1 & b = p `2 holds
f . [a,b] = a + (b * <i>) ) & ( for p being Element of [:REAL,REAL:]
for a, b being Element of REAL st a = p `1 & b = p `2 holds
g . [a,b] = a + (b * <i>) ) implies f = g )
assume A10: for p being Element of [:REAL,REAL:]
for a, b being Element of REAL st a = p `1 & b = p `2 holds
f . [a,b] = a + (b * <i>) ; :: thesis: ( ex p being Element of [:REAL,REAL:] ex a, b being Element of REAL st
( a = p `1 & b = p `2 & not g . [a,b] = a + (b * <i>) ) or f = g )
assume A11: for p being Element of [:REAL,REAL:]
for a, b being Element of REAL st a = p `1 & b = p `2 holds
g . [a,b] = a + (b * <i>) ; :: thesis: f = g
for p0 being object st p0 in [:REAL,REAL:] holds
f . p0 = g . p0

proof

let p0 be object ; :: thesis: ( p0 in [:REAL,REAL:] implies f . p0 = g . p0 )
assume A12: p0 in [:REAL,REAL:] ; :: thesis: f . p0 = g . p0
then consider x0, y0 being object such that
A13: ( x0 in REAL & y0 in REAL & p0 = [x0,y0] ) by ZFMISC_1:def 2;
reconsider a = x0, b = y0 as Element of REAL by A13;
A14: p0 `1 = a by A13;
A15: p0 `2 = b by A13;
then f . p0 = a + (b * <i>) by A12, A10, A14, A13
.= g . p0 by A13, A12, A11, A14, A15 ;
hence f . p0 = g . p0 ; :: thesis: verum

end;

hence f = g by FUNCT_2:12; :: thesis: verum