deffunc H3( set , set ) -> set = $2 \/ { ([o,0] -tree p) where o is Symbol of F1(), p is Element of $2 * : ex q being FinSequence of FinTrees [: the carrier of F1(),NAT:] st
( p = q & o ==> pr1 (roots q) ) } ;
consider f being Function such that
A3: dom f = NAT and
A4: f . 0 = { (root-tree [t,d]) where t is Symbol of F1(), d is Element of NAT : ( ( t in Terminals F1() & d = H1(t) ) or ( t ==> {} & d = H2(t, {} , {} ) ) ) } and
A5: for n being Nat holds f . (n + 1) = H3(n,f . n) from NAT_1:sch 11();
 A6: for n being Nat holds f . (n + 1) = (f . n) \/ { ([o,H2(o, pr1 (roots p), pr2 (roots p))] -tree p) where o is Symbol of F1(), p is Element of (f . n) * : ex q being FinSequence of FinTrees [: the carrier of F1(),NAT:] st
( p = q & o ==> pr1 (roots q) ) } by A5;
A7: ex X being Subset of (FinTrees [: the carrier of F1(),NAT:]) st
( X = Union f & ( for d being Symbol of F1() st d in Terminals F1() holds
root-tree [d,H1(d)] in X ) & ( for o being Symbol of F1()
for p being FinSequence of X st o ==> pr1 (roots p) holds
[o,H2(o, pr1 (roots p), pr2 (roots p))] -tree p in X ) & ( for F being Subset of (FinTrees [: the carrier of F1(),NAT:]) st ( for d being Symbol of F1() st d in Terminals F1() holds
root-tree [d,H1(d)] in F ) & ( for o being Symbol of F1()
for p being FinSequence of F st o ==> pr1 (roots p) holds
[o,H2(o, pr1 (roots p), pr2 (roots p))] -tree p in F ) holds
X c= F ) ) from DTCONSTR:sch 3(A3, A4, A6);
 consider TSG being Subset of (FinTrees the carrier of F1()) such that
A8: TSG = { (t `1) where t is Element of FinTrees [: the carrier of F1(),NAT:] : t in Union f } and
A9: for d being Symbol of F1() st d in Terminals F1() holds
root-tree d in TSG and
A10: for o being Symbol of F1()
for p being FinSequence of TSG st o ==> roots p holds
o -tree p in TSG and
A11: for F being Subset of (FinTrees the carrier of F1()) st ( for d being Symbol of F1() st d in Terminals F1() holds
root-tree d in F ) & ( for o being Symbol of F1()
for p being FinSequence of F st o ==> roots p holds
o -tree p in F ) holds
TSG c= F from DTCONSTR:sch 4(A3, A4, A6);
 A12: TSG = TS F1() by A9, A10, A11, Def1;
defpred S1[ Nat] means for t being DecoratedTree of [: the carrier of F1(),NAT:] st t in f . $1 holds
P1[t `1 ];
A13: S1[ 0 ]
proof
let tt be DecoratedTree of [: the carrier of F1(),NAT:]; :: thesis: ( tt in f . 0 implies P1[tt `1 ] )
set p = <*> (TS F1());
assume tt in f . 0 ; :: thesis: P1[tt `1 ]
then consider t being Symbol of F1(), d being Element of NAT such that
A14: tt = root-tree [t,d] and
A15: ( ( t in Terminals F1() & d = 0 ) or ( t ==> roots (<*> (TS F1())) & d = 0 ) ) by A4, Th3;
A16: tt `1 = root-tree t by A14, TREES_4:25;
A17: t -tree (<*> (TS F1())) = root-tree t by TREES_4:20;
for T being DecoratedTree of the carrier of F1() st T in rng (<*> (TS F1())) holds
P1[T] ;
hence P1[tt `1 ] by A1, A2, A15, A16, A17; :: thesis: verum
end;
A18: now :: thesis: for n being Nat st S1[n] holds
S1[n + 1]
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A19: S1[n] ; :: thesis: S1[n + 1]
thus S1[n + 1] :: thesis: verum
proof
let x be DecoratedTree of [: the carrier of F1(),NAT:]; :: thesis: ( x in f . (n + 1) implies P1[x `1 ] )
assume that
A20: x in f . (n + 1) and
A21: P1[x `1 ] ; :: thesis: contradiction
x in (f . n) \/ { ([o,0] -tree p) where o is Symbol of F1(), p is Element of (f . n) * : ex q being FinSequence of FinTrees [: the carrier of F1(),NAT:] st
( p = q & o ==> pr1 (roots q) ) } by A5, A20;
then ( x in f . n or x in { ([o,0] -tree p) where o is Symbol of F1(), p is Element of (f . n) * : ex q being FinSequence of FinTrees [: the carrier of F1(),NAT:] st
( p = q & o ==> pr1 (roots q) ) } ) by XBOOLE_0:def 3;
then consider o being Symbol of F1(), p being Element of (f . n) * such that
A22: x = [o,0] -tree p and
A23: ex q being FinSequence of FinTrees [: the carrier of F1(),NAT:] st
( p = q & o ==> pr1 (roots q) ) by A19, A21;
A24: Union f = union (rng f) by CARD_3:def 4;
n in NAT by ORDINAL1:def 12;
then A25: f . n in rng f by A3, FUNCT_1:def 3;
A26: rng p c= f . n by FINSEQ_1:def 4;
A27: f . n c= Union f by A24, A25, ZFMISC_1:74;
A28: dom p = Seg (len p) by FINSEQ_1:def 3;
defpred S2[ set , set ] means ex dt being Element of FinTrees [: the carrier of F1(),NAT:] st
( dt = p . $1 & dt `1 = $2 & dt in Union f );
A29: for k being Nat st k in Seg (len p) holds
ex x being Element of FinTrees the carrier of F1() st S2[k,x]
proof
let k be Nat; :: thesis: ( k in Seg (len p) implies ex x being Element of FinTrees the carrier of F1() st S2[k,x] )
assume k in Seg (len p) ; :: thesis: ex x being Element of FinTrees the carrier of F1() st S2[k,x]
then A30: p . k in rng p by A28, FUNCT_1:def 3;
A31: rng p c= Union f by A26, A27;
then p . k in Union f by A30;
then reconsider dt = p . k as Element of FinTrees [: the carrier of F1(),NAT:] by A7;
A32: dt `1 = (pr1 ( the carrier of F1(),NAT)) * dt by TREES_3:def 12;
A33: rng dt c= [: the carrier of F1(),NAT:] by RELAT_1:def 19;
dom (pr1 ( the carrier of F1(),NAT)) = [: the carrier of F1(),NAT:] by FUNCT_2:def 1;
then dom (dt `1) = dom dt by A32, A33, RELAT_1:27;
then reconsider x = dt `1 as Element of FinTrees the carrier of F1() by TREES_3:def 8;
take x ; :: thesis: S2[k,x]
take dt ; :: thesis: ( dt = p . k & dt `1 = x & dt in Union f )
thus ( dt = p . k & dt `1 = x & dt in Union f ) by A30, A31; :: thesis: verum
end;
consider p1 being FinSequence of FinTrees the carrier of F1() such that
A34: dom p1 = Seg (len p) and
A35: for k being Nat st k in Seg (len p) holds
S2[k,p1 . k] from FINSEQ_1:sch 5(A29);
 reconsider p = p as FinSequence of Trees [: the carrier of F1(),NAT:] by A23, Th1;
A36: dom (roots p1) = dom p1 by TREES_3:def 18;
A37: dom (pr1 (roots p)) = dom (roots p) by MCART_1:def 12;
then A38: dom (pr1 (roots p)) = dom p1 by A28, A34, TREES_3:def 18;
now :: thesis: for k being Nat st k in dom p1 holds
(roots p1) . k = (pr1 (roots p)) . k
let k be Nat; :: thesis: ( k in dom p1 implies (roots p1) . k = (pr1 (roots p)) . k )
assume A39: k in dom p1 ; :: thesis: (roots p1) . k = (pr1 (roots p)) . k
then consider dt being Element of FinTrees [: the carrier of F1(),NAT:] such that
A40: dt = p . k and
A41: dt `1 = p1 . k and
dt in Union f by A34, A35;
reconsider r = {} as Node of dt by TREES_1:22;
ex T being DecoratedTree st
( T = p1 . k & (roots p1) . k = T . {} ) by A39, TREES_3:def 18;
then A42: (roots p1) . k = (dt . r) `1 by A41, TREES_3:39;
ex T being DecoratedTree st
( T = p . k & (roots p) . k = T . {} ) by A28, A34, A39, TREES_3:def 18;
hence (roots p1) . k = (pr1 (roots p)) . k by A37, A38, A39, A40, A42, MCART_1:def 12; :: thesis: verum
end;
then A43: roots p1 = pr1 (roots p) by A36, A38, FINSEQ_1:13;
rng p1 c= TS F1()
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng p1 or x in TS F1() )
assume x in rng p1 ; :: thesis: x in TS F1()
then consider k being object such that
A44: k in dom p1 and
A45: x = p1 . k by FUNCT_1:def 3;
reconsider k = k as Element of NAT by A44;
ex dt being Element of FinTrees [: the carrier of F1(),NAT:] st
( dt = p . k & dt `1 = p1 . k & dt in Union f ) by A34, A35, A44;
hence x in TS F1() by A8, A12, A45; :: thesis: verum
end;
then reconsider p1 = p1 as FinSequence of TS F1() by FINSEQ_1:def 4;
now :: thesis: for t being DecoratedTree of the carrier of F1() st t in rng p1 holds
P1[t]
let t be DecoratedTree of the carrier of F1(); :: thesis: ( t in rng p1 implies P1[t] )
assume t in rng p1 ; :: thesis: P1[t]
then consider k being object such that
A46: k in dom p1 and
A47: t = p1 . k by FUNCT_1:def 3;
reconsider k = k as Element of NAT by A46;
A48: ex dt being Element of FinTrees [: the carrier of F1(),NAT:] st
( dt = p . k & dt `1 = p1 . k & dt in Union f ) by A34, A35, A46;
p . k in rng p by A28, A34, A46, FUNCT_1:def 3;
hence P1[t] by A19, A26, A47, A48; :: thesis: verum
end;
then A49: P1[o -tree p1] by A2, A23, A43;
reconsider p1 = p1 as FinSequence of Trees the carrier of F1() by Th1;
now :: thesis: for k being Nat st k in dom p holds
for T being DecoratedTree of [: the carrier of F1(),NAT:] st T = p . k holds
p1 . k = T `1
let k be Nat; :: thesis: ( k in dom p implies for T being DecoratedTree of [: the carrier of F1(),NAT:] st T = p . k holds
p1 . k = T `1 )
assume k in dom p ; :: thesis: for T being DecoratedTree of [: the carrier of F1(),NAT:] st T = p . k holds
p1 . k = T `1
then ex dt being Element of FinTrees [: the carrier of F1(),NAT:] st
( dt = p . k & dt `1 = p1 . k & dt in Union f ) by A28, A35;
hence for T being DecoratedTree of [: the carrier of F1(),NAT:] st T = p . k holds
p1 . k = T `1 ; :: thesis: verum
end;
hence contradiction by A21, A22, A28, A34, A49, TREES_4:27; :: thesis: verum
end;
end;
A50: for n being Nat holds S1[n] from NAT_1:sch 2(A13, A18);
 let t be DecoratedTree of the carrier of F1(); :: thesis: ( t in TS F1() implies P1[t] )
assume t in TS F1() ; :: thesis: P1[t]
then consider tt being Element of FinTrees [: the carrier of F1(),NAT:] such that
A51: t = tt `1 and
A52: tt in Union f by A8, A12;
ex n being object st
( n in NAT & tt in f . n ) by A3, A52, CARD_5:2;
hence P1[t] by A50, A51; :: thesis: verum