deffunc H1( Real, Real) -> set = $1 + ($2 * <i>);
A1:
for x, y being Element of REAL holds H1(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) = H1(x,y)
from FUNCT_7:sch 1(A1);
deffunc H2( Element of [:REAL,REAL:]) -> set = f . (($1 `1),($1 `2));
consider g being Function of [:REAL,REAL:],COMPLEX such that
A5:
for p being Element of [:REAL,REAL:] holds g . p = H2(p)
from FUNCT_2:sch 8(A3);
take
g
; 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:];
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 ;
( a = p `1 & b = p `2 implies g . [a,b] = a + (b * <i>) )
assume A6:
(
a = p `1 &
b = p `2 )
;
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>)
;
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>)
; verum