o
in
rng
the
charact
of
S
;
then
(
o
<>
{}
&
o
in
PFuncs
(
(
the
carrier
of
S
*
)
, the
carrier
of
S
) )
by
RELAT_1:def 9
;
then
(
o
.
a
in
rng
o
&
rng
o
c=
the
carrier
of
S
)
by
RELAT_1:def 19
,
FUNCT_1:3
;
hence
o
.
a
is
Element
of
S
;
:: thesis:
verum