A1
:
dom
g
=
X
by
FUNCT_2:def 1
;
A2
:
dom
(
f
div
g
)
=
(
dom
f
)
/\
(
dom
g
)
by
Def3
;
A3
:
dom
f
=
X
by
FUNCT_2:def 1
;
rng
(
f
div
g
)
c=
INT
;
hence
f
div
g
is
Function
of
X
,
INT
by
A2
,
A3
,
A1
,
FUNCT_2:2
;
:: thesis:
verum