reconsider D = Union F3() as non empty set ;
TS (DTConMSA F2()) = union (rng (FreeSort F2())) by MSAFREE:11
.= Union (FreeSort F2()) by CARD_3:def 4 ;
then reconsider f1 = Flatten F6(), f2 = Flatten F7() as Function of (TS (DTConMSA F2())),D ;
deffunc H1( Element of (DTConMSA F2()), Element of (TS (DTConMSA F2())) * , Element of (Union F3()) * ) -> Element of Union F3() = F5(($1 `1),$2,$3);
consider H being Function of [: the carrier of (DTConMSA F2()),((TS (DTConMSA F2())) *),((Union F3()) *):],(Union F3()) such that
A5: for nt being Element of (DTConMSA F2())
for ts being Element of (TS (DTConMSA F2())) *
for x being Element of (Union F3()) * holds H . (nt,ts,x) = H1(nt,ts,x) from MULTOP_1:sch 4();
 reconsider H = H as Function of [: the carrier of (DTConMSA F2()),((TS (DTConMSA F2())) *),(D *):],D ;
deffunc H2( Element of (DTConMSA F2()), Element of (TS (DTConMSA F2())) * , Element of D * ) -> Element of D = H . ($1,$2,$3);
A6: DTConMSA F2() = DTConstrStr(# ([: the carrier' of F1(),{ the carrier of F1()}:] \/ (Union (coprod F2()))),(REL F2()) #) by MSAFREE:def 8;
A7: now :: thesis: for f being ManySortedFunction of FreeSort F2(),F3() st ( for o being OperSymbol of F1()
for ts being Element of Args (o,(FreeMSA F2()))
for x being Element of D * st x = (Flatten f) * ts holds
(f . (the_result_sort_of o)) . ((Den (o,(FreeMSA F2()))) . ts) = F5(o,ts,x) ) holds
for nt being Element of (DTConMSA F2())
for ts being Element of (TS (DTConMSA F2())) * st nt ==> roots ts holds
for x being Element of D * st x = (Flatten f) * ts holds
(Flatten f) . (nt -tree ts) = H . (nt,ts,x)
let f be ManySortedFunction of FreeSort F2(),F3(); :: thesis: ( ( for o being OperSymbol of F1()
for ts being Element of Args (o,(FreeMSA F2()))
for x being Element of D * st x = (Flatten f) * ts holds
(f . (the_result_sort_of o)) . ((Den (o,(FreeMSA F2()))) . ts) = F5(o,ts,x) ) implies for nt being Element of (DTConMSA F2())
for ts being Element of (TS (DTConMSA F2())) * st nt ==> roots ts holds
for x being Element of D * st x = (Flatten f) * ts holds
(Flatten f) . (nt -tree ts) = H . (nt,ts,x) )
assume A8: for o being OperSymbol of F1()
for ts being Element of Args (o,(FreeMSA F2()))
for x being Element of D * st x = (Flatten f) * ts holds
(f . (the_result_sort_of o)) . ((Den (o,(FreeMSA F2()))) . ts) = F5(o,ts,x) ; :: thesis: for nt being Element of (DTConMSA F2())
for ts being Element of (TS (DTConMSA F2())) * st nt ==> roots ts holds
for x being Element of D * st x = (Flatten f) * ts holds
(Flatten f) . (nt -tree ts) = H . (nt,ts,x)
let nt be Element of (DTConMSA F2()); :: thesis: for ts being Element of (TS (DTConMSA F2())) * st nt ==> roots ts holds
for x being Element of D * st x = (Flatten f) * ts holds
(Flatten f) . (nt -tree ts) = H . (nt,ts,x)
let ts be Element of (TS (DTConMSA F2())) * ; :: thesis: ( nt ==> roots ts implies for x being Element of D * st x = (Flatten f) * ts holds
(Flatten f) . (nt -tree ts) = H . (nt,ts,x) )
assume A9: nt ==> roots ts ; :: thesis: for x being Element of D * st x = (Flatten f) * ts holds
(Flatten f) . (nt -tree ts) = H . (nt,ts,x)
then [nt,(roots ts)] in REL F2() by A6, LANG1:def 1;
then consider o being OperSymbol of F1(), x2 being Element of { the carrier of F1()} such that
A10: nt = [o,x2] by Th2, DOMAIN_1:1;
let x be Element of D * ; :: thesis: ( x = (Flatten f) * ts implies (Flatten f) . (nt -tree ts) = H . (nt,ts,x) )
assume A11: x = (Flatten f) * ts ; :: thesis: (Flatten f) . (nt -tree ts) = H . (nt,ts,x)
A12: FreeMSA F2() = MSAlgebra(# (FreeSort F2()),(FreeOper F2()) #) by MSAFREE:def 14;
reconsider tss = ts as FinSequence of TS (DTConMSA F2()) by FINSEQ_1:def 11;
reconsider xx = x as Element of (Union F3()) * ;
A13: x2 = the carrier of F1() by TARSKI:def 1;
then A14: nt = Sym (o,F2()) by A10, MSAFREE:def 9;
then A15: tss in (((FreeSort F2()) #) * the Arity of F1()) . o by A9, MSAFREE:10;
((FreeSort F2()) * the ResultSort of F1()) . o = (FreeSort F2()) . (the_result_sort_of o) by FUNCT_2:15;
then A16: (DenOp (o,F2())) . ts in (FreeSort F2()) . (the_result_sort_of o) by A15, FUNCT_2:5;
(Flatten f) . ([o, the carrier of F1()] -tree ts) = (Flatten f) . ((DenOp (o,F2())) . tss) by A9, A10, A13, A14, MSAFREE:def 12
.= (f . (the_result_sort_of o)) . ((DenOp (o,F2())) . ts) by A16, Def1
.= (f . (the_result_sort_of o)) . ((Den (o,(FreeMSA F2()))) . ts) by A12, MSAFREE:def 13
.= F5(o,ts,x) by A8, A12, A15, A11
.= F5((nt `1),ts,x) by A10 ;
hence (Flatten f) . (nt -tree ts) = H1(nt,ts,xx) by A10, A13
.= H . (nt,ts,x) by A5 ;
:: thesis: verum
end;
then A17: for nt being Symbol of (DTConMSA F2())
for ts being Element of (TS (DTConMSA F2())) * st nt ==> roots ts holds
for x being Element of D * st x = f1 * ts holds
f1 . (nt -tree ts) = H2(nt,ts,x) by A1;
deffunc H3( Element of (DTConMSA F2())) -> Element of Union F3() = F4((root-tree $1));
A18: Terminals (DTConMSA F2()) = Union (coprod F2()) by MSAFREE:6;
consider G being Function of the carrier of (DTConMSA F2()),(Union F3()) such that
A19: for t being Element of (DTConMSA F2()) holds G . t = H3(t) from FUNCT_2:sch 4();
 reconsider G = G as Function of the carrier of (DTConMSA F2()),D ;
