set f = F₁();
set G = F₂();
set D = 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)));
defpred S₁[ Nat] means for dt being Element of FinTrees [: the carrier of F₂(),F₃():] st dt in Union F₁() holds
( dt in F₁() . $1 iff height (dom dt) <= $1 );
A4: S₁[ 0 ]

proof

let dt be Element of FinTrees [: the carrier of F₂(),F₃():]; :: thesis: ( dt in Union F₁() implies ( dt in F₁() . 0 iff height (dom dt) <= 0 ) )
assume A5: dt in Union F₁() ; :: thesis: ( dt in F₁() . 0 iff height (dom dt) <= 0 )

hereby :: thesis: ( height (dom dt) <= 0 implies dt in F₁() . 0 )

assume dt in F₁() . 0 ; :: thesis: height (dom dt) <= 0
then ex t being Symbol of F₂() ex d being Element of F₃() st
( dt = root-tree [t,d] & ( ( t in Terminals F₂() & d = F₄(t) ) or ( t ==> {} & d = F₅(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 F₁() . 0
then A6: height (dom dt) = 0 ;
defpred S₂[ Nat] means not dt in F₁() . $1;
assume A7: S₂[ 0 ] ; :: thesis: contradiction

A8: now :: thesis: for n being Nat st S₂[n] holds
S₂[n + 1]

let n be Nat; :: thesis: ( S₂[n] implies S₂[n + 1] )
assume A9: S₂[n] ; :: thesis: S₂[n + 1]
thus S₂[n + 1] :: thesis: verum

proof

assume dt in F₁() . (n + 1) ; :: thesis: contradiction
then dt 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 ( dt in F₁() . n or dt 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;
then consider o being Symbol of F₂(), p being Element of (F₁() . n) * such that
A10: dt = [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 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,F₅(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 S₂[n] from NAT_1:sch 2(A7, A8);
ex n being object st
( n in NAT & dt in F₁() . n ) by A1, A5, CARD_5:2;
hence contradiction by A14; :: thesis: verum

end;

A15: now :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A16: S₁[n] ; :: thesis: S₁[n + 1]
thus S₁[n + 1] :: thesis: verum

proof

let dt be Element of FinTrees [: the carrier of F₂(),F₃():]; :: thesis: ( dt in Union F₁() implies ( dt in F₁() . (n + 1) iff height (dom dt) <= n + 1 ) )
assume A17: dt in Union F₁() ; :: thesis: ( dt in F₁() . (n + 1) iff height (dom dt) <= n + 1 )

hereby :: thesis: ( height (dom dt) <= n + 1 implies dt in F₁() . (n + 1) )

assume dt in F₁() . (n + 1) ; :: thesis: height (dom dt) <= n + 1
then dt 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 A18: ( dt in F₁() . n or dt 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;

per cases ( dt in F₁() . n or not dt in F₁() . n ) ;

suppose dt in F₁() . 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 F₁() . n ; :: thesis: height (dom dt) <= n + 1

then consider o being Symbol of F₂(), p being Element of (F₁() . n) * such that
A20: dt = [o,H₃(o,p)] -tree p and
A21: ex q being FinSequence of FinTrees [: the carrier of F₂(),F₃():] st
( p = q & o ==> pr1 (roots q) ) by A18;
reconsider p = p as FinSequence of FinTrees [: the carrier of F₂(),F₃():] 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 F₂(),F₃():] by FINSEQ_1:def 4;
then reconsider pk = p . k as Element of FinTrees [: the carrier of F₂(),F₃():] by A26;
A27: n in NAT by ORDINAL1:def 12;
A28: rng p c= F₁() . n by FINSEQ_1:def 4;
A29: t = dom pk by A24, A25, FUNCT_6:22;
pk in Union F₁() 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 F₁() . (n + 1)
defpred S₂[ Nat] means dt in F₁() . $1;
ex k being object st
( k in NAT & dt in F₁() . k ) by A1, A17, CARD_5:2;
then A31: ex k being Nat st S₂[k] ;
consider mk being Nat such that
A32: ( S₂[mk] & ( for kk being Nat st S₂[kk] holds
mk <= kk ) ) from NAT_1:sch 5(A31);
deffunc H₄( set , set ) -> set = { ([o,F₅(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p) where o is Symbol of F₂(), p is Element of (F₁() . $1) * : ex q being FinSequence of FinTrees [: the carrier of F₂(),F₃():] st
( p = q & o ==> pr1 (roots q) ) } ;
A33: for n being Nat holds F₁() . n c= F₁() . (n + 1)

proof

let n be Nat; :: thesis: F₁() . n c= F₁() . (n + 1)
F₁() . (n + 1) = (F₁() . n) \/ H₄(n,F₁() . n) by A3;
hence F₁() . n c= F₁() . (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 F₁() . (n + 1)

then F₁() . mk c= F₁() . (0 + (n + 1)) by A33, MEASURE2:18;
hence dt in F₁() . (n + 1) by A32; :: thesis: verum

end;

suppose ex k being Nat st mk = k + 1 ; :: thesis: dt in F₁() . (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;
F₁() . mk = (F₁() . k) \/ { ([o,H₃(o,p)] -tree p) where o is Symbol of F₂(), p is Element of (F₁() . k) * : ex q being FinSequence of FinTrees [: the carrier of F₂(),F₃():] st
( p = q & o ==> pr1 (roots q) ) } by A3, A34;
then ( dt in F₁() . k or dt in { ([o,H₃(o,p)] -tree p) where o is Symbol of F₂(), p is Element of (F₁() . k) * : ex q being FinSequence of FinTrees [: the carrier of F₂(),F₃():] st
( p = q & o ==> pr1 (roots q) ) } ) by A32, XBOOLE_0:def 3;
then consider o being Symbol of F₂(), p being Element of (F₁() . k) * such that
A36: dt = [o,H₃(o,p)] -tree p and
A37: ex q being FinSequence of FinTrees [: the carrier of F₂(),F₃():] st
( p = q & o ==> pr1 (roots q) ) by A32, A34, A35;
reconsider p = p as FinSequence of FinTrees [: the carrier of F₂(),F₃():] by A37;
A38: dom dt = tree (doms p) by A36, TREES_4:10;
rng p c= F₁() . n

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng p or x in F₁() . n )
assume x in rng p ; :: thesis: x in F₁() . 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 F₂(),F₃():] by FINSEQ_1:def 4;
then reconsider t = x as Element of FinTrees [: the carrier of F₂(),F₃():] 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= F₁() . k by FINSEQ_1:def 4;
t in rng p by A39, A40, FUNCT_1:def 3;
then t in Union F₁() by A1, A44, CARD_5:2;
hence x in F₁() . n by A16, A43; :: thesis: verum

end;

then p is FinSequence of F₁() . n by FINSEQ_1:def 4;
then reconsider p = p as Element of (F₁() . n) * by FINSEQ_1:def 11;
[o,H₃(o,p)] -tree p 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 A37;
then dt 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 A36, XBOOLE_0:def 3;
hence dt in F₁() . (n + 1) by A3; :: thesis: verum

end;

end;

end;

end;

thus for n being Nat holds S₁[n] from NAT_1:sch 2(A4, A15); :: thesis: verum