deffunc H₁( Real, Real) -> set = $1 + ($2 * <i>);
A1: for x, y being Element of REAL holds H₁(x,y) in COMPLEX by XCMPLX_0:def 2;
consider f being Function of [:REAL,REAL:],COMPLEX such that
A2: for x, y being Element of REAL holds f . (x,y) = H₁(x,y) from FUNCT_7:sch 1(A1);
deffunc H₂( Element of [:REAL,REAL:]) -> set = f . (($1 `1),($1 `2));

A3: now :: thesis: for p being Element of [:REAL,REAL:] holds H₂(p) in COMPLEX

let p be Element of [:REAL,REAL:]; :: thesis: H₂(p) in COMPLEX
( p `1 is Element of REAL & p `2 is Element of REAL ) by MCART_1:10;
then consider a, b being Element of REAL such that
A4: ( a = p `1 & b = p `2 ) ;
H₂(p) = a + (b * <i>) by A2, A4;
hence H₂(p) in COMPLEX by XCMPLX_0:def 2; :: thesis: verum

end;

consider g being Function of [:REAL,REAL:],COMPLEX such that
A5: for p being Element of [:REAL,REAL:] holds g . p = H₂(p) from FUNCT_2:sch 8(A3);
take g ; :: thesis: 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>)
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>)

proof

let p be Element of [:REAL,REAL:]; :: thesis: for a, b being Element of REAL st a = p `1 & b = p `2 holds
g . [a,b] = a + (b * <i>)
let a, b be Element of REAL ; :: thesis: ( a = p `1 & b = p `2 implies g . [a,b] = a + (b * <i>) )
assume A6: ( a = p `1 & b = p `2 ) ; :: thesis: g . [a,b] = a + (b * <i>)
A8: [a,b] is Element of [:REAL,REAL:] by ZFMISC_1:def 2;
A9: [a,b] `1 = p `1 by A6;
[a,b] `2 = p `2 by A6;
then g . [a,b] = f . (a,b) by A5, A8, A9
.= a + (b * <i>) by A2 ;
hence g . [a,b] = a + (b * <i>) ; :: thesis: verum

end;

hence 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: verum