dom
(
R
~
)
=
rng
R
by
RELAT_1:20
.=
Y
by
FUNCT_2:def 3
;
hence
for
b
_{1}
being
Y
-defined
Relation
st
b
_{1}
=
R
~
holds
b
_{1}
is
total
by
PARTFUN1:def 2
;
:: thesis:
verum