set G = F1();
deffunc H3( Symbol of F1(), FinSequence) -> Element of F2() = F4($1,(pr1 (roots $2)),(pr2 (roots $2)));
deffunc H4( set , set ) -> set = $2 \/ { ([o,F4(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p) where o is Symbol of F1(), p is Element of $2 * : ex q being FinSequence of FinTrees [:the carrier of F1(),F2():] st
( p = q & o ==> pr1 (roots q) ) } ;
consider f being Function such that
A1: dom f = NAT and
A2: f . 0 = { (root-tree [t,d]) where t is Symbol of F1(), d is Element of F2() : ( ( t in Terminals F1() & d = F3(t) ) or ( t ==> {} & d = F4(t,{} ,{} ) ) ) } and
A3: for n being Nat holds f . (n + 1) = H4(n,f . n) from NAT_1:sch 11();
 A4: for n being Element of NAT holds f . (n + 1) = (f . n) \/ { ([o,F4(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p) where o is Symbol of F1(), p is Element of (f . n) * : ex q being FinSequence of FinTrees [:the carrier of F1(),F2():] st
( p = q & o ==> pr1 (roots q) ) } by A3;
ex X1 being Subset of (FinTrees the carrier of F1()) st
( X1 = { (t `1 ) where t is Element of FinTrees [:the carrier of F1(),F2():] : t in Union f } & ( for d being Symbol of F1() st d in Terminals F1() holds
root-tree d in X1 ) & ( for o being Symbol of F1()
for p being FinSequence of X1 st o ==> roots p holds
o -tree p in X1 ) & ( for F being Subset of (FinTrees the carrier of F1()) st ( for d being Symbol of F1() st d in Terminals F1() holds
root-tree d in F ) & ( for o being Symbol of F1()
for p being FinSequence of F st o ==> roots p holds
o -tree p in F ) holds
X1 c= F ) ) from DTCONSTR:sch 4(A1, A2, A4);
 then A5: TS F1() = { (t `1 ) where t is Element of FinTrees [:the carrier of F1(),F2():] : t in Union f } by Def4;
defpred S1[ set , set ] means for dt being DecoratedTree of st dt in Union f & $1 = dt `1 holds
$2 = (dt `2 ) . {} ;
A6: for e being set st e in TS F1() holds
ex u being set st
( u in F2() & S1[e,u] )
proof
let e be set ; :: thesis: ( e in TS F1() implies ex u being set st
( u in F2() & S1[e,u] ) )
assume e in TS F1() ; :: thesis: ex u being set st
( u in F2() & S1[e,u] )
then consider DT being Element of FinTrees [:the carrier of F1(),F2():] such that
A7: ( e = DT `1 & DT in Union f ) by A5;
reconsider r = {} as Node of (DT `2 ) by TREES_1:47;
take u = (DT `2 ) . r; :: thesis: ( u in F2() & S1[e,u] )
thus u in F2() ; :: thesis: S1[e,u]
A8: for dt1, dt2 being DecoratedTree of st dt1 in Union f & dt2 in Union f & dt1 `1 = dt2 `1 holds
dt1 = dt2 from DTCONSTR:sch 6(A1, A2, A4);
 let dt be DecoratedTree of ; :: thesis: ( dt in Union f & e = dt `1 implies u = (dt `2 ) . {} )
assume ( dt in Union f & e = dt `1 ) ; :: thesis: u = (dt `2 ) . {}
hence u = (dt `2 ) . {} by A7, A8; :: thesis: verum
end;
consider ff being Function such that
A9: ( dom ff = TS F1() & rng ff c= F2() ) and
A10: for e being set st e in TS F1() holds
S1[e,ff . e] from WELLORD2:sch 1(A6);
 reconsider ff = ff as Function of (TS F1()),F2() by A9, FUNCT_2:def 1, RELSET_1:11;
take ff ; :: thesis: ( ( for t being Symbol of F1() st t in Terminals F1() holds
ff . (root-tree t) = F3(t) ) & ( for nt being Symbol of F1()
for ts being FinSequence of TS F1() st nt ==> roots ts holds
ff . (nt -tree ts) = F4(nt,(roots ts),(ff * ts)) ) )
consider X being Subset of (FinTrees [:the carrier of F1(),F2():]) such that
A11: X = Union f and
A12: for d being Symbol of F1() st d in Terminals F1() holds
root-tree [d,F3(d)] in X and
A13: for o being Symbol of F1()
for p being FinSequence of X st o ==> pr1 (roots p) holds
[o,F4(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p in X and
for F being Subset of (FinTrees [:the carrier of F1(),F2():]) st ( for d being Symbol of F1() st d in Terminals F1() holds
root-tree [d,F3(d)] in F ) & ( for o being Symbol of F1()
for p being FinSequence of F st o ==> pr1 (roots p) holds
[o,F4(o,(pr1 (roots p)),(pr2 (roots p)))] -tree p in F ) holds
X c= F from DTCONSTR:sch 3(A1, A2, A4);
hereby :: thesis: for nt being Symbol of F1()
for ts being FinSequence of TS F1() st nt ==> roots ts holds
ff . (nt -tree ts) = F4(nt,(roots ts),(ff * ts))
let t be Symbol of F1(); :: thesis: ( t in Terminals F1() implies ff . (root-tree t) = F3(t) )
assume A14: t in Terminals F1() ; :: thesis: ff . (root-tree t) = F3(t)
A15: ( (root-tree [t,F3(t)]) `1 = root-tree t & (root-tree [t,F3(t)]) `2 = root-tree F3(t) ) by TREES_4:25;
root-tree [t,F3(t)] in Union f by A11, A12, A14;
then root-tree t in TS F1() by A5, A15;
hence ff . (root-tree t) = (root-tree F3(t)) . {} by A10, A11, A12, A14, A15
.= F3(t) by TREES_4:3 ;
:: thesis: verum
end;
let nt be Symbol of F1(); :: thesis: for ts being FinSequence of TS F1() st nt ==> roots ts holds
ff . (nt -tree ts) = F4(nt,(roots ts),(ff * ts))
let ts be FinSequence of TS F1(); :: thesis: ( nt ==> roots ts implies ff . (nt -tree ts) = F4(nt,(roots ts),(ff * ts)) )
set rts = roots ts;
assume A16: nt ==> roots ts ; :: thesis: ff . (nt -tree ts) = F4(nt,(roots ts),(ff * ts))
set x = ff * ts;
A17: dom ts = Seg (len ts) by FINSEQ_1:def 3;
defpred S2[ set , set ] means ex dt being DecoratedTree of st
( dt = $2 & dt `1 = ts . $1 & dt in Union f );
A18: for k being Nat st k in Seg (len ts) holds
ex x being Element of FinTrees [:the carrier of F1(),F2():] st S2[k,x]
proof
let k be Nat; :: thesis: ( k in Seg (len ts) implies ex x being Element of FinTrees [:the carrier of F1(),F2():] st S2[k,x] )
assume k in Seg (len ts) ; :: thesis: ex x being Element of FinTrees [:the carrier of F1(),F2():] st S2[k,x]
then ( ts . k in rng ts & rng ts c= TS F1() ) by A17, FINSEQ_1:def 4, FUNCT_1:def 5;
then ts . k in TS F1() ;
then ex x being Element of FinTrees [:the carrier of F1(),F2():] st
( ts . k = x `1 & x in Union f ) by A5;
hence ex x being Element of FinTrees [:the carrier of F1(),F2():] st S2[k,x] ; :: thesis: verum
end;
consider dts being FinSequence of FinTrees [:the carrier of F1(),F2():] such that
A19: dom dts = Seg (len ts) and
A20: for k being Nat st k in Seg (len ts) holds
S2[k,dts . k] from FINSEQ_1:sch 5(A18);
 rng dts c= X
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng dts or x in X )
assume x in rng dts ; :: thesis: x in X
then consider k being set such that
A21: ( k in dom ts & x = dts . k ) by A17, A19, FUNCT_1:def 5;
reconsider k = k as Element of NAT by A21;
ex dt being DecoratedTree of st
( dt = x & dt `1 = ts . k & dt in Union f ) by A17, A20, A21;
hence x in X by A11; :: thesis: verum
end;
then reconsider dts = dts as FinSequence of X by FINSEQ_1:def 4;
A22: dom (roots ts) = dom ts by TREES_3:def 18;
A23: ( dom (pr1 (roots dts)) = dom (roots dts) & dom (pr2 (roots dts)) = dom (roots dts) ) by MCART_1:def 12, MCART_1:def 13;
then A24: ( dom (pr1 (roots dts)) = dom ts & dom (pr2 (roots dts)) = dom ts ) by A17, A19, TREES_3:def 18;
now
let k be Nat; :: thesis: ( k in dom ts implies (roots ts) . k = (pr1 (roots dts)) . k )
assume A25: k in dom ts ; :: thesis: (roots ts) . k = (pr1 (roots dts)) . k
then consider dt being DecoratedTree of such that
A26: ( dt = dts . k & dt `1 = ts . k & dt in Union f ) by A17, A20;
reconsider r = {} as Node of dt by TREES_1:47;
ex T being DecoratedTree st
( T = ts . k & (roots ts) . k = T . {} ) by A25, TREES_3:def 18;
then A27: (roots ts) . k = (dt . r) `1 by A26, TREES_3:41;
ex T being DecoratedTree st
( T = dts . k & (roots dts) . k = T . {} ) by A17, A19, A25, TREES_3:def 18;
hence (roots ts) . k = (pr1 (roots dts)) . k by A23, A24, A25, A26, A27, MCART_1:def 12; :: thesis: verum
end;
then A28: roots ts = pr1 (roots dts) by A22, A24, FINSEQ_1:17;
then A29: [nt,H3(nt,dts)] -tree dts in X by A13, A16;
A30: rng dts c= FinTrees [:the carrier of F1(),F2():] by FINSEQ_1:def 4;
FinTrees [:the carrier of F1(),F2():] c= Trees [:the carrier of F1(),F2():] by TREES_3:22;
then rng dts c= Trees [:the carrier of F1(),F2():] by A30, XBOOLE_1:1;
then reconsider dts' = dts as FinSequence of Trees [:the carrier of F1(),F2():] by FINSEQ_1:def 4;
A31: rng ts c= FinTrees the carrier of F1() by FINSEQ_1:def 4;
FinTrees the carrier of F1() c= Trees the carrier of F1() by TREES_3:22;
then rng ts c= Trees the carrier of F1() by A31, XBOOLE_1:1;
then reconsider ts' = ts as FinSequence of Trees the carrier of F1() by FINSEQ_1:def 4;
now
let i be Element of NAT ; :: thesis: ( i in dom dts implies for T being DecoratedTree of st T = dts . i holds
ts . i = T `1 )
assume i in dom dts ; :: thesis: for T being DecoratedTree of st T = dts . i holds
ts . i = T `1
then consider dt being DecoratedTree of such that
A32: ( dt = dts . i & dt `1 = ts . i & dt in Union f ) by A19, A20;
let T be DecoratedTree of ; :: thesis: ( T = dts . i implies ts . i = T `1 )
assume T = dts . i ; :: thesis: ts . i = T `1
hence ts . i = T `1 by A32; :: thesis: verum
end;
then A33: ([nt,H3(nt,dts)] -tree dts') `1 = nt -tree ts' by A17, A19, TREES_4:27;
A34: rng ts c= dom ff by A9, FINSEQ_1:def 4;
then A35: dom (ff * ts) = dom ts by RELAT_1:46;
now
let k be Nat; :: thesis: ( k in dom ts implies (ff * ts) . k = (pr2 (roots dts)) . k )
assume A36: k in dom ts ; :: thesis: (ff * ts) . k = (pr2 (roots dts)) . k
then consider dt being DecoratedTree of such that
A37: ( dt = dts . k & dt `1 = ts . k & dt in Union f ) by A17, A20;
reconsider r = {} as Node of dt by TREES_1:47;
A38: ts . k in rng ts by A36, FUNCT_1:def 5;
A39: (ff * ts) . k = ff . (dt `1 ) by A35, A36, A37, FUNCT_1:22
.= (dt `2 ) . {} by A9, A10, A34, A37, A38
.= (dt . r) `2 by TREES_3:41 ;
ex T being DecoratedTree st
( T = dts . k & (roots dts) . k = T . r ) by A17, A19, A36, TREES_3:def 18;
hence (ff * ts) . k = (pr2 (roots dts)) . k by A23, A24, A36, A37, A39, MCART_1:def 13; :: thesis: verum
end;
then A40: ff * ts = pr2 (roots dts) by A24, A35, FINSEQ_1:17;
reconsider r = {} as Node of ([nt,F4(nt,(roots ts),(ff * ts))] -tree dts) by TREES_1:47;
nt -tree ts in TS F1() by A5, A11, A29, A33;
then ff . (nt -tree ts) = (([nt,F4(nt,(roots ts),(ff * ts))] -tree dts) `2 ) . r by A10, A11, A13, A16, A28, A33, A40
.= (([nt,F4(nt,(roots ts),(ff * ts))] -tree dts) . r) `2 by TREES_3:41
.= [nt,F4(nt,(roots ts),(ff * ts))] `2 by TREES_4:def 4 ;
hence ff . (nt -tree ts) = F4(nt,(roots ts),(ff * ts)) by MCART_1:7; :: thesis: verum