set f = F₁();
set G = F₂();
set D = F₃();
deffunc H₃( Symbol of F₂(), FinSequence) -> Element of F₃() = F₅($1,(pr1 (roots $2)),(pr2 (roots $2)));
Union F₁() c= FinTrees [: the carrier of F₂(),F₃():]

proof

let u be object ; :: according to TARSKI:def 3 :: thesis:
assume u in Union F₁() ; :: thesis:
then A4: ex k being object st
( k in NAT & u in F₁() . k ) by A1, CARD_5:2;
defpred S₁[ Nat] means for u being set st u in F₁() . $1 holds
u in FinTrees [: the carrier of F₂(),F₃():];
A5: S₁[ 0 ]

proof

let u be set ; :: thesis:
assume u in F₁() . 0 ; :: thesis:
then ex t being Symbol of F₂() ex d being Element of F₃() st
( u = root-tree [t,d] & ( ( t in Terminals F₂() & d = F₄(t) ) or ( t ==> {} & d = F₅(t,{},{}) ) ) ) by A2;
hence u in FinTrees [: the carrier of F₂(),F₃():] ; :: thesis:

end;

A6: now :: thesis:

let n be Nat; :: thesis:
assume A7: S₁[n] ; :: thesis:
thus S₁[n + 1] :: thesis:

proof

let u be set ; :: thesis:
assume u in F₁() . (n + 1) ; :: thesis:
then u in (F₁() . n) \/ { ([o,H₃(o,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;
then A8: ( u in F₁() . n or u in { ([o,H₃(o,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 XBOOLE_0:def 3;
assume A9: not u in FinTrees [: the carrier of F₂(),F₃():] ; :: thesis:
then consider o being Symbol of F₂(), p being Element of (F₁() . n) * such that
A10: u = [o,H₃(o,p)] -tree p and
A11: ex q being FinSequence of FinTrees [: the carrier of F₂(),F₃():] st
( p = q & o ==> pr1 (roots q) ) by A7, A8;
reconsider p = p as FinSequence of FinTrees [: the carrier of F₂(),F₃():] by A11;
u = [o,H₃(o,p)] -tree p by A10;
hence contradiction by A9; :: thesis:

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A5, A6);
hence u in FinTrees [: the carrier of F₂(),F₃():] by A4; :: thesis:

end;

then reconsider X = Union F₁() as Subset of (FinTrees [: the carrier of F₂(),F₃():]) ;
take X ; :: thesis:
thus X = Union F₁() ; :: thesis:

hereby :: thesis:

let d be Symbol of F₂(); :: thesis:
assume d in Terminals F₂() ; :: thesis:
then root-tree [d,F₄(d)] in F₁() . 0 by A2;
hence root-tree [d,F₄(d)] in X by A1, CARD_5:2; :: thesis:

end;

hereby :: thesis:

let o be Symbol of F₂(); :: thesis:
let p be FinSequence of X; :: thesis:
assume A12: o ==> pr1 (roots p) ; :: thesis:
set s = pr1 (roots p);
set v = pr2 (roots p);
A13: dom p = Seg (len p) by FINSEQ_1:def 3;
defpred S₁[ set , set ] means p . $1 in F₁() . $2;
A14: for x being Nat st x in Seg (len p) holds
ex n being Element of NAT st S₁[x,n]

proof

let x be Nat; :: thesis:
assume x in Seg (len p) ; :: thesis:
then A15: p . x in rng p by A13, FUNCT_1:def 3;
rng p c= X by FINSEQ_1:def 4;
then ex n being object st
( n in NAT & p . x in F₁() . n ) by A1, A15, CARD_5:2;
hence ex n being Element of NAT st S₁[x,n] ; :: thesis:

end;

consider pn being FinSequence of NAT such that
A16: ( dom pn = Seg (len p) & ( for k being Nat st k in Seg (len p) holds
S₁[k,pn . k] ) ) from FINSEQ_1:sch 5(A14);

A17: now :: thesis:

defpred S₂[ Element of NAT , Element of NAT ] means $1 >= $2;
assume rng pn <> {} ; :: thesis:
then A18: ( rng pn is finite & rng pn <> {} & rng pn c= NAT ) by FINSEQ_1:def 4;
A19: for x, y being Element of NAT holds
( S₂[x,y] or S₂[y,x] ) ;
A20: for x, y, z being Element of NAT st S₂[x,y] & S₂[y,z] holds
S₂[x,z] by XXREAL_0:2;
consider n being Element of NAT such that
A21: ( n in rng pn & ( for y being Element of NAT st y in rng pn holds
S₂[n,y] ) ) from CQC_SIM1:sch 4(A18, A19, A20);
take n = n; :: thesis:
thus rng p c= F₁() . n :: thesis:

proof

let t be object ; :: according to TARSKI:def 3 :: thesis:
assume t in rng p ; :: thesis:
then consider k being object such that
A22: k in dom p and
A23: t = p . k by FUNCT_1:def 3;
reconsider k = k as Element of NAT by A22;
A24: pn . k in rng pn by A13, A16, A22, FUNCT_1:def 3;
then reconsider pnk = pn . k as Element of NAT by A18;
consider s being Nat such that
A25: n = pnk + s by A21, A24, NAT_1:10;
deffunc H₄( set , set ) -> set = { ([o1,F₅(o1,(pr1 (roots p1)),(pr2 (roots p1)))] -tree p1) where o1 is Symbol of F₂(), p1 is Element of (F₁() . $1) * : ex q being FinSequence of FinTrees [: the carrier of F₂(),F₃():] st
( p1 = q & o1 ==> pr1 (roots q) ) } ;
for n being Nat holds F₁() . n c= F₁() . (n + 1)

proof

let n be Nat; :: thesis:
F₁() . (n + 1) = (F₁() . n) \/ H₄(n,F₁() . n) by A3;
hence F₁() . n c= F₁() . (n + 1) by XBOOLE_1:7; :: thesis:

end;

then A26: F₁() . pnk c= F₁() . n by A25, MEASURE2:18, NAT_1:11;
t in F₁() . (pn . k) by A13, A16, A22, A23;
hence t in F₁() . n by A26; :: thesis:

end;

now :: thesis:

assume rng pn = {} ; :: thesis:
then pn = {} ;
then p = {} by A16;
then rng p = {} ;
hence rng p c= F₁() . 0 ; :: thesis:

end;

then consider n being Element of NAT such that
A27: rng p c= F₁() . n by A17;
A28: X = union (rng F₁()) by CARD_3:def 4;
F₁() . n in rng F₁() by A1, FUNCT_1:def 3;
then F₁() . n c= X by A28, ZFMISC_1:74;
then reconsider fn = F₁() . n as Subset of (FinTrees [: the carrier of F₂(),F₃():]) by XBOOLE_1:1;
reconsider q = p as FinSequence of fn by A27, FINSEQ_1:def 4;
reconsider q9 = q as Element of fn * by FINSEQ_1:def 11;
[o,F₅(o,(pr1 (roots p)),(pr2 (roots p)))] -tree q9 in { ([oo,H₃(oo,pp)] -tree pp) where oo is Symbol of F₂(), pp is Element of fn * : ex q being FinSequence of FinTrees [: the carrier of F₂(),F₃():] st
( pp = q & oo ==> pr1 (roots q) ) } by A12;
then [o,F₅(o,(pr1 (roots p)),(pr2 (roots p)))] -tree q9 in (F₁() . n) \/ { ([oo,H₃(oo,pp)] -tree pp) where oo is Symbol of F₂(), pp is Element of fn * : ex q being FinSequence of FinTrees [: the carrier of F₂(),F₃():] st
( pp = q & oo ==> pr1 (roots q) ) } by XBOOLE_0:def 3;
then [o,F₅(o,(pr1 (roots p)),(pr2 (roots p)))] -tree q9 in F₁() . (n + 1) by A3;
hence [o,F₅(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p in X by A1, CARD_5:2; :: thesis:

end;

let F be Subset of (FinTrees [: the carrier of F₂(),F₃():]); :: thesis:
assume that
A29: for d being Symbol of F₂() st d in Terminals F₂() holds
root-tree [d,F₄(d)] in F and
A30: for o being Symbol of F₂()
for p being FinSequence of F st o ==> pr1 (roots p) holds
[o,H₃(o,p)] -tree p in F ; :: thesis:
defpred S₁[ Nat] means F₁() . $1 c= F;
A31: S₁[ 0 ]

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
reconsider p = <*> F as FinSequence of F ;
assume x in F₁() . 0 ; :: thesis:
then consider t being Symbol of F₂(), d being Element of F₃() such that
A32: x = root-tree [t,d] and
A33: ( ( t in Terminals F₂() & d = F₄(t) ) or ( t ==> pr1 (roots p) & d = H₃(t,p) ) ) by A2, Th3, Th7;
[t,d] -tree p = root-tree [t,d] by TREES_4:20;
hence x in F by A29, A30, A32, A33; :: thesis:

end;

A34: now :: thesis:

let n be Nat; :: thesis:
assume A35: S₁[n] ; :: thesis:
thus S₁[n + 1] :: thesis:

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume that
A36: x in F₁() . (n + 1) and
A37: not x in F ; :: thesis:
x in (F₁() . n) \/ { ([oo,H₃(oo,pp)] -tree pp) where oo is Symbol of F₂(), pp is Element of (F₁() . n) * : ex q being FinSequence of FinTrees [: the carrier of F₂(),F₃():] st
( pp = q & oo ==> pr1 (roots q) ) } by A3, A36;
then ( x in F₁() . n or x in { ([oo,H₃(oo,pp)] -tree pp) where oo is Symbol of F₂(), pp is Element of (F₁() . n) * : ex q being FinSequence of FinTrees [: the carrier of F₂(),F₃():] st
( pp = q & oo ==> pr1 (roots q) ) } ) by XBOOLE_0:def 3;
then consider o being Symbol of F₂(), p being Element of (F₁() . n) * such that
A38: x = [o,H₃(o,p)] -tree p and
A39: ex q being FinSequence of FinTrees [: the carrier of F₂(),F₃():] st
( p = q & o ==> pr1 (roots q) ) by A35, A37;
rng p c= F₁() . n by FINSEQ_1:def 4;
then rng p c= F by A35, XBOOLE_1:1;
then reconsider p = p as FinSequence of F by FINSEQ_1:def 4;
o ==> pr1 (roots p) by A39;
hence contradiction by A30, A37, A38; :: thesis:

end;

A40: for n being Nat holds S₁[n] from NAT_1:sch 2(A31, A34);
thus X c= F :: thesis:

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in X ; :: thesis:
then consider n being object such that
A41: n in NAT and
A42: x in F₁() . n by A1, CARD_5:2;
F₁() . n c= F by A40, A41;
hence x in F by A42; :: thesis:

end;