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 set st p0 in [:REAL ,REAL :] holds
f . p0 = g . p0

proof

let p0 be set ; :: 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 set 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, MCART_1:7;
A15: p0 `2 = b by A13, MCART_1:7;
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:18; :: thesis: verum