dom
(
T

t
)
=
(
dom
T
)

t
by
TREES_2:def 10
;
hence
T

t
is
finite
by
FINSET_1:10
;
:: thesis:
verum