set f = F1();
set G = F2();
set D = F3();
set SxD = [: the carrier of F2(),F3():];
deffunc H3( Symbol of F2(), FinSequence) -> Element of F3() = F5($1,(pr1 (roots $2)),(pr2 (roots $2)));
defpred S1[ Nat] means for dt being Element of FinTrees [: the carrier of F2(),F3():] st dt in Union F1() holds
( dt in F1() . $1 iff height (dom dt) <= $1 );
A4: S1[ 0 ]
proof
let dt be Element of FinTrees [: the carrier of F2(),F3():]; :: thesis: ( dt in Union F1() implies ( dt in F1() . 0 iff height (dom dt) <= 0 ) )
assume A5: dt in Union F1() ; :: thesis: ( dt in F1() . 0 iff height (dom dt) <= 0 )
hereby :: thesis: ( height (dom dt) <= 0 implies dt in F1() . 0 )
assume dt in F1() . 0 ; :: thesis: height (dom dt) <= 0
then ex t being Symbol of F2() ex d being Element of F3() st
( dt = root-tree [t,d] & ( ( t in Terminals F2() & d = F4(t) ) or ( t ==> {} & d = F5(t,{},{}) ) ) ) by A2;
hence height (dom dt) <= 0 by TREES_1:42, TREES_4:3; :: thesis: verum
end;
assume height (dom dt) <= 0 ; :: thesis: dt in F1() . 0
then A6: height (dom dt) = 0 ;
defpred S2[ Nat] means not dt in F1() . $1;
assume A7: S2[ 0 ] ; :: thesis: contradiction
A8: now :: thesis: for n being Nat st S2[n] holds
S2[n + 1]
let n be Nat; :: thesis: ( S2[n] implies S2[n + 1] )
assume A9: S2[n] ; :: thesis: S2[n + 1]
thus S2[n + 1] :: thesis: verum
proof
assume dt in F1() . (n + 1) ; :: thesis: contradiction
then dt 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 ( dt in F1() . n or dt 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;
then consider o being Symbol of F2(), p being Element of (F1() . n) * such that
A10: dt = [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 A9;
A12: dt = root-tree (dt . {}) by A6, TREES_1:43, TREES_4:5;
then A13: p = {} by A10, A11, TREES_4:17;
then dt = root-tree [o,F5(o,{},{})] by A10, A12, Th3, Th7, TREES_4:def 4;
hence contradiction by A2, A7, A11, A13, Th3, Th7; :: thesis: verum
end;
end;
A14: for n being Nat holds S2[n] from NAT_1:sch 2(A7, A8);
 ex n being object st
( n in NAT & dt in F1() . n ) by A1, A5, CARD_5:2;
hence contradiction by A14; :: thesis: verum
end;
A15: 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 A16: S1[n] ; :: thesis: S1[n + 1]
thus S1[n + 1] :: thesis: verum
proof
let dt be Element of FinTrees [: the carrier of F2(),F3():]; :: thesis: ( dt in Union F1() implies ( dt in F1() . (n + 1) iff height (dom dt) <= n + 1 ) )
assume A17: dt in Union F1() ; :: thesis: ( dt in F1() . (n + 1) iff height (dom dt) <= n + 1 )
hereby :: thesis: ( height (dom dt) <= n + 1 implies dt in F1() . (n + 1) )
assume dt in F1() . (n + 1) ; :: thesis: height (dom dt) <= n + 1
then dt 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 A18: ( dt in F1() . n or dt 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;
per cases ( dt in F1() . n or not dt in F1() . n ) ;
suppose dt in F1() . n ; :: thesis: height (dom dt) <= n + 1
then A19: height (dom dt) <= n by A16, A17;
n <= n + 1 by NAT_1:11;
hence height (dom dt) <= n + 1 by A19, XXREAL_0:2; :: thesis: verum
end;
suppose not dt in F1() . n ; :: thesis: height (dom dt) <= n + 1
then consider o being Symbol of F2(), p being Element of (F1() . n) * such that
A20: dt = [o,H3(o,p)] -tree p and
A21: ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st
( p = q & o ==> pr1 (roots q) ) by A18;
reconsider p = p as FinSequence of FinTrees [: the carrier of F2(),F3():] by A21;
A22: dom dt = tree (doms p) by A20, TREES_4:10;
now :: thesis: for t being finite Tree st t in rng (doms p) holds
height t <= n
let t be finite Tree; :: thesis: ( t in rng (doms p) implies height t <= n )
assume t in rng (doms p) ; :: thesis: height t <= n
then consider k being object such that
A23: k in dom (doms p) and
A24: t = (doms p) . k by FUNCT_1:def 3;
A25: k in dom p by A23, TREES_3:37;
then A26: p . k in rng p by FUNCT_1:def 3;
rng p c= FinTrees [: the carrier of F2(),F3():] by FINSEQ_1:def 4;
then reconsider pk = p . k as Element of FinTrees [: the carrier of F2(),F3():] by A26;
A27: n in NAT by ORDINAL1:def 12;
A28: rng p c= F1() . n by FINSEQ_1:def 4;
A29: t = dom pk by A24, A25, FUNCT_6:22;
pk in Union F1() by A1, A26, A28, CARD_5:2, A27;
hence height t <= n by A16, A26, A28, A29; :: thesis: verum
end;
hence height (dom dt) <= n + 1 by A22, TREES_3:77; :: thesis: verum
end;
end;
end;
assume A30: height (dom dt) <= n + 1 ; :: thesis: dt in F1() . (n + 1)
defpred S2[ Nat] means dt in F1() . $1;
ex k being object st
( k in NAT & dt in F1() . k ) by A1, A17, CARD_5:2;
then A31: ex k being Nat st S2[k] ;
consider mk being Nat such that
A32: ( S2[mk] & ( for kk being Nat st S2[kk] holds
mk <= kk ) ) from NAT_1:sch 5(A31);
 deffunc H4( set , set ) -> set = { ([o,F5(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p) where o is Symbol of F2(), p is Element of (F1() . $1) * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st
( p = q & o ==> pr1 (roots q) ) } ;
A33: 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;
per cases ( mk = 0 or ex k being Nat st mk = k + 1 ) by NAT_1:6;
suppose mk = 0 ; :: thesis: dt in F1() . (n + 1)
then F1() . mk c= F1() . (0 + (n + 1)) by A33, MEASURE2:18;
hence dt in F1() . (n + 1) by A32; :: thesis: verum
end;
suppose ex k being Nat st mk = k + 1 ; :: thesis: dt in F1() . (n + 1)
then consider k being Nat such that
A34: mk = k + 1 ;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
A35: k < k + 1 by NAT_1:13;
F1() . mk = (F1() . k) \/ { ([o,H3(o,p)] -tree p) where o is Symbol of F2(), p is Element of (F1() . k) * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st
( p = q & o ==> pr1 (roots q) ) } by A3, A34;
then ( dt in F1() . k or dt in { ([o,H3(o,p)] -tree p) where o is Symbol of F2(), p is Element of (F1() . k) * : ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st
( p = q & o ==> pr1 (roots q) ) } ) by A32, XBOOLE_0:def 3;
then consider o being Symbol of F2(), p being Element of (F1() . k) * such that
A36: dt = [o,H3(o,p)] -tree p and
A37: ex q being FinSequence of FinTrees [: the carrier of F2(),F3():] st
( p = q & o ==> pr1 (roots q) ) by A32, A34, A35;
reconsider p = p as FinSequence of FinTrees [: the carrier of F2(),F3():] by A37;
A38: dom dt = tree (doms p) by A36, TREES_4:10;
rng p c= F1() . n
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng p or x in F1() . n )
assume x in rng p ; :: thesis: x in F1() . n
then consider k9 being object such that
A39: k9 in dom p and
A40: x = p . k9 by FUNCT_1:def 3;
A41: x in rng p by A39, A40, FUNCT_1:def 3;
rng p c= FinTrees [: the carrier of F2(),F3():] by FINSEQ_1:def 4;
then reconsider t = x as Element of FinTrees [: the carrier of F2(),F3():] by A41;
A42: k9 in dom (doms p) by A39, A40, FUNCT_6:22;
dom t = (doms p) . k9 by A39, A40, FUNCT_6:22;
then dom t in rng (doms p) by A42, FUNCT_1:def 3;
then height (dom t) < n + 1 by A30, A38, TREES_3:78, XXREAL_0:2;
then A43: height (dom t) <= n by NAT_1:13;
A44: rng p c= F1() . k by FINSEQ_1:def 4;
t in rng p by A39, A40, FUNCT_1:def 3;
then t in Union F1() by A1, A44, CARD_5:2;
hence x in F1() . n by A16, A43; :: thesis: verum
end;
then p is FinSequence of F1() . n by FINSEQ_1:def 4;
then reconsider p = p as Element of (F1() . n) * by FINSEQ_1:def 11;
[o,H3(o,p)] -tree p 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 A37;
then dt 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 A36, XBOOLE_0:def 3;
hence dt in F1() . (n + 1) by A3; :: thesis: verum
end;
end;
end;
end;
thus for n being Nat holds S1[n] from NAT_1:sch 2(A4, A15); :: thesis: verum