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 set ; :: according to TARSKI:def 3 :: thesis:
assume u in Union F₁() ; :: thesis:
then consider k being set such that
A4: ( k in NAT & u in F₁() . k ) by A1, CARD_5:10;
defpred S₁[ Element of 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

let n be Element of 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 & 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 A10;
u = [o,H₃(o,p)] -tree p by A10;
hence contradiction by A9; :: thesis:

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(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:10; :: thesis:

end;

hereby :: thesis:

let o be Symbol of F₂(); :: thesis:
let p be FinSequence of X; :: thesis:
assume A11: o ==> pr1 (roots p) ; :: thesis:
set s = pr1 (roots p);
set v = pr2 (roots p);
A12: dom p = Seg (len p) by FINSEQ_1:def 3;
defpred S₁[ set , set ] means p . $1 in F₁() . $2;
A13: 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 ( p . x in rng p & rng p c= X ) by A12, FINSEQ_1:def 4, FUNCT_1:def 5;
then ex n being set st
( n in NAT & p . x in F₁() . n ) by A1, CARD_5:10;
hence ex n being Element of NAT st S₁[x,n] ; :: thesis:

end;

consider pn being FinSequence of NAT such that
A14: ( 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(A13);

A15: now

defpred S₂[ Element of NAT , Element of NAT ] means $1 >= $2;
assume rng pn <> {} ; :: thesis:
then A16: ( rng pn is finite & rng pn <> {} & rng pn c= NAT ) by FINSEQ_1:def 4;
A17: for x, y being Element of NAT holds
( S₂[x,y] or S₂[y,x] ) ;
A18: 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
A19: ( n in rng pn & ( for y being Element of NAT st y in rng pn holds
S₂[n,y] ) ) from CQC_SIM1:sch 4(A16, A17, A18);
take n = n; :: thesis:
thus rng p c= F₁() . n :: thesis:

proof

let t be set ; :: according to TARSKI:def 3 :: thesis:
assume t in rng p ; :: thesis:
then consider k being set such that
A20: ( k in dom p & t = p . k ) by FUNCT_1:def 5;
reconsider k = k as Element of NAT by A20;
A21: pn . k in rng pn by A12, A14, A20, FUNCT_1:def 5;
then reconsider pnk = pn . k as Element of NAT by A16;
consider s being Nat such that
A22: n = pnk + s by A19, A21, NAT_1:10;
reconsider s = s as Element of NAT by ORDINAL1:def 13;
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) ) } ;
A24: for n being Element of NAT holds F₁() . n c= F₁() . (n + 1)

proof

let n be Element of 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;

A25: F₁() . pnk c= F₁() . n by A22, A24, MEASURE2:22, NAT_1:11;
t in F₁() . (pn . k) by A12, A14, A20;
hence t in F₁() . n by A25; :: thesis:

end;

now

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

end;

then consider n being Element of NAT such that
A27: rng p c= F₁() . n by A15;
( X = union (rng F₁()) & F₁() . n in rng F₁() ) by A1, CARD_3:def 4, FUNCT_1:def 5;
then F₁() . n c= X by ZFMISC_1:92;
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 q' = q as Element of fn * by FINSEQ_1:def 11;
[o,F₅(o,(pr1 (roots p)),(pr2 (roots p)))] -tree q' 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 A11;
then [o,F₅(o,(pr1 (roots p)),(pr2 (roots p)))] -tree q' 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 q' in F₁() . (n + 1) by A3;
hence [o,F₅(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p in X by A1, CARD_5:10; :: thesis:

end;

let F be Subset of (FinTrees [:the carrier of F₂(),F₃():]); :: thesis:
assume A28: ( ( 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,H₃(o,p)] -tree p in F ) ) ; :: thesis:
defpred S₁[ Element of NAT ] means F₁() . $1 c= F;
A29: S₁[ 0 ]

proof

let x be set ; :: 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
A30: ( x = root-tree [t,d] & ( ( 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 A28, A30; :: thesis:

end;

A31: now

let n be Element of NAT ; :: thesis:
assume A32: S₁[n] ; :: thesis:
thus S₁[n + 1] :: thesis:

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A33: ( x in F₁() . (n + 1) & not x in F ) ; :: thesis:
then 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;
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
A34: ( x = [o,H₃(o,p)] -tree p & ex q being FinSequence of FinTrees [:the carrier of F₂(),F₃():] st
( p = q & o ==> pr1 (roots q) ) ) by A32, A33;
rng p c= F₁() . n by FINSEQ_1:def 4;
then rng p c= F by A32, XBOOLE_1:1;
then reconsider p = p as FinSequence of F by FINSEQ_1:def 4;
o ==> pr1 (roots p) by A34;
hence contradiction by A28, A33, A34; :: thesis:

end;

A35: for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A29, A31);
thus X c= F :: thesis:

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in X ; :: thesis:
then consider n being set such that
A36: ( n in NAT & x in F₁() . n ) by A1, CARD_5:10;
F₁() . n c= F by A35, A36;
hence x in F by A36; :: thesis:

end;