consider x being type of s;
set Tr = {{} } --> [[<*x*>,x],0 ];
A1: dom ({{} } --> [[<*x*>,x],0 ]) = {{} } by FUNCOP_1:19;
reconsider Tr = {{} } --> [[<*x*>,x],0 ] as finite DecoratedTree by TREES_1:48;
A2: [[<*x*>,x],0 ] in [:H₁(s),NAT :] by ZFMISC_1:106;
{[[<*x*>,x],0 ]} = rng Tr by FUNCOP_1:14;
then rng Tr c= [:H₁(s),NAT :] by A2, ZFMISC_1:37;
then reconsider Tr = Tr as PreProof of by RELAT_1:def 19;
take Tr ; :: thesis: ( dom Tr is finite & ( for v being Element of dom Tr holds v is correct ) )
thus dom Tr is finite ; :: thesis: for v being Element of dom Tr holds v is correct
let v be Element of dom Tr; :: thesis: v is correct
A3: v = {} by A1, TARSKI:def 1;

A4: now

consider x being Element of (dom Tr) -level 1;
assume (dom Tr) -level 1 <> {} ; :: thesis: contradiction
then x in (dom Tr) -level 1 ;
then x in { w where w is Element of dom Tr : len w = 1 } by TREES_2:def 6;
then consider w being Element of dom Tr such that
A5: ( x = w & len w = 1 ) ;
w = {} by A1, TARSKI:def 1;
hence contradiction by A5, CARD_1:47; :: thesis: verum

end;

A6: branchdeg v = card (succ v) by TREES_2:def 13
.= 0 by A3, A4, CARD_1:47, TREES_2:15 ;
Tr . v = [[<*x*>,x],0 ] by A1, FUNCOP_1:13;
then ( (Tr . v) `1 = [<*x*>,x] & (Tr . v) `2 = 0 ) by MCART_1:7;
hence v is correct by A6, Def5; :: thesis: verum