deffunc H4( Element of (DTConMSA F2())) -> Element of D = G . $1;
A20: dom F2() = the carrier of F1() by PARTFUN1:def 2;
A21: now :: thesis: for f being ManySortedFunction of FreeSort F2(),F3() st ( for s being SortSymbol of F1()
for y being set st y in FreeGen (s,F2()) holds
(f . s) . y = F4(y) ) holds
for t being Element of (DTConMSA F2()) st t in Terminals (DTConMSA F2()) holds
(Flatten f) . (root-tree t) = G . t
let f be ManySortedFunction of FreeSort F2(),F3(); :: thesis: ( ( for s being SortSymbol of F1()
for y being set st y in FreeGen (s,F2()) holds
(f . s) . y = F4(y) ) implies for t being Element of (DTConMSA F2()) st t in Terminals (DTConMSA F2()) holds
(Flatten f) . (root-tree t) = G . t )
assume A22: for s being SortSymbol of F1()
for y being set st y in FreeGen (s,F2()) holds
(f . s) . y = F4(y) ; :: thesis: for t being Element of (DTConMSA F2()) st t in Terminals (DTConMSA F2()) holds
(Flatten f) . (root-tree t) = G . t
let t be Element of (DTConMSA F2()); :: thesis: ( t in Terminals (DTConMSA F2()) implies (Flatten f) . (root-tree t) = G . t )
assume A23: t in Terminals (DTConMSA F2()) ; :: thesis: (Flatten f) . (root-tree t) = G . t
then reconsider s = t `2 as SortSymbol of F1() by A18, A20, CARD_3:22;
t `1 in F2() . (t `2) by A18, A23, CARD_3:22;
then A24: root-tree [(t `1),s] in FreeGen (s,F2()) by MSAFREE:def 15;
A25: t = [(t `1),(t `2)] by A18, A23, CARD_3:22;
hence (Flatten f) . (root-tree t) = (f . s) . (root-tree [(t `1),s]) by A24, Def1
.= F4((root-tree t)) by A22, A25, A24
.= G . t by A19 ;
:: thesis: verum
end;
then A26: for t being Symbol of (DTConMSA F2()) st t in Terminals (DTConMSA F2()) holds
f2 . (root-tree t) = H4(t) by A4;
A27: for nt being Symbol of (DTConMSA F2())
for ts being Element of (TS (DTConMSA F2())) * st nt ==> roots ts holds
for x being Element of D * st x = f2 * ts holds
f2 . (nt -tree ts) = H2(nt,ts,x) by A3, A7;
A28: for t being Element of (DTConMSA F2()) st t in Terminals (DTConMSA F2()) holds
f1 . (root-tree t) = H4(t) by A2, A21;
f1 = f2 from MSAFREE1:sch 1(A28, A17, A26, A27);
 hence F6() = F7() by Th4; :: thesis: verum