deffunc
H
_{1}
(
Element
of
V
)
->
Element
of the
carrier
of
V
=
r
*
$1;
defpred
S
_{1}
[
set
]
means
$1
in
M
;
{
H
_{1}
(
v
) where
v
is
Element
of
V
:
S
_{1}
[
v
] } is
Subset
of
V
from
DOMAIN_1:sch 8
();
hence
{
(
r
*
v
) where
v
is
Element
of
V
:
v
in
M
} is
Subset
of
V
;
:: thesis:
verum