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 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 Def1;
defpred S1[ object , object ] means for dt being DecoratedTree of [: the carrier of F1(),F2():] st dt in Union f & $1 = dt `1 holds
$2 = (dt `2) . {};
A6: for e being object st e in TS F1() holds
ex u being object st
( u in F2() & S1[e,u] )
proof
let e be object ; :: thesis: ( e in TS F1() implies ex u being object st
( u in F2() & S1[e,u] ) )
assume e in TS F1() ; :: thesis: ex u being object 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 and
A8: DT in Union f by A5;
reconsider r = {} as Node of (DT `2) by TREES_1:22;
take u = (DT `2) . r; :: thesis: ( u in F2() & S1[e,u] )
thus u in F2() ; :: thesis: S1[e,u]
A9: for dt1, dt2 being DecoratedTree of [: the carrier of F1(),F2():] 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 [: the carrier of F1(),F2():]; :: thesis: ( dt in Union f & e = dt `1 implies u = (dt `2) . {} )
assume that
A10: dt in Union f and
A11: e = dt `1 ; :: thesis: u = (dt `2) . {}
thus u = (dt `2) . {} by A7, A8, A9, A10, A11; :: thesis: verum
end;
consider ff being Function such that
A12: ( dom ff = TS F1() & rng ff c= F2() ) and
A13: for e being object st e in TS F1() holds
S1[e,ff . e] from FUNCT_1:sch 6(A6);
 reconsider ff = ff as Function of (TS F1()),F2() by A12, FUNCT_2:def 1, RELSET_1:4;
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
A14: X = Union f and
A15: for d being Symbol of F1() st d in Terminals F1() holds
root-tree [d,F3(d)] in X and
A16: 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 A17: t in Terminals F1() ; :: thesis: ff . (root-tree t) = F3(t)
A18: (root-tree [t,F3(t)]) `1 = root-tree t by TREES_4:25;
A19: (root-tree [t,F3(t)]) `2 = root-tree F3(t) by TREES_4:25;
root-tree [t,F3(t)] in Union f by A14, A15, A17;
then root-tree t in TS F1() by A5, A18;
hence ff . (root-tree t) = (root-tree F3(t)) . {} by A13, A14, A15, A17, A18, A19
.= 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 A20: nt ==> roots ts ; :: thesis: ff . (nt -tree ts) = F4(nt,(roots ts),(ff * ts))
set x = ff * ts;
A21: dom ts = Seg (len ts) by FINSEQ_1:def 3;
defpred S2[ set , set ] means ex dt being DecoratedTree of [: the carrier of F1(),F2():] st
( dt = $2 & dt `1 = ts . $1 & dt in Union f );
A22: 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 A23: ts . k in rng ts by A21, FUNCT_1:def 3;
rng ts c= TS F1() by FINSEQ_1:def 4;
then ts . k in TS F1() by A23;
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
A24: dom dts = Seg (len ts) and
A25: for k being Nat st k in Seg (len ts) holds
S2[k,dts . k] from FINSEQ_1:sch 5(A22);
 rng dts c= X
