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₁[ Element of 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₂[ Element of NAT ] means not dt in F₁() . $1;
assume A7: S₂[ 0 ] ; :: thesis: contradiction

A8: now

let n be Element of 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 Element of NAT holds S₂[n] from NAT_1:sch 1(A7, A8);
ex n being set st
( n in NAT & dt in F₁() . n ) by A1, A5, CARD_5:2;
hence contradiction by A14; :: thesis: verum

end;

A15: now

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

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 set 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: rng p c= F₁() . n by FINSEQ_1:def 4;
A28: t = dom pk by A24, A25, FUNCT_6:22;
pk in Union F₁() by A1, A26, A27, CARD_5:2;
hence height t <= n by A16, A26, A27, A28; :: thesis: verum

end;

hence height (dom dt) <= n + 1 by A22, TREES_3:77; :: thesis: verum

end;

end;

end;

assume A29: height (dom dt) <= n + 1 ; :: thesis: dt in F₁() . (n + 1)
defpred S₂[ Nat] means dt in F₁() . $1;
ex k being set st
( k in NAT & dt in F₁() . k ) by A1, A17, CARD_5:2;
then A30: ex k being Nat st S₂[k] ;
consider mk being Nat such that
A31: ( S₂[mk] & ( for kk being Nat st S₂[kk] holds
mk <= kk ) ) from NAT_1:sch 5(A30);
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) ) } ;
A32: for n being Element of NAT holds F₁() . n c= F₁() . (n + 1)

proof

let n be Element of 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 A32, MEASURE2:18;
hence dt in F₁() . (n + 1) by A31; :: 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
A33: mk = k + 1 ;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
A34: 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, A33;
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 A31, XBOOLE_0:def 3;
then consider o being Symbol of F₂(), p being Element of (F₁() . k) * such that
A35: dt = [o,H₃(o,p)] -tree p and
A36: ex q being FinSequence of FinTrees [: the carrier of F₂(),F₃():] st
( p = q & o ==> pr1 (roots q) ) by A31, A33, A34;
reconsider p = p as FinSequence of FinTrees [: the carrier of F₂(),F₃():] by A36;
A37: dom dt = tree (doms p) by A35, TREES_4:10;
rng p c= F₁() . n

proof

let x be set ; :: 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 set such that
A38: k9 in dom p and
A39: x = p . k9 by FUNCT_1:def 3;
A40: x in rng p by A38, A39, 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 A40;
A41: k9 in dom (doms p) by A38, A39, FUNCT_6:22;
dom t = (doms p) . k9 by A38, A39, FUNCT_6:22;
then dom t in rng (doms p) by A41, FUNCT_1:def 3;
then height (dom t) < n + 1 by A29, A37, TREES_3:78, XXREAL_0:2;
then A42: height (dom t) <= n by NAT_1:13;
A43: rng p c= F₁() . k by FINSEQ_1:def 4;
t in rng p by A38, A39, FUNCT_1:def 3;
then t in Union F₁() by A1, A43, CARD_5:2;
hence x in F₁() . n by A16, A42; :: 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 A36;
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 A35, XBOOLE_0:def 3;
hence dt in F₁() . (n + 1) by A3; :: thesis: verum

end;

end;

end;

end;

thus for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A4, A15); :: thesis: verum