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
; ( dom Tr is finite & ( for v being Element of dom Tr holds v is correct ) )
thus
dom Tr is finite
; for v being Element of dom Tr holds v is correct
let v be Element of dom Tr; v is correct
A3:
v = {}
by A1, TARSKI:def 1;
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; verum