proof
let x be object ; :: 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 object such that
A26: k in dom ts and
A27: x = dts . k by A21, A24, FUNCT_1:def 3;
reconsider k = k as Element of NAT by A26;
ex dt being DecoratedTree of [: the carrier of F1(),F2():] st
( dt = x & dt `1 = ts . k & dt in Union f ) by A21, A25, A26, A27;
hence x in X by A14; :: thesis: verum
end;
then reconsider dts = dts as FinSequence of X by FINSEQ_1:def 4;
A28: dom (roots ts) = dom ts by TREES_3:def 18;
A29: dom (pr1 (roots dts)) = dom (roots dts) by MCART_1:def 12;
A30: dom (pr2 (roots dts)) = dom (roots dts) by MCART_1:def 13;
A31: dom (pr1 (roots dts)) = dom ts by A21, A24, A29, TREES_3:def 18;
A32: dom (pr2 (roots dts)) = dom ts by A21, A24, A30, TREES_3:def 18;
now :: thesis: for k being Nat st k in dom ts holds
(roots ts) . k = (pr1 (roots dts)) . k
let k be Nat; :: thesis: ( k in dom ts implies (roots ts) . k = (pr1 (roots dts)) . k )
assume A33: k in dom ts ; :: thesis: (roots ts) . k = (pr1 (roots dts)) . k
then consider dt being DecoratedTree of [: the carrier of F1(),F2():] such that
A34: dt = dts . k and
A35: dt `1 = ts . k and
dt in Union f by A21, A25;
reconsider r = {} as Node of dt by TREES_1:22;
ex T being DecoratedTree st
( T = ts . k & (roots ts) . k = T . {} ) by A33, TREES_3:def 18;
then A36: (roots ts) . k = (dt . r) `1 by A35, TREES_3:39;
ex T being DecoratedTree st
( T = dts . k & (roots dts) . k = T . {} ) by A21, A24, A33, TREES_3:def 18;
hence (roots ts) . k = (pr1 (roots dts)) . k by A29, A31, A33, A34, A36, MCART_1:def 12; :: thesis: verum
end;
then A37: roots ts = pr1 (roots dts) by A28, A31, FINSEQ_1:13;
then A38: [nt,H3(nt,dts)] -tree dts in X by A16, A20;
A39: 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:21;
then rng dts c= Trees [: the carrier of F1(),F2():] by A39;
then reconsider dts9 = dts as FinSequence of Trees [: the carrier of F1(),F2():] by FINSEQ_1:def 4;
A40: 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:21;
then rng ts c= Trees the carrier of F1() by A40;
then reconsider ts9 = ts as FinSequence of Trees the carrier of F1() by FINSEQ_1:def 4;
now :: thesis: for i being Nat st i in dom dts holds
for T being DecoratedTree of [: the carrier of F1(),F2():] st T = dts . i holds
ts . i = T `1
let i be Nat; :: thesis: ( i in dom dts implies for T being DecoratedTree of [: the carrier of F1(),F2():] st T = dts . i holds
ts . i = T `1 )
assume i in dom dts ; :: thesis: for T being DecoratedTree of [: the carrier of F1(),F2():] st T = dts . i holds
ts . i = T `1
then A41: ex dt being DecoratedTree of [: the carrier of F1(),F2():] st
( dt = dts . i & dt `1 = ts . i & dt in Union f ) by A24, A25;
let T be DecoratedTree of [: the carrier of F1(),F2():]; :: thesis: ( T = dts . i implies ts . i = T `1 )
assume T = dts . i ; :: thesis: ts . i = T `1
hence ts . i = T `1 by A41; :: thesis: verum
end;
then A42: ([nt,H3(nt,dts)] -tree dts9) `1 = nt -tree ts9 by A21, A24, TREES_4:27;
A43: rng ts c= dom ff by A12, FINSEQ_1:def 4;
then A44: dom (ff * ts) = dom ts by RELAT_1:27;
now :: thesis: for k being Nat st k in dom ts holds
(ff * ts) . k = (pr2 (roots dts)) . k
let k be Nat; :: thesis: ( k in dom ts implies (ff * ts) . k = (pr2 (roots dts)) . k )
assume A45: k in dom ts ; :: thesis: (ff * ts) . k = (pr2 (roots dts)) . k
then consider dt being DecoratedTree of [: the carrier of F1(),F2():] such that
A46: dt = dts . k and
A47: dt `1 = ts . k and
A48: dt in Union f by A21, A25;
reconsider r = {} as Node of dt by TREES_1:22;
A49: ts . k in rng ts by A45, FUNCT_1:def 3;
A50: (ff * ts) . k = ff . (dt `1) by A44, A45, A47, FUNCT_1:12
.= (dt `2) . {} by A12, A13, A43, A47, A48, A49
.= (dt . r) `2 by TREES_3:39 ;
ex T being DecoratedTree st
( T = dts . k & (roots dts) . k = T . r ) by A21, A24, A45, TREES_3:def 18;
hence (ff * ts) . k = (pr2 (roots dts)) . k by A29, A31, A45, A46, A50, MCART_1:def 13; :: thesis: verum
end;
then A51: ff * ts = pr2 (roots dts) by A32, A44, FINSEQ_1:13;
reconsider r = {} as Node of ([nt,F4(nt,(roots ts),(ff * ts))] -tree dts) by TREES_1:22;
nt -tree ts in TS F1() by A5, A14, A38, A42;
then ff . (nt -tree ts) = (([nt,F4(nt,(roots ts),(ff * ts))] -tree dts) `2) . r by A13, A14, A16, A20, A37, A42, A51
.= (([nt,F4(nt,(roots ts),(ff * ts))] -tree dts) . r) `2 by TREES_3:39
.= [nt,F4(nt,(roots ts),(ff * ts))] `2 by TREES_4:def 4 ;
hence ff . (nt -tree ts) = F4(nt,(roots ts),(ff * ts)) ; :: thesis: verum