set f = F1();
set G = F2();
set D = F3();
deffunc H3( Symbol of F2(), FinSequence) -> Element of F3() = F5($1,(pr1 (roots $2)),(pr2 (roots $2)));
Union F1() c= FinTrees [: the carrier of F2(),F3():]
proof
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in Union F1() or u in FinTrees [: the carrier of F2(),F3():] )
assume u in Union F1() ; :: thesis: u in FinTrees [: the carrier of F2(),F3():]
then A4: ex k being object st
( k in NAT & u in F1() . k ) by A1, CARD_5:2;
defpred S1[ Nat] means for u being set st u in F1() . $1 holds
u in FinTrees [: the carrier of F2(),F3():];
A5: S1[ 0 ]
proof
let u be set ; :: thesis: ( u in F1() . 0 implies u in FinTrees [: the carrier of F2(),F3():] )
assume u in F1() . 0 ; :: thesis: u in FinTrees [: the carrier of F2(),F3():]
then ex t being Symbol of F2() ex d being Element of F3() st
( u = root-tree [t,d] & ( ( t in Terminals F2() & d = F4(t) ) or ( t ==> {} & d = F5(t,{},{}) ) ) ) by A2;
hence u in FinTrees [: the carrier of F2(),F3():] ; :: thesis: verum
end;
A6: 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 A7: S1[n] ; :: thesis: S1[n + 1]
thus S1[n + 1] :: thesis: verum
proof
let u be set ; :: thesis: ( u in F1() . (n + 1) implies u in FinTrees [: the carrier of F2(),F3():] )
assume u in F1() . (n + 1) ; :: thesis: u in FinTrees [: the carrier of F2(),F3():]
then u in (F1() . n) \/ { ([o,H3(o,p)] -tree p) where o is Symbol of F2(), p is Element of (F1() . n) * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st
( p = q & o ==> pr1 (roots q) ) } by A3;
then A8: ( u in F1() . n or u in { ([o,H3(o,p)] -tree p) where o is Symbol of F2(), p is Element of (F1() . n) * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st
( p = q & o ==> pr1 (roots q) ) } ) by XBOOLE_0:def 3;
assume A9: not u in FinTrees [: the carrier of F2(),F3():] ; :: thesis: contradiction
then consider o being Symbol of F2(), p being Element of (F1() . n) * such that
A10: u = [o,H3(o,p)] -tree p and
A11: ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st
( p = q & o ==> pr1 (roots q) ) by A7, A8;
reconsider p = p as FinSequence of FinTrees [: the carrier of F2(),F3():] by A11;
u = [o,H3(o,p)] -tree p by A10;
hence contradiction by A9; :: thesis: verum
end;
end;
for n being Nat holds S1[n] from NAT_1:sch 2(A5, A6);
 hence u in FinTrees [: the carrier of F2(),F3():] by A4; :: thesis: verum
end;
then reconsider X = Union F1() as Subset of (FinTrees [: the carrier of F2(),F3():]) ;
take X ; :: thesis: ( X = Union F1() & ( for d being Symbol of F2() st d in Terminals F2() holds
root-tree [d,F4(d)] in X ) & ( for o being Symbol of F2()
for p being FinSequence of X st o ==> pr1 (roots p) holds
[o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p in X ) & ( for F being Subset of (FinTrees [: the carrier of F2(),F3():]) st ( for d being Symbol of F2() st d in Terminals F2() holds
root-tree [d,F4(d)] in F ) & ( for o being Symbol of F2()
for p being FinSequence of F st o ==> pr1 (roots p) holds
[o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p in F ) holds
X c= F ) )
thus X = Union F1() ; :: thesis: ( ( for d being Symbol of F2() st d in Terminals F2() holds
root-tree [d,F4(d)] in X ) & ( for o being Symbol of F2()
for p being FinSequence of X st o ==> pr1 (roots p) holds
[o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p in X ) & ( for F being Subset of (FinTrees [: the carrier of F2(),F3():]) st ( for d being Symbol of F2() st d in Terminals F2() holds
root-tree [d,F4(d)] in F ) & ( for o being Symbol of F2()
for p being FinSequence of F st o ==> pr1 (roots p) holds
[o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p in F ) holds
X c= F ) )
hereby :: thesis: ( ( for o being Symbol of F2()
for p being FinSequence of X st o ==> pr1 (roots p) holds
[o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p in X ) & ( for F being Subset of (FinTrees [: the carrier of F2(),F3():]) st ( for d being Symbol of F2() st d in Terminals F2() holds
root-tree [d,F4(d)] in F ) & ( for o being Symbol of F2()
for p being FinSequence of F st o ==> pr1 (roots p) holds
[o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p in F ) holds
X c= F ) )
let d be Symbol of F2(); :: thesis: ( d in Terminals F2() implies root-tree [d,F4(d)] in X )
assume d in Terminals F2() ; :: thesis: root-tree [d,F4(d)] in X
then root-tree [d,F4(d)] in F1() . 0 by A2;
hence root-tree [d,F4(d)] in X by A1, CARD_5:2; :: thesis: verum
end;
hereby :: thesis: for F being Subset of (FinTrees [: the carrier of F2(),F3():]) st ( for d being Symbol of F2() st d in Terminals F2() holds
root-tree [d,F4(d)] in F ) & ( for o being Symbol of F2()
for p being FinSequence of F st o ==> pr1 (roots p) holds
[o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p in F ) holds
X c= F
let o be Symbol of F2(); :: thesis: for p being FinSequence of X st o ==> pr1 (roots p) holds
[o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p in X
let p be FinSequence of X; :: thesis: ( o ==> pr1 (roots p) implies [o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p in X )
assume A12: o ==> pr1 (roots p) ; :: thesis: [o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p in X
set s = pr1 (roots p);
set v = pr2 (roots p);
A13: dom p = Seg (len p) by FINSEQ_1:def 3;
defpred S1[ set , set ] means p . $1 in F1() . $2;
A14: for x being Nat st x in Seg (len p) holds
ex n being Element of NAT st S1[x,n]
proof
let x be Nat; :: thesis: ( x in Seg (len p) implies ex n being Element of NAT st S1[x,n] )
assume x in Seg (len p) ; :: thesis: ex n being Element of NAT st S1[x,n]
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 F1() . n ) by A1, A15, CARD_5:2;
hence ex n being Element of NAT st S1[x,n] ; :: thesis: verum
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
S1[k,pn . k] ) ) from FINSEQ_1:sch 5(A14);
A17: now :: thesis: ( rng pn <> {} implies ex n being Element of NAT st rng p c= F1() . n )
defpred S2[ Element of NAT , Element of NAT ] means $1 >= $2;
assume rng pn <> {} ; :: thesis: ex n being Element of NAT st rng p c= F1() . n
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
( S2[x,y] or S2[y,x] ) ;
A20: for x, y, z being Element of NAT st S2[x,y] & S2[y,z] holds
S2[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
S2[n,y] ) ) from CQC_SIM1:sch 4(A18, A19, A20);
take n = n; :: thesis: rng p c= F1() . n
thus rng p c= F1() . n :: thesis: verum
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in rng p or t in F1() . n )
assume t in rng p ; :: thesis: t in F1() . n
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 H4( set , set ) -> set = { ([o1,F5(o1,(pr1 (roots p1)),(pr2 (roots p1)))] -tree p1) where o1 is Symbol of F2(), p1 is Element of (F1() . $1) * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st
( p1 = q & o1 ==> pr1 (roots q) ) } ;
for n being Nat holds F1() . n c= F1() . (n + 1)
proof
let n be Nat; :: thesis: F1() . n c= F1() . (n + 1)
F1() . (n + 1) = (F1() . n) \/ H4(n,F1() . n) by A3;
hence F1() . n c= F1() . (n + 1) by XBOOLE_1:7; :: thesis: verum
end;
then A26: F1() . pnk c= F1() . n by A25, MEASURE2:18, NAT_1:11;
t in F1() . (pn . k) by A13, A16, A22, A23;
hence t in F1() . n by A26; :: thesis: verum
end;
end;
now :: thesis: ( rng pn = {} implies rng p c= F1() . 0 )
assume rng pn = {} ; :: thesis: rng p c= F1() . 0
then pn = {} ;
then p = {} by A16;
then rng p = {} ;
hence rng p c= F1() . 0 ; :: thesis: verum
end;
then consider n being Element of NAT such that
A27: rng p c= F1() . n by A17;
A28: X = union (rng F1()) by CARD_3:def 4;
F1() . n in rng F1() by A1, FUNCT_1:def 3;
then F1() . n c= X by A28, ZFMISC_1:74;
then reconsider fn = F1() . n as Subset of (FinTrees [: the carrier of F2(),F3():]) 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,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree q9 in { ([oo,H3(oo,pp)] -tree pp) where oo is Symbol of F2(), pp is Element of fn * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st
( pp = q & oo ==> pr1 (roots q) ) } by A12;
then [o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree q9 in (F1() . n) \/ { ([oo,H3(oo,pp)] -tree pp) where oo is Symbol of F2(), pp is Element of fn * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st
( pp = q & oo ==> pr1 (roots q) ) } by XBOOLE_0:def 3;
then [o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree q9 in F1() . (n + 1) by A3;
hence [o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p in X by A1, CARD_5:2; :: thesis: verum
end;
let F be Subset of (FinTrees [: the carrier of F2(),F3():]); :: thesis: ( ( for d being Symbol of F2() st d in Terminals F2() holds
root-tree [d,F4(d)] in F ) & ( for o being Symbol of F2()
for p being FinSequence of F st o ==> pr1 (roots p) holds
[o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p in F ) implies X c= F )
assume that
A29: for d being Symbol of F2() st d in Terminals F2() holds
root-tree [d,F4(d)] in F and
A30: for o being Symbol of F2()
for p being FinSequence of F st o ==> pr1 (roots p) holds
[o,H3(o,p)] -tree p in F ; :: thesis: X c= F
defpred S1[ Nat] means F1() . $1 c= F;
A31: S1[ 0 ]
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in F1() . 0 or x in F )
reconsider p = <*> F as FinSequence of F ;
assume x in F1() . 0 ; :: thesis: x in F
then consider t being Symbol of F2(), d being Element of F3() such that
A32: x = root-tree [t,d] and
A33: ( ( t in Terminals F2() & d = F4(t) ) or ( t ==> pr1 (roots p) & d = H3(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: verum
end;
A34: 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 A35: S1[n] ; :: thesis: S1[n + 1]
thus S1[n + 1] :: thesis: verum
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in F1() . (n + 1) or x in F )
assume that
A36: x in F1() . (n + 1) and
A37: not x in F ; :: thesis: contradiction
x in (F1() . n) \/ { ([oo,H3(oo,pp)] -tree pp) where oo is Symbol of F2(), pp is Element of (F1() . n) * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st
( pp = q & oo ==> pr1 (roots q) ) } by A3, A36;
then ( x in F1() . n or x in { ([oo,H3(oo,pp)] -tree pp) where oo is Symbol of F2(), pp is Element of (F1() . n) * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st
( pp = q & oo ==> pr1 (roots q) ) } ) by XBOOLE_0:def 3;
then consider o being Symbol of F2(), p being Element of (F1() . n) * such that
A38: x = [o,H3(o,p)] -tree p and
A39: ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st
( p = q & o ==> pr1 (roots q) ) by A35, A37;
rng p c= F1() . 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: verum
end;
end;
A40: for n being Nat holds S1[n] from NAT_1:sch 2(A31, A34);
 thus X c= F :: thesis: verum
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in F )
assume x in X ; :: thesis: x in F
then consider n being object such that
A41: n in NAT and
A42: x in F1() . n by A1, CARD_5:2;
F1() . n c= F by A40, A41;
hence x in F by A42; :: thesis: verum
end;