A4
:
dom
g
=
X
by
FUNCT_2:def 1
;
A5
:
dom
(
f
mod
g
)
=
(
dom
f
)
/\
(
dom
g
)
by
Def4
;
A6
:
dom
f
=
X
by
FUNCT_2:def 1
;
rng
(
f
mod
g
)
c=
INT
;
hence
f
mod
g
is
Function
of
X
,
INT
by
A5
,
A6
,
A4
,
FUNCT_2:2
;
:: thesis:
verum