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:79, 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 & ex q being FinSequence of FinTrees [:the carrier of F₂(),F₃():] st
( p = q & o ==> pr1 (roots q) ) ) by A9;
A11: dt = root-tree (dt . {} ) by A6, TREES_1:80, TREES_4:5;
then A12: p = {} by A10, TREES_4:17;
then dt = root-tree [o,F₅(o,{} ,{} )] by A10, A11, Th3, Th7, TREES_4:def 4;
hence contradiction by A2, A7, A10, A12, Th3, Th7; :: thesis: verum

end;

end;

A13: 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:10;
hence contradiction by A13; :: thesis: verum

end;

A14: now

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A15: 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 A16: 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 A17: ( 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 ( height (dom dt) <= n & n <= n + 1 ) by A15, A16, NAT_1:11;
hence height (dom dt) <= n + 1 by 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
A18: ( dt = [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 A17;
reconsider p = p as FinSequence of FinTrees [:the carrier of F₂(),F₃():] by A18;
A19: dom dt = tree (doms p) by A18, 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
A20: ( k in dom (doms p) & t = (doms p) . k ) by FUNCT_1:def 5;
A21: k in dom p by A20, TREES_3:39;
then A22: ( p . k in rng p & rng p c= FinTrees [:the carrier of F₂(),F₃():] ) by FINSEQ_1:def 4, FUNCT_1:def 5;
then reconsider pk = p . k as Element of FinTrees [:the carrier of F₂(),F₃():] ;
A23: rng p c= F₁() . n by FINSEQ_1:def 4;
then A24: ( t = dom pk & pk in F₁() . n ) by A20, A21, A22, FUNCT_6:31;
pk in Union F₁() by A1, A22, A23, CARD_5:10;
hence height t <= n by A15, A24; :: thesis: verum

end;

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

end;

end;

end;

assume A25: height (dom dt) <= n + 1 ; :: thesis: dt in F₁() . (n + 1)
defpred S₂[ Nat] means dt in F₁() . $1;
consider k being set such that
A26: ( k in NAT & dt in F₁() . k ) by A1, A16, CARD_5:10;
A27: ex k being Nat st S₂[k] by A26;
consider mk being Nat such that
A28: ( S₂[mk] & ( for kk being Nat st S₂[kk] holds
mk <= kk ) ) from NAT_1:sch 5(A27);
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) ) } ;
A29: 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)) & 0 + (n + 1) = n + 1 ) by A29, MEASURE2:22;
hence dt in F₁() . (n + 1) by A28; :: 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
A31: mk = k + 1 ;
reconsider k = k as Element of NAT by ORDINAL1:def 13;
A32: 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, A31;
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 A28, XBOOLE_0:def 3;
then consider o being Symbol of F₂(), p being Element of (F₁() . k) * such that
A33: ( dt = [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 A28, A31, A32;
reconsider p = p as FinSequence of FinTrees [:the carrier of F₂(),F₃():] by A33;
A34: dom dt = tree (doms p) by A33, 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 k' being set such that
A35: ( k' in dom p & x = p . k' ) by FUNCT_1:def 5;
( x in rng p & rng p c= FinTrees [:the carrier of F₂(),F₃():] ) by A35, FINSEQ_1:def 4, FUNCT_1:def 5;
then reconsider t = x as Element of FinTrees [:the carrier of F₂(),F₃():] ;
t = x ;
then ( k' in dom (doms p) & dom t = (doms p) . k' ) by A35, FUNCT_6:31;
then dom t in rng (doms p) by FUNCT_1:def 5;
then height (dom t) < n + 1 by A25, A34, TREES_3:81, XXREAL_0:2;
then A36: height (dom t) <= n by NAT_1:13;
( rng p c= F₁() . k & t in rng p ) by A35, FINSEQ_1:def 4, FUNCT_1:def 5;
then t in Union F₁() by A1, CARD_5:10;
hence x in F₁() . n by A15, A36; :: 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 A33;
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 A33, 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, A14); :: thesis: verum