reconsider
g
=
f
.
(
x1
,
x2
) as
Element
of
Funcs
(
A
,
D
) ;
A1
:
[
x1
,
x2
]
in
[:
D1
,
D2
:]
;
(
dom
f
=
[:
D1
,
D2
:]
&
dom
g
=
A
)
by
FUNCT_2:def 1
;
then
f
..
(
x1
,
x2
,
x
)
=
g
.
x
by
A1
,
FUNCT_5:38
;
hence
f
..
(
x1
,
x2
,
x
) is
Element
of
D
;
:: thesis:
verum