set f = F₁();
set G = F₂();
set D = F₃();
set S = the carrier of F₂();
set SxD = [:the carrier of F₂(),F₃():];
deffunc H₃( Symbol of F₂(), FinSequence) -> Element of F₃() = F₅($1,(pr1 (roots $2)),(pr2 (roots $2)));
A4: F₁() . 0 = { (root-tree [t,d]) where t is Symbol of F₂(), d is Element of F₃() : ( ( t in Terminals F₂() & d = F₄(t) ) or ( t ==> {} & d = F₅(t,{} ,{} ) ) ) } by A2;
A5: for n being Element of NAT holds F₁() . (n + 1) = (F₁() . n) \/ { ([o,F₅(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p) where o is Symbol of F₂(), p is Element of (F₁() . n) * : ex q being FinSequence of FinTrees [:the carrier of F₂(),F₃():] st
( p = q & o ==> pr1 (roots q) ) } by A3;
consider X being Subset of (FinTrees [:the carrier of F₂(),F₃():]) such that
A6: ( X = Union F₁() & ( for d being Symbol of F₂() st d in Terminals F₂() holds
root-tree [d,F₄(d)] in X ) & ( for o being Symbol of F₂()
for p being FinSequence of X st o ==> pr1 (roots p) holds
[o,F₅(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p in X ) & ( for F being Subset of (FinTrees [:the carrier of F₂(),F₃():]) st ( for d being Symbol of F₂() st d in Terminals F₂() holds
root-tree [d,F₄(d)] in F ) & ( for o being Symbol of F₂()
for p being FinSequence of F st o ==> pr1 (roots p) holds
[o,F₅(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p in F ) holds
X c= F ) ) from DTCONSTR:sch 3(A1, A4, A5);
set X' = { (t `1 ) where t is Element of FinTrees [:the carrier of F<sub>2</sub>(),F<sub>3</sub>():] : t in Union F<sub>1</sub>() } ;
{ (t `1 ) where t is Element of FinTrees [:the carrier of F₂(),F₃():] : t in Union F₁() } c= FinTrees the carrier of F₂()

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { (t `1 ) where t is Element of FinTrees [:the carrier of F<sub>2</sub>(),F<sub>3</sub>():] : t in Union F<sub>1</sub>() } or x in FinTrees the carrier of F<sub>2</sub>() )
assume x in { (t `1 ) where t is Element of FinTrees [:the carrier of F₂(),F₃():] : t in Union F₁() } ; :: thesis: x in FinTrees the carrier of F₂()
then consider tt being Element of FinTrees [:the carrier of F₂(),F₃():] such that
A7: ( x = tt `1 & tt in Union F<sub>1</sub>() ) ;
( tt `1 = (pr1 the carrier of F₂(),F₃()) * tt & rng tt c= [:the carrier of F₂(),F₃():] & dom (pr1 the carrier of F₂(),F₃()) = [:the carrier of F₂(),F₃():] ) by FUNCT_2:def 1, RELAT_1:def 19, TREES_3:def 12;
then ( dom (tt `1 ) = dom tt & dom tt is finite ) by RELAT_1:46;
hence x in FinTrees the carrier of F₂() by A7, TREES_3:def 8; :: thesis: verum

end;

then reconsider X' = { (t `1 ) where t is Element of FinTrees [:the carrier of F<sub>2</sub>(),F<sub>3</sub>():] : t in Union F<sub>1</sub>() } as Subset of (FinTrees the carrier of F<sub>2</sub>()) ;
take X1 = X'; :: thesis: ( X1 = { (t `1 ) where t is Element of FinTrees [:the carrier of F₂(),F₃():] : t in Union F₁() } & ( for d being Symbol of F₂() st d in Terminals F₂() holds
root-tree d in X1 ) & ( for o being Symbol of F₂()
for p being FinSequence of X1 st o ==> roots p holds
o -tree p in X1 ) & ( for F being Subset of (FinTrees the carrier of F₂()) st ( for d being Symbol of F₂() st d in Terminals F₂() holds
root-tree d in F ) & ( for o being Symbol of F₂()
for p being FinSequence of F st o ==> roots p holds
o -tree p in F ) holds
X1 c= F ) )
thus X1 = { (t `1 ) where t is Element of FinTrees [:the carrier of F₂(),F₃():] : t in Union F₁() } ; :: thesis: ( ( for d being Symbol of F₂() st d in Terminals F₂() holds
root-tree d in X1 ) & ( for o being Symbol of F₂()
for p being FinSequence of X1 st o ==> roots p holds
o -tree p in X1 ) & ( for F being Subset of (FinTrees the carrier of F₂()) st ( for d being Symbol of F₂() st d in Terminals F₂() holds
root-tree d in F ) & ( for o being Symbol of F₂()
for p being FinSequence of F st o ==> roots p holds
o -tree p in F ) holds
X1 c= F ) )

hereby :: thesis: ( ( for o being Symbol of F₂()
for p being FinSequence of X1 st o ==> roots p holds
o -tree p in X1 ) & ( for F being Subset of (FinTrees the carrier of F₂()) st ( for d being Symbol of F₂() st d in Terminals F₂() holds
root-tree d in F ) & ( for o being Symbol of F₂()
for p being FinSequence of F st o ==> roots p holds
o -tree p in F ) holds
X1 c= F ) )

let t be Symbol of F₂(); :: thesis: ( t in Terminals F₂() implies root-tree t in X1 )
assume A8: t in Terminals F₂() ; :: thesis: root-tree t in X1
A9: (root-tree [t,F₄(t)]) `1 = root-tree t by TREES_4:25;
root-tree [t,F₄(t)] in Union F₁() by A6, A8;
hence root-tree t in X1 by A9; :: thesis: verum

end;

hereby :: thesis: for F being Subset of (FinTrees the carrier of F₂()) st ( for d being Symbol of F₂() st d in Terminals F₂() holds
root-tree d in F ) & ( for o being Symbol of F₂()
for p being FinSequence of F st o ==> roots p holds
o -tree p in F ) holds
X1 c= F

let nt be Symbol of F₂(); :: thesis: for ts being FinSequence of X1 st nt ==> roots ts holds
nt -tree ts in X1
let ts be FinSequence of X1; :: thesis: ( nt ==> roots ts implies nt -tree ts in X1 )
assume A10: nt ==> roots ts ; :: thesis: nt -tree ts in X1
A11: dom ts = Seg (len ts) by FINSEQ_1:def 3;
defpred S₁[ set , set ] means ex dt being DecoratedTree of st
( dt = $2 & dt `1 = ts . $1 & dt in Union F₁() );
A12: for k being Nat st k in Seg (len ts) holds
ex x being Element of FinTrees [:the carrier of F₂(),F₃():] st S₁[k,x]

proof

let k be Nat; :: thesis: ( k in Seg (len ts) implies ex x being Element of FinTrees [:the carrier of F₂(),F₃():] st S₁[k,x] )
assume k in Seg (len ts) ; :: thesis: ex x being Element of FinTrees [:the carrier of F₂(),F₃():] st S₁[k,x]
then ( ts . k in rng ts & rng ts c= X1 ) by A11, FINSEQ_1:def 4, FUNCT_1:def 5;
then ts . k in X1 ;
then ex x being Element of FinTrees [:the carrier of F₂(),F₃():] st
( ts . k = x `1 & x in Union F₁() ) ;
hence ex x being Element of FinTrees [:the carrier of F₂(),F₃():] st S₁[k,x] ; :: thesis: verum

end;

consider dts being FinSequence of FinTrees [:the carrier of F₂(),F₃():] such that
A13: dom dts = Seg (len ts) and
A14: for k being Nat st k in Seg (len ts) holds
S₁[k,dts . k] from FINSEQ_1:sch 5(A12);
rng dts c= Union F₁()

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng dts or x in Union F₁() )
assume x in rng dts ; :: thesis: x in Union F₁()
then consider k being set such that
A15: ( k in dom ts & x = dts . k ) by A11, A13, FUNCT_1:def 5;
reconsider k = k as Element of NAT by A15;
ex dt being DecoratedTree of st
( dt = x & dt `1 = ts . k & dt in Union F₁() ) by A11, A14, A15;
hence x in Union F₁() ; :: thesis: verum

end;

then reconsider dts = dts as FinSequence of X by A6, FINSEQ_1:def 4;
A16: dom (roots ts) = dom ts by TREES_3:def 18;
A17: ( dom (pr1 (roots dts)) = dom (roots dts) & dom (pr2 (roots dts)) = dom (roots dts) ) by MCART_1:def 12, MCART_1:def 13;
then A18: ( dom (pr1 (roots dts)) = dom ts & dom (pr2 (roots dts)) = dom ts ) by A11, A13, TREES_3:def 18;

now

let k be Nat; :: thesis: ( k in dom ts implies (roots ts) . k = (pr1 (roots dts)) . k )
assume A19: k in dom ts ; :: thesis: (roots ts) . k = (pr1 (roots dts)) . k
then consider dt being DecoratedTree of such that
A20: ( dt = dts . k & dt `1 = ts . k & dt in Union F<sub>1</sub>() ) by A11, A14;
reconsider r = {} as Node of dt by TREES_1:47;
ex T being DecoratedTree st
( T = ts . k & (roots ts) . k = T . {} ) by A19, TREES_3:def 18;
then A21: (roots ts) . k = (dt . r) `1 by A20, TREES_3:41;
ex T being DecoratedTree st
( T = dts . k & (roots dts) . k = T . {} ) by A11, A13, A19, TREES_3:def 18;
hence (roots ts) . k = (pr1 (roots dts)) . k by A17, A18, A19, A20, A21, MCART_1:def 12; :: thesis: verum

end;

then roots ts = pr1 (roots dts) by A16, A18, FINSEQ_1:17;
then A22: [nt,H₃(nt,dts)] -tree dts in X by A6, A10;
A23: rng dts c= FinTrees [:the carrier of F₂(),F₃():] by FINSEQ_1:def 4;
FinTrees [:the carrier of F₂(),F₃():] c= Trees [:the carrier of F₂(),F₃():] by TREES_3:22;
then rng dts c= Trees [:the carrier of F₂(),F₃():] by A23, XBOOLE_1:1;
then reconsider dts' = dts as FinSequence of Trees [:the carrier of F₂(),F₃():] by FINSEQ_1:def 4;
A24: rng ts c= FinTrees the carrier of F₂() by FINSEQ_1:def 4;
FinTrees the carrier of F₂() c= Trees the carrier of F₂() by TREES_3:22;
then rng ts c= Trees the carrier of F₂() by A24, XBOOLE_1:1;
then reconsider ts' = ts as FinSequence of Trees the carrier of F₂() by FINSEQ_1:def 4;

now

let i be Element of NAT ; :: thesis: ( i in dom dts implies for T being DecoratedTree of st T = dts . i holds
ts . i = T `1 )
assume i in dom dts ; :: thesis: for T being DecoratedTree of st T = dts . i holds
ts . i = T `1
then consider dt being DecoratedTree of such that
A25: ( dt = dts . i & dt `1 = ts . i & dt in Union F<sub>1</sub>() ) by A13, A14;
let T be DecoratedTree of ; :: thesis: ( T = dts . i implies ts . i = T `1 )
assume T = dts . i ; :: thesis: ts . i = T `1
hence ts . i = T `1 by A25; :: thesis: verum

end;

then ([nt,H₃(nt,dts)] -tree dts') `1 = nt -tree ts' by A11, A13, TREES_4:27;
hence nt -tree ts in X1 by A6, A22; :: thesis: verum

end;

let F be Subset of (FinTrees the carrier of F₂()); :: thesis: ( ( for d being Symbol of F₂() st d in Terminals F₂() holds
root-tree d in F ) & ( for o being Symbol of F₂()
for p being FinSequence of F st o ==> roots p holds
o -tree p in F ) implies X1 c= F )
assume that
A26: for d being Symbol of F₂() st d in Terminals F₂() holds
root-tree d in F and
A27: for o being Symbol of F₂()
for p being FinSequence of F st o ==> roots p holds
o -tree p in F ; :: thesis: X1 c= F
thus X1 c= F :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X1 or x in F )
assume x in X1 ; :: thesis: x in F
then consider tt being Element of FinTrees [:the carrier of F₂(),F₃():] such that
A28: ( x = tt `1 & tt in Union F<sub>1</sub>() ) ;
set FF = { dt where dt is Element of FinTrees [:the carrier of F<sub>2</sub>(),F<sub>3</sub>():] : dt `1 in F } ;
{ dt where dt is Element of FinTrees [:the carrier of F₂(),F₃():] : dt `1 in F } c= FinTrees [:the carrier of F₂(),F₃():]

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { dt where dt is Element of FinTrees [:the carrier of F₂(),F₃():] : dt `1 in F } or x in FinTrees [:the carrier of F<sub>2</sub>(),F<sub>3</sub>():] )
assume x in { dt where dt is Element of FinTrees [:the carrier of F<sub>2</sub>(),F<sub>3</sub>():] : dt `1 in F } ; :: thesis: x in FinTrees [:the carrier of F₂(),F₃():]
then ex dt being Element of FinTrees [:the carrier of F₂(),F₃():] st
( x = dt & dt `1 in F ) ;
hence x in FinTrees [:the carrier of F₂(),F₃():] ; :: thesis: verum

end;

then reconsider FF = { dt where dt is Element of FinTrees [:the carrier of F₂(),F₃():] : dt `1 in F } as Subset of (FinTrees [:the carrier of F₂(),F₃():]) ;

A29: now

let d be Symbol of F₂(); :: thesis: ( d in Terminals F₂() implies root-tree [d,F₄(d)] in FF )
assume d in Terminals F₂() ; :: thesis: root-tree [d,F₄(d)] in FF
then A30: root-tree d in F by A26;
(root-tree [d,F₄(d)]) `1 = root-tree d by TREES_4:25;
hence root-tree [d,F₄(d)] in FF by A30; :: thesis: verum

end;

now

let o be Symbol of F₂(); :: thesis: for p being FinSequence of FF st o ==> pr1 (roots p) holds
[o,H₃(o,p)] -tree p in FF
let p be FinSequence of FF; :: thesis: ( o ==> pr1 (roots p) implies [o,H₃(o,p)] -tree p in FF )
assume A31: o ==> pr1 (roots p) ; :: thesis: [o,H₃(o,p)] -tree p in FF
consider p1 being FinSequence of FinTrees the carrier of F₂() such that
A32: dom p1 = dom p and
A33: for i being Element of NAT st i in dom p holds
ex T being Element of FinTrees [:the carrier of F₂(),F₃():] st
( T = p . i & p1 . i = T `1 ) and
A34: ([o,F<sub>5</sub>(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p) `1 = o -tree p1 by TREES_4:31;
rng p1 c= F

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng p1 or x in F )
assume x in rng p1 ; :: thesis: x in F
then consider k being set such that
A35: ( k in dom p1 & x = p1 . k ) by FUNCT_1:def 5;
reconsider k = k as Element of NAT by A35;
A36: p . k in rng p by A32, A35, FUNCT_1:def 5;
consider dt being Element of FinTrees [:the carrier of F₂(),F₃():] such that
A37: ( dt = p . k & x = dt `1 ) by A32, A33, A35;
rng p c= FF by FINSEQ_1:def 4;
then p . k in FF by A36;
then ex dt being Element of FinTrees [:the carrier of F<sub>2</sub>(),F<sub>3</sub>():] st
( p . k = dt & dt `1 in F ) ;
hence x in F by A37; :: thesis: verum

end;

then reconsider p1 = p1 as FinSequence of F by FINSEQ_1:def 4;
A38: dom (roots p1) = dom p1 by TREES_3:def 18;
A39: dom (pr1 (roots p)) = dom (roots p) by MCART_1:def 12;
then A40: dom (pr1 (roots p)) = dom p1 by A32, TREES_3:def 18;

now

let k be Nat; :: thesis: ( k in dom p1 implies (roots p1) . k = (pr1 (roots p)) . k )
assume A41: k in dom p1 ; :: thesis: (roots p1) . k = (pr1 (roots p)) . k
then A42: p . k in rng p by A32, FUNCT_1:def 5;
consider dt being Element of FinTrees [:the carrier of F₂(),F₃():] such that
A43: ( dt = p . k & p1 . k = dt `1 ) by A32, A33, A41;
rng p c= FF by FINSEQ_1:def 4;
then p . k in FF by A42;
then consider dt being Element of FinTrees [:the carrier of F<sub>2</sub>(),F<sub>3</sub>():] such that
A44: ( p . k = dt & dt `1 in F ) ;
reconsider r = {} as Node of dt by TREES_1:47;
ex T being DecoratedTree st
( T = p1 . k & (roots p1) . k = T . {} ) by A41, TREES_3:def 18;
then A45: (roots p1) . k = (dt . r) `1 by A43, A44, TREES_3:41;
ex T being DecoratedTree st
( T = p . k & (roots p) . k = T . {} ) by A32, A41, TREES_3:def 18;
hence (roots p1) . k = (pr1 (roots p)) . k by A39, A40, A41, A44, A45, MCART_1:def 12; :: thesis: verum

end;

then pr1 (roots p) = roots p1 by A38, A40, FINSEQ_1:17;
then ([o,F₅(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p) `1 in F by A27, A31, A34;
hence [o,H₃(o,p)] -tree p in FF ; :: thesis: verum

end;

then X c= FF by A6, A29;
then tt in FF by A6, A28;
then ex dt being Element of FinTrees [:the carrier of F₂(),F₃():] st
( tt = dt & dt `1 in F ) ;
hence x in F by A28; :: thesis: verum

end;