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 s 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 ex w being Element of dom Tr st
( x = w & len w = 1 ) ;
hence contradiction by A1, CARD_1:47, TARSKI:def 1; :: thesis: verum

end;

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