set x = the type of s;
set Tr = {{}} --> [[<* the type of s*>, the type of s],0];
A1: dom ({{}} --> [[<* the type of s*>, the type of s],0]) = {{}} by FUNCOP_1:13;
reconsider Tr = {{}} --> [[<* the type of s*>, the type of s],0] as finite DecoratedTree by TREES_1:23;
A2: [[<* the type of s*>, the type of s],0] in [:H1(s),NAT:] by ZFMISC_1:87;
{[[<* the type of s*>, the type of s],0]} = rng Tr by FUNCOP_1:8;
then rng Tr c= [:H1(s),NAT:] by A2, ZFMISC_1:31;
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 :: thesis: not (dom Tr) -level 1 <> {}
set x = the Element of (dom Tr) -level 1;
assume (dom Tr) -level 1 <> {} ; :: thesis: contradiction
then the Element of (dom Tr) -level 1 in (dom Tr) -level 1 ;
then the Element of (dom Tr) -level 1 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
( the Element of (dom Tr) -level 1 = w & len w = 1 ) ;
hence contradiction by A1, CARD_1:27, TARSKI:def 1; :: thesis: verum
end;
A5: branchdeg v = card (succ v) by TREES_2:def 12
.= 0 by A3, A4, CARD_1:27, TREES_2:13 ;
A6: Tr . v = [[<* the type of s*>, the type of s],0] by A1, FUNCOP_1:7;
then A7: (Tr . v) `1 = [<* the type of s*>, the type of s] ;
(Tr . v) `2 = 0 by A6;
hence v is correct by A5, A7, Def4; :: thesis: verum