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 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 X9 = { (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 object ; :: 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 and
tt in Union F<sub>1</sub>() ;
A8: tt `1 = (pr1 ( the carrier of F₂(),F₃())) * tt by TREES_3:def 12;
A9: rng tt c= [: the carrier of F₂(),F₃():] by RELAT_1:def 19;
dom (pr1 ( the carrier of F₂(),F₃())) = [: the carrier of F₂(),F₃():] by FUNCT_2:def 1;
then dom (tt `1) = dom tt by A8, A9, RELAT_1:27;
hence x in FinTrees the carrier of F₂() by A7, TREES_3:def 8; :: thesis: verum

end;

then reconsider X9 = { (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 = X9; :: 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 A10: t in Terminals F₂() ; :: thesis: root-tree t in X1
A11: (root-tree [t,F₄(t)]) `1 = root-tree t by TREES_4:25;
root-tree [t,F₄(t)] in Union F₁() by A6, A10;
hence root-tree t in X1 by A11; :: 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 A12: nt ==> roots ts ; :: thesis: nt -tree ts in X1
A13: dom ts = Seg (len ts) by FINSEQ_1:def 3;
defpred S₁[ set , set ] means ex dt being DecoratedTree of [: the carrier of F₂(),F₃():] st
( dt = $2 & dt `1 = ts . $1 & dt in Union F₁() );
A14: 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 A15: ts . k in rng ts by A13, FUNCT_1:def 3;
rng ts c= X1 by FINSEQ_1:def 4;
then ts . k in X1 by A15;
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
A16: dom dts = Seg (len ts) and
A17: for k being Nat st k in Seg (len ts) holds
S₁[k,dts . k] from FINSEQ_1:sch 5(A14);
rng dts c= Union F₁()

proof

let x be object ; :: 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 object such that
A18: k in dom ts and
A19: x = dts . k by A13, A16, FUNCT_1:def 3;
reconsider k = k as Element of NAT by A18;
ex dt being DecoratedTree of [: the carrier of F₂(),F₃():] st
( dt = x & dt `1 = ts . k & dt in Union F₁() ) by A13, A17, A18, A19;
hence x in Union F₁() ; :: thesis: verum

end;

then reconsider dts = dts as FinSequence of X by A6, FINSEQ_1:def 4;
A20: dom (roots ts) = dom ts by TREES_3:def 18;
A21: dom (pr1 (roots dts)) = dom (roots dts) by MCART_1:def 12;
then A22: dom (pr1 (roots dts)) = dom ts by A13, A16, TREES_3:def 18;

now :: thesis: for k being Nat st k in dom ts holds
(roots ts) . k = (pr1 (roots dts)) . k

let k be Nat; :: thesis: ( k in dom ts implies (roots ts) . k = (pr1 (roots dts)) . k )
assume A23: k in dom ts ; :: thesis: (roots ts) . k = (pr1 (roots dts)) . k
then consider dt being DecoratedTree of [: the carrier of F₂(),F₃():] such that
A24: dt = dts . k and
A25: dt `1 = ts . k and
dt in Union F<sub>1</sub>() by A13, A17;
reconsider r = {} as Node of dt by TREES_1:22;
ex T being DecoratedTree st
( T = ts . k & (roots ts) . k = T . {} ) by A23, TREES_3:def 18;
then A26: (roots ts) . k = (dt . r) `1 by A25, TREES_3:39;
ex T being DecoratedTree st
( T = dts . k & (roots dts) . k = T . {} ) by A13, A16, A23, TREES_3:def 18;
hence (roots ts) . k = (pr1 (roots dts)) . k by A21, A22, A23, A24, A26, MCART_1:def 12; :: thesis: verum

end;

then roots ts = pr1 (roots dts) by A20, A22, FINSEQ_1:13;
then A27: [nt,H₃(nt,dts)] -tree dts in X by A6, A12;
A28: 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:21;
then rng dts c= Trees [: the carrier of F₂(),F₃():] by A28;
then reconsider dts9 = dts as FinSequence of Trees [: the carrier of F₂(),F₃():] by FINSEQ_1:def 4;
A29: 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:21;
then rng ts c= Trees the carrier of F₂() by A29;
then reconsider ts9 = ts as FinSequence of Trees the carrier of F₂() by FINSEQ_1:def 4;

now :: thesis: for i being Nat st i in dom dts holds
for T being DecoratedTree of [: the carrier of F₂(),F₃():] st T = dts . i holds
ts . i = T `1

let i be Nat; :: thesis: ( i in dom dts implies for T being DecoratedTree of [: the carrier of F₂(),F₃():] st T = dts . i holds
ts . i = T `1 )
assume i in dom dts ; :: thesis: for T being DecoratedTree of [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():] st T = dts . i holds
ts . i = T `1
then A30: ex dt being DecoratedTree of [: the carrier of F₂(),F₃():] st
( dt = dts . i & dt `1 = ts . i & dt in Union F<sub>1</sub>() ) by A16, A17;
let T be DecoratedTree of [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():]; :: thesis: ( T = dts . i implies ts . i = T `1 )
assume T = dts . i ; :: thesis: ts . i = T `1
hence ts . i = T `1 by A30; :: thesis: verum

end;

then ([nt,H₃(nt,dts)] -tree dts9) `1 = nt -tree ts9 by A13, A16, TREES_4:27;
hence nt -tree ts in X1 by A6, A27; :: 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
A31: for d being Symbol of F₂() st d in Terminals F₂() holds
root-tree d in F and
A32: 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 object ; :: 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
A33: x = tt `1 and
A34: 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 object ; :: 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₃():]) ;

A35: now :: thesis: for d being Symbol of F₂() st d in Terminals F₂() holds
root-tree [d,F₄(d)] in FF

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 A36: root-tree d in F by A31;
(root-tree [d,F₄(d)]) `1 = root-tree d by TREES_4:25;
hence root-tree [d,F₄(d)] in FF by A36; :: thesis: verum

end;

now :: thesis: for o being Symbol of F₂()
for p being FinSequence of FF st o ==> pr1 (roots p) holds
[o,H₃(o,p)] -tree p in FF

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 A37: 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
A38: dom p1 = dom p and
A39: for i being 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
A40: ([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 object ; :: 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 object such that
A41: k in dom p1 and
A42: x = p1 . k by FUNCT_1:def 3;
reconsider k = k as Element of NAT by A41;
A43: p . k in rng p by A38, A41, FUNCT_1:def 3;
A44: ex dt being Element of FinTrees [: the carrier of F₂(),F₃():] st
( dt = p . k & x = dt `1 ) by A38, A39, A41, A42;
rng p c= FF by FINSEQ_1:def 4;
then p . k in FF by A43;
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 A44; :: thesis: verum

end;

then reconsider p1 = p1 as FinSequence of F by FINSEQ_1:def 4;
A45: dom (roots p1) = dom p1 by TREES_3:def 18;
A46: dom (pr1 (roots p)) = dom (roots p) by MCART_1:def 12;
then A47: dom (pr1 (roots p)) = dom p1 by A38, 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 A48: k in dom p1 ; :: thesis: (roots p1) . k = (pr1 (roots p)) . k
then A49: p . k in rng p by A38, FUNCT_1:def 3;
A50: ex dt being Element of FinTrees [: the carrier of F₂(),F₃():] st
( dt = p . k & p1 . k = dt `1 ) by A38, A39, A48;
rng p c= FF by FINSEQ_1:def 4;
then p . k in FF by A49;
then consider dt being Element of FinTrees [: the carrier of F<sub>2</sub>(),F<sub>3</sub>():] such that
A51: p . k = dt and
dt `1 in F ;
reconsider r = {} as Node of dt by TREES_1:22;
ex T being DecoratedTree st
( T = p1 . k & (roots p1) . k = T . {} ) by A48, TREES_3:def 18;
then A52: (roots p1) . k = (dt . r) `1 by A50, A51, TREES_3:39;
ex T being DecoratedTree st
( T = p . k & (roots p) . k = T . {} ) by A38, A48, TREES_3:def 18;
hence (roots p1) . k = (pr1 (roots p)) . k by A46, A47, A48, A51, A52, MCART_1:def 12; :: thesis: verum

end;

then pr1 (roots p) = roots p1 by A45, A47, FINSEQ_1:13;
then ([o,F₅(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p) `1 in F by A32, A37, A40;
hence [o,H₃(o,p)] -tree p in FF ; :: thesis: verum

end;

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

end;