deffunc
H
_{1}
(
Element
of
V
)
->
Element
of the
carrier
of
V
=
v
+
V
;
card
{
H
_{1}
(
w
) where
w
is
Element
of
V
:
w
in
A
}
c=
card
A
from
TREES_2:sch 2
();
then
card
(
v
+
A
)
is
finite
by
RUSUB_4:def 8
;
hence
v
+
A
is
finite
;
:: thesis:
verum