let S be non empty non void ManySortedSign ; :: thesis: for X being V5() ManySortedSet of the carrier of S holds FreeGen X is free

let X be V5() ManySortedSet of the carrier of S; :: thesis: FreeGen X is free

set D = DTConMSA X;

set FA = FreeMSA X;

set FG = FreeGen X;

let U1 be non-empty MSAlgebra over S; :: according to MSAFREE:def 5 :: thesis: for f being ManySortedFunction of FreeGen X, the Sorts of U1 ex h being ManySortedFunction of (FreeMSA X),U1 st

( h is_homomorphism FreeMSA X,U1 & h || (FreeGen X) = f )

let F be ManySortedFunction of FreeGen X, the Sorts of U1; :: thesis: ex h being ManySortedFunction of (FreeMSA X),U1 st

( h is_homomorphism FreeMSA X,U1 & h || (FreeGen X) = F )

set SA = the Sorts of (FreeMSA X);

set AR = the Arity of S;

set S1 = the Sorts of U1;

set O = the carrier' of S;

set RS = the ResultSort of S;

set DU = Union the Sorts of U1;

deffunc H_{1}( Symbol of (DTConMSA X)) -> Element of Union the Sorts of U1 = pi (F, the Sorts of U1,$1);

deffunc H_{2}( Symbol of (DTConMSA X), FinSequence, FinSequence) -> Element of Union the Sorts of U1 = pi ((@ (X,$1)),U1,$3);

consider G being Function of (TS (DTConMSA X)),(Union the Sorts of U1) such that

A1: for t being Symbol of (DTConMSA X) st t in Terminals (DTConMSA X) holds

G . (root-tree t) = H_{1}(t)
and

A2: for nt being Symbol of (DTConMSA X)

for ts being FinSequence of TS (DTConMSA X) st nt ==> roots ts holds

G . (nt -tree ts) = H_{2}(nt, roots ts,G * ts)
from DTCONSTR:sch 8();

deffunc H_{3}( object ) -> Element of bool [:(TS (DTConMSA X)),(Union the Sorts of U1):] = G | ( the Sorts of (FreeMSA X) . $1);

consider h being Function such that

A3: ( dom h = the carrier of S & ( for s being object st s in the carrier of S holds

h . s = H_{3}(s) ) )
from FUNCT_1:sch 3();

reconsider h = h as ManySortedSet of the carrier of S by A3, PARTFUN1:def 2, RELAT_1:def 18;

for s being object st s in dom h holds

h . s is Function

defpred S_{1}[ set ] means for s being SortSymbol of S st $1 in the Sorts of (FreeMSA X) . s holds

(h . s) . $1 in the Sorts of U1 . s;

A4: for nt being Symbol of (DTConMSA X)

for ts being FinSequence of TS (DTConMSA X) st nt ==> roots ts & ( for t being DecoratedTree of the carrier of (DTConMSA X) st t in rng ts holds

S_{1}[t] ) holds

S_{1}[nt -tree ts]

S_{1}[ root-tree t]

S_{1}[t]
from DTCONSTR:sch 7(A39, A4);

for s being object st s in the carrier of S holds

h . s is Function of ( the Sorts of (FreeMSA X) . s),( the Sorts of U1 . s)

take h ; :: thesis: ( h is_homomorphism FreeMSA X,U1 & h || (FreeGen X) = F )

thus h is_homomorphism FreeMSA X,U1 :: thesis: h || (FreeGen X) = F

(h || (FreeGen X)) . x = F . x

let X be V5() ManySortedSet of the carrier of S; :: thesis: FreeGen X is free

set D = DTConMSA X;

set FA = FreeMSA X;

set FG = FreeGen X;

let U1 be non-empty MSAlgebra over S; :: according to MSAFREE:def 5 :: thesis: for f being ManySortedFunction of FreeGen X, the Sorts of U1 ex h being ManySortedFunction of (FreeMSA X),U1 st

( h is_homomorphism FreeMSA X,U1 & h || (FreeGen X) = f )

let F be ManySortedFunction of FreeGen X, the Sorts of U1; :: thesis: ex h being ManySortedFunction of (FreeMSA X),U1 st

( h is_homomorphism FreeMSA X,U1 & h || (FreeGen X) = F )

set SA = the Sorts of (FreeMSA X);

set AR = the Arity of S;

set S1 = the Sorts of U1;

set O = the carrier' of S;

set RS = the ResultSort of S;

set DU = Union the Sorts of U1;

deffunc H

deffunc H

consider G being Function of (TS (DTConMSA X)),(Union the Sorts of U1) such that

A1: for t being Symbol of (DTConMSA X) st t in Terminals (DTConMSA X) holds

G . (root-tree t) = H

A2: for nt being Symbol of (DTConMSA X)

for ts being FinSequence of TS (DTConMSA X) st nt ==> roots ts holds

G . (nt -tree ts) = H

deffunc H

consider h being Function such that

A3: ( dom h = the carrier of S & ( for s being object st s in the carrier of S holds

h . s = H

reconsider h = h as ManySortedSet of the carrier of S by A3, PARTFUN1:def 2, RELAT_1:def 18;

for s being object st s in dom h holds

h . s is Function

proof

then reconsider h = h as ManySortedFunction of the carrier of S by FUNCOP_1:def 6;
let s be object ; :: thesis: ( s in dom h implies h . s is Function )

assume s in dom h ; :: thesis: h . s is Function

then h . s = G | ( the Sorts of (FreeMSA X) . s) by A3;

hence h . s is Function ; :: thesis: verum

end;assume s in dom h ; :: thesis: h . s is Function

then h . s = G | ( the Sorts of (FreeMSA X) . s) by A3;

hence h . s is Function ; :: thesis: verum

defpred S

(h . s) . $1 in the Sorts of U1 . s;

A4: for nt being Symbol of (DTConMSA X)

for ts being FinSequence of TS (DTConMSA X) st nt ==> roots ts & ( for t being DecoratedTree of the carrier of (DTConMSA X) st t in rng ts holds

S

S

proof

A39:
for t being Symbol of (DTConMSA X) st t in Terminals (DTConMSA X) holds
let nt be Symbol of (DTConMSA X); :: thesis: for ts being FinSequence of TS (DTConMSA X) st nt ==> roots ts & ( for t being DecoratedTree of the carrier of (DTConMSA X) st t in rng ts holds

S_{1}[t] ) holds

S_{1}[nt -tree ts]

let ts be FinSequence of TS (DTConMSA X); :: thesis: ( nt ==> roots ts & ( for t being DecoratedTree of the carrier of (DTConMSA X) st t in rng ts holds

S_{1}[t] ) implies S_{1}[nt -tree ts] )

assume that

A5: nt ==> roots ts and

A6: for t being DecoratedTree of the carrier of (DTConMSA X) st t in rng ts holds

S_{1}[t]
; :: thesis: S_{1}[nt -tree ts]

set p = G * ts;

set o = @ (X,nt);

set ar = the_arity_of (@ (X,nt));

set rs = the_result_sort_of (@ (X,nt));

set OU = [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X));

set rt = roots ts;

A7: [(@ (X,nt)), the carrier of S] = nt by A5, Def20;

then A8: [[(@ (X,nt)), the carrier of S],(roots ts)] in the Rules of (DTConMSA X) by A5, LANG1:def 1;

A9: [(@ (X,nt)), the carrier of S] = Sym ((@ (X,nt)),X) ;

then A10: (DenOp ((@ (X,nt)),X)) . ts = nt -tree ts by A5, A7, Def12;

dom (DenOp ((@ (X,nt)),X)) = (((FreeSort X) #) * the Arity of S) . (@ (X,nt)) by FUNCT_2:def 1;

then ts in dom (DenOp ((@ (X,nt)),X)) by A5, A7, A9, Th10;

then ( rng (DenOp ((@ (X,nt)),X)) c= ((FreeSort X) * the ResultSort of S) . (@ (X,nt)) & nt -tree ts in rng (DenOp ((@ (X,nt)),X)) ) by A10, FUNCT_1:def 3, RELAT_1:def 19;

then A11: nt -tree ts in ( the Sorts of (FreeMSA X) * the ResultSort of S) . (@ (X,nt)) ;

set ppi = pi ((@ (X,nt)),U1,(G * ts));

A12: rng the ResultSort of S c= the carrier of S by RELAT_1:def 19;

A13: rng (the_arity_of (@ (X,nt))) c= the carrier of S by FINSEQ_1:def 4;

reconsider rt = roots ts as Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * by A8, ZFMISC_1:87;

A14: len rt = len (the_arity_of (@ (X,nt))) by A8, Th5;

A15: dom rt = Seg (len rt) by FINSEQ_1:def 3;

dom the Sorts of (FreeMSA X) = the carrier of S by PARTFUN1:def 2;

then A16: dom ( the Sorts of (FreeMSA X) * (the_arity_of (@ (X,nt)))) = dom (the_arity_of (@ (X,nt))) by A13, RELAT_1:27;

A17: the_arity_of (@ (X,nt)) = the Arity of S . (@ (X,nt)) by MSUALG_1:def 1;

dom the Sorts of U1 = the carrier of S by PARTFUN1:def 2;

then A18: dom ( the Sorts of U1 * (the_arity_of (@ (X,nt)))) = dom (the_arity_of (@ (X,nt))) by A13, RELAT_1:27;

A19: ( dom rt = dom ts & Seg (len (the_arity_of (@ (X,nt)))) = dom (the_arity_of (@ (X,nt))) ) by FINSEQ_1:def 3, TREES_3:def 18;

A20: dom (G * ts) = dom ts by FINSEQ_3:120;

then A21: dom (G * ts) = dom ( the Sorts of U1 * (the_arity_of (@ (X,nt)))) by A18, A8, A15, A19, Th5;

A22: for x being object st x in dom ( the Sorts of U1 * (the_arity_of (@ (X,nt)))) holds

(G * ts) . x in ( the Sorts of U1 * (the_arity_of (@ (X,nt)))) . x

then A30: dom ( the Sorts of U1 * the ResultSort of S) = dom the ResultSort of S by A12, RELAT_1:27;

let s be SortSymbol of S; :: thesis: ( nt -tree ts in the Sorts of (FreeMSA X) . s implies (h . s) . (nt -tree ts) in the Sorts of U1 . s )

A31: dom (Den ((@ (X,nt)),U1)) = Args ((@ (X,nt)),U1) by FUNCT_2:def 1;

A32: dom the ResultSort of S = the carrier' of S by FUNCT_2:def 1;

dom the Sorts of (FreeMSA X) = the carrier of S by PARTFUN1:def 2;

then dom ( the Sorts of (FreeMSA X) * the ResultSort of S) = dom the ResultSort of S by A12, RELAT_1:27;

then nt -tree ts in the Sorts of (FreeMSA X) . ( the ResultSort of S . (@ (X,nt))) by A32, A11, FUNCT_1:12;

then A33: nt -tree ts in the Sorts of (FreeMSA X) . (the_result_sort_of (@ (X,nt))) by MSUALG_1:def 2;

Args ((@ (X,nt)),U1) = (( the Sorts of U1 #) * the Arity of S) . (@ (X,nt)) by MSUALG_1:def 4

.= product ( the Sorts of U1 * (the_arity_of (@ (X,nt)))) by A17, Th1 ;

then A34: G * ts in Args ((@ (X,nt)),U1) by A20, A18, A14, A15, A19, A22, CARD_3:9;

then pi ((@ (X,nt)),U1,(G * ts)) = (Den ((@ (X,nt)),U1)) . (G * ts) by Def21;

then ( rng (Den ((@ (X,nt)),U1)) c= Result ((@ (X,nt)),U1) & pi ((@ (X,nt)),U1,(G * ts)) in rng (Den ((@ (X,nt)),U1)) ) by A34, A31, FUNCT_1:def 3, RELAT_1:def 19;

then A35: pi ((@ (X,nt)),U1,(G * ts)) in Result ((@ (X,nt)),U1) ;

assume A36: nt -tree ts in the Sorts of (FreeMSA X) . s ; :: thesis: (h . s) . (nt -tree ts) in the Sorts of U1 . s

A37: the_result_sort_of (@ (X,nt)) = s by A33, A36, XBOOLE_0:3, Th12;

G . (nt -tree ts) = pi ((@ (X,nt)),U1,(G * ts)) by A2, A5;

then A38: pi ((@ (X,nt)),U1,(G * ts)) = (G | ( the Sorts of (FreeMSA X) . (the_result_sort_of (@ (X,nt))))) . (nt -tree ts) by A33, FUNCT_1:49;

Result ((@ (X,nt)),U1) = ( the Sorts of U1 * the ResultSort of S) . (@ (X,nt)) by MSUALG_1:def 5

.= the Sorts of U1 . ( the ResultSort of S . (@ (X,nt))) by A30, A32, FUNCT_1:12

.= the Sorts of U1 . (the_result_sort_of (@ (X,nt))) by MSUALG_1:def 2 ;

hence (h . s) . (nt -tree ts) in the Sorts of U1 . s by A3, A35, A38, A37; :: thesis: verum

end;S

S

let ts be FinSequence of TS (DTConMSA X); :: thesis: ( nt ==> roots ts & ( for t being DecoratedTree of the carrier of (DTConMSA X) st t in rng ts holds

S

assume that

A5: nt ==> roots ts and

A6: for t being DecoratedTree of the carrier of (DTConMSA X) st t in rng ts holds

S

set p = G * ts;

set o = @ (X,nt);

set ar = the_arity_of (@ (X,nt));

set rs = the_result_sort_of (@ (X,nt));

set OU = [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X));

set rt = roots ts;

A7: [(@ (X,nt)), the carrier of S] = nt by A5, Def20;

then A8: [[(@ (X,nt)), the carrier of S],(roots ts)] in the Rules of (DTConMSA X) by A5, LANG1:def 1;

A9: [(@ (X,nt)), the carrier of S] = Sym ((@ (X,nt)),X) ;

then A10: (DenOp ((@ (X,nt)),X)) . ts = nt -tree ts by A5, A7, Def12;

dom (DenOp ((@ (X,nt)),X)) = (((FreeSort X) #) * the Arity of S) . (@ (X,nt)) by FUNCT_2:def 1;

then ts in dom (DenOp ((@ (X,nt)),X)) by A5, A7, A9, Th10;

then ( rng (DenOp ((@ (X,nt)),X)) c= ((FreeSort X) * the ResultSort of S) . (@ (X,nt)) & nt -tree ts in rng (DenOp ((@ (X,nt)),X)) ) by A10, FUNCT_1:def 3, RELAT_1:def 19;

then A11: nt -tree ts in ( the Sorts of (FreeMSA X) * the ResultSort of S) . (@ (X,nt)) ;

set ppi = pi ((@ (X,nt)),U1,(G * ts));

A12: rng the ResultSort of S c= the carrier of S by RELAT_1:def 19;

A13: rng (the_arity_of (@ (X,nt))) c= the carrier of S by FINSEQ_1:def 4;

reconsider rt = roots ts as Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * by A8, ZFMISC_1:87;

A14: len rt = len (the_arity_of (@ (X,nt))) by A8, Th5;

A15: dom rt = Seg (len rt) by FINSEQ_1:def 3;

dom the Sorts of (FreeMSA X) = the carrier of S by PARTFUN1:def 2;

then A16: dom ( the Sorts of (FreeMSA X) * (the_arity_of (@ (X,nt)))) = dom (the_arity_of (@ (X,nt))) by A13, RELAT_1:27;

A17: the_arity_of (@ (X,nt)) = the Arity of S . (@ (X,nt)) by MSUALG_1:def 1;

dom the Sorts of U1 = the carrier of S by PARTFUN1:def 2;

then A18: dom ( the Sorts of U1 * (the_arity_of (@ (X,nt)))) = dom (the_arity_of (@ (X,nt))) by A13, RELAT_1:27;

A19: ( dom rt = dom ts & Seg (len (the_arity_of (@ (X,nt)))) = dom (the_arity_of (@ (X,nt))) ) by FINSEQ_1:def 3, TREES_3:def 18;

A20: dom (G * ts) = dom ts by FINSEQ_3:120;

then A21: dom (G * ts) = dom ( the Sorts of U1 * (the_arity_of (@ (X,nt)))) by A18, A8, A15, A19, Th5;

A22: for x being object st x in dom ( the Sorts of U1 * (the_arity_of (@ (X,nt)))) holds

(G * ts) . x in ( the Sorts of U1 * (the_arity_of (@ (X,nt)))) . x

proof

dom the Sorts of U1 = the carrier of S
by PARTFUN1:def 2;
let x be object ; :: thesis: ( x in dom ( the Sorts of U1 * (the_arity_of (@ (X,nt)))) implies (G * ts) . x in ( the Sorts of U1 * (the_arity_of (@ (X,nt)))) . x )

assume A23: x in dom ( the Sorts of U1 * (the_arity_of (@ (X,nt)))) ; :: thesis: (G * ts) . x in ( the Sorts of U1 * (the_arity_of (@ (X,nt)))) . x

then reconsider n = x as Nat ;

A24: ts . n in rng ts by A18, A14, A15, A19, A23, FUNCT_1:def 3;

rng ts c= TS (DTConMSA X) by FINSEQ_1:def 4;

then reconsider t = ts . n as Element of TS (DTConMSA X) by A24;

A25: (G * ts) . n = G . (ts . n) by A21, A23, FINSEQ_3:120;

(the_arity_of (@ (X,nt))) . x in rng (the_arity_of (@ (X,nt))) by A18, A23, FUNCT_1:def 3;

then reconsider s = (the_arity_of (@ (X,nt))) . x as SortSymbol of S by A13;

A26: h . s = G | ( the Sorts of (FreeMSA X) . s) by A3;

dom the Sorts of (FreeMSA X) = the carrier of S by PARTFUN1:def 2;

then A27: the Sorts of (FreeMSA X) . s in rng the Sorts of (FreeMSA X) by FUNCT_1:def 3;

dom G = TS (DTConMSA X) by FUNCT_2:def 1

.= union (rng the Sorts of (FreeMSA X)) by Th11 ;

then A28: dom (h . s) = the Sorts of (FreeMSA X) . s by A26, A27, RELAT_1:62, ZFMISC_1:74;

ts in (((FreeSort X) #) * the Arity of S) . (@ (X,nt)) by A5, A7, A9, Th10;

then ts in product ((FreeSort X) * (the_arity_of (@ (X,nt)))) by A17, Th1;

then ts . x in ((FreeSort X) * (the_arity_of (@ (X,nt)))) . x by A18, A16, A23, CARD_3:9;

then A29: ts . x in (FreeSort X) . ((the_arity_of (@ (X,nt))) . x) by A18, A16, A23, FUNCT_1:12;

then (h . s) . t in the Sorts of U1 . s by A6, A24;

then G . t in the Sorts of U1 . s by A29, A26, A28, FUNCT_1:47;

hence (G * ts) . x in ( the Sorts of U1 * (the_arity_of (@ (X,nt)))) . x by A23, A25, FUNCT_1:12; :: thesis: verum

end;assume A23: x in dom ( the Sorts of U1 * (the_arity_of (@ (X,nt)))) ; :: thesis: (G * ts) . x in ( the Sorts of U1 * (the_arity_of (@ (X,nt)))) . x

then reconsider n = x as Nat ;

A24: ts . n in rng ts by A18, A14, A15, A19, A23, FUNCT_1:def 3;

rng ts c= TS (DTConMSA X) by FINSEQ_1:def 4;

then reconsider t = ts . n as Element of TS (DTConMSA X) by A24;

A25: (G * ts) . n = G . (ts . n) by A21, A23, FINSEQ_3:120;

(the_arity_of (@ (X,nt))) . x in rng (the_arity_of (@ (X,nt))) by A18, A23, FUNCT_1:def 3;

then reconsider s = (the_arity_of (@ (X,nt))) . x as SortSymbol of S by A13;

A26: h . s = G | ( the Sorts of (FreeMSA X) . s) by A3;

dom the Sorts of (FreeMSA X) = the carrier of S by PARTFUN1:def 2;

then A27: the Sorts of (FreeMSA X) . s in rng the Sorts of (FreeMSA X) by FUNCT_1:def 3;

dom G = TS (DTConMSA X) by FUNCT_2:def 1

.= union (rng the Sorts of (FreeMSA X)) by Th11 ;

then A28: dom (h . s) = the Sorts of (FreeMSA X) . s by A26, A27, RELAT_1:62, ZFMISC_1:74;

ts in (((FreeSort X) #) * the Arity of S) . (@ (X,nt)) by A5, A7, A9, Th10;

then ts in product ((FreeSort X) * (the_arity_of (@ (X,nt)))) by A17, Th1;

then ts . x in ((FreeSort X) * (the_arity_of (@ (X,nt)))) . x by A18, A16, A23, CARD_3:9;

then A29: ts . x in (FreeSort X) . ((the_arity_of (@ (X,nt))) . x) by A18, A16, A23, FUNCT_1:12;

then (h . s) . t in the Sorts of U1 . s by A6, A24;

then G . t in the Sorts of U1 . s by A29, A26, A28, FUNCT_1:47;

hence (G * ts) . x in ( the Sorts of U1 * (the_arity_of (@ (X,nt)))) . x by A23, A25, FUNCT_1:12; :: thesis: verum

then A30: dom ( the Sorts of U1 * the ResultSort of S) = dom the ResultSort of S by A12, RELAT_1:27;

let s be SortSymbol of S; :: thesis: ( nt -tree ts in the Sorts of (FreeMSA X) . s implies (h . s) . (nt -tree ts) in the Sorts of U1 . s )

A31: dom (Den ((@ (X,nt)),U1)) = Args ((@ (X,nt)),U1) by FUNCT_2:def 1;

A32: dom the ResultSort of S = the carrier' of S by FUNCT_2:def 1;

dom the Sorts of (FreeMSA X) = the carrier of S by PARTFUN1:def 2;

then dom ( the Sorts of (FreeMSA X) * the ResultSort of S) = dom the ResultSort of S by A12, RELAT_1:27;

then nt -tree ts in the Sorts of (FreeMSA X) . ( the ResultSort of S . (@ (X,nt))) by A32, A11, FUNCT_1:12;

then A33: nt -tree ts in the Sorts of (FreeMSA X) . (the_result_sort_of (@ (X,nt))) by MSUALG_1:def 2;

Args ((@ (X,nt)),U1) = (( the Sorts of U1 #) * the Arity of S) . (@ (X,nt)) by MSUALG_1:def 4

.= product ( the Sorts of U1 * (the_arity_of (@ (X,nt)))) by A17, Th1 ;

then A34: G * ts in Args ((@ (X,nt)),U1) by A20, A18, A14, A15, A19, A22, CARD_3:9;

then pi ((@ (X,nt)),U1,(G * ts)) = (Den ((@ (X,nt)),U1)) . (G * ts) by Def21;

then ( rng (Den ((@ (X,nt)),U1)) c= Result ((@ (X,nt)),U1) & pi ((@ (X,nt)),U1,(G * ts)) in rng (Den ((@ (X,nt)),U1)) ) by A34, A31, FUNCT_1:def 3, RELAT_1:def 19;

then A35: pi ((@ (X,nt)),U1,(G * ts)) in Result ((@ (X,nt)),U1) ;

assume A36: nt -tree ts in the Sorts of (FreeMSA X) . s ; :: thesis: (h . s) . (nt -tree ts) in the Sorts of U1 . s

A37: the_result_sort_of (@ (X,nt)) = s by A33, A36, XBOOLE_0:3, Th12;

G . (nt -tree ts) = pi ((@ (X,nt)),U1,(G * ts)) by A2, A5;

then A38: pi ((@ (X,nt)),U1,(G * ts)) = (G | ( the Sorts of (FreeMSA X) . (the_result_sort_of (@ (X,nt))))) . (nt -tree ts) by A33, FUNCT_1:49;

Result ((@ (X,nt)),U1) = ( the Sorts of U1 * the ResultSort of S) . (@ (X,nt)) by MSUALG_1:def 5

.= the Sorts of U1 . ( the ResultSort of S . (@ (X,nt))) by A30, A32, FUNCT_1:12

.= the Sorts of U1 . (the_result_sort_of (@ (X,nt))) by MSUALG_1:def 2 ;

hence (h . s) . (nt -tree ts) in the Sorts of U1 . s by A3, A35, A38, A37; :: thesis: verum

S

proof

A50:
for t being DecoratedTree of the carrier of (DTConMSA X) st t in TS (DTConMSA X) holds
let t be Symbol of (DTConMSA X); :: thesis: ( t in Terminals (DTConMSA X) implies S_{1}[ root-tree t] )

assume A40: t in Terminals (DTConMSA X) ; :: thesis: S_{1}[ root-tree t]

then consider s being SortSymbol of S, x being set such that

x in X . s and

A41: t = [x,s] by Th7;

set E = { (root-tree tt) where tt is Symbol of (DTConMSA X) : ( tt in Terminals (DTConMSA X) & tt `2 = s ) } ;

set a = root-tree t;

A42: t `2 = s by A41;

then A43: root-tree t in { (root-tree tt) where tt is Symbol of (DTConMSA X) : ( tt in Terminals (DTConMSA X) & tt `2 = s ) } by A40;

let s1 be SortSymbol of S; :: thesis: ( root-tree t in the Sorts of (FreeMSA X) . s1 implies (h . s1) . (root-tree t) in the Sorts of U1 . s1 )

reconsider f = F . s as Function of ((FreeGen X) . s),( the Sorts of U1 . s) ;

A44: dom f = (FreeGen X) . s by FUNCT_2:def 1;

A45: { (root-tree tt) where tt is Symbol of (DTConMSA X) : ( tt in Terminals (DTConMSA X) & tt `2 = s ) } = FreeGen (s,X) by Th13;

then (FreeGen X) . s = { (root-tree tt) where tt is Symbol of (DTConMSA X) : ( tt in Terminals (DTConMSA X) & tt `2 = s ) } by Def16;

then A46: ( rng f c= the Sorts of U1 . s & f . (root-tree t) in rng f ) by A43, A44, FUNCT_1:def 3, RELAT_1:def 19;

assume A47: root-tree t in the Sorts of (FreeMSA X) . s1 ; :: thesis: (h . s1) . (root-tree t) in the Sorts of U1 . s1

then (h . s) . (root-tree t) = G . (root-tree t) by A43, A45, FUNCT_1:49

.= pi (F, the Sorts of U1,t) by A1, A40

.= f . (root-tree t) by A40, A42, Def19 ;

hence (h . s1) . (root-tree t) in the Sorts of U1 . s1 by A46, A48; :: thesis: verum

end;assume A40: t in Terminals (DTConMSA X) ; :: thesis: S

then consider s being SortSymbol of S, x being set such that

x in X . s and

A41: t = [x,s] by Th7;

set E = { (root-tree tt) where tt is Symbol of (DTConMSA X) : ( tt in Terminals (DTConMSA X) & tt `2 = s ) } ;

set a = root-tree t;

A42: t `2 = s by A41;

then A43: root-tree t in { (root-tree tt) where tt is Symbol of (DTConMSA X) : ( tt in Terminals (DTConMSA X) & tt `2 = s ) } by A40;

let s1 be SortSymbol of S; :: thesis: ( root-tree t in the Sorts of (FreeMSA X) . s1 implies (h . s1) . (root-tree t) in the Sorts of U1 . s1 )

reconsider f = F . s as Function of ((FreeGen X) . s),( the Sorts of U1 . s) ;

A44: dom f = (FreeGen X) . s by FUNCT_2:def 1;

A45: { (root-tree tt) where tt is Symbol of (DTConMSA X) : ( tt in Terminals (DTConMSA X) & tt `2 = s ) } = FreeGen (s,X) by Th13;

then (FreeGen X) . s = { (root-tree tt) where tt is Symbol of (DTConMSA X) : ( tt in Terminals (DTConMSA X) & tt `2 = s ) } by Def16;

then A46: ( rng f c= the Sorts of U1 . s & f . (root-tree t) in rng f ) by A43, A44, FUNCT_1:def 3, RELAT_1:def 19;

assume A47: root-tree t in the Sorts of (FreeMSA X) . s1 ; :: thesis: (h . s1) . (root-tree t) in the Sorts of U1 . s1

A48: now :: thesis: not s <> s1

h . s = G | ( the Sorts of (FreeMSA X) . s)
by A3;
root-tree t in ((FreeSort X) . s) /\ ((FreeSort X) . s1)
by A43, A45, A47, XBOOLE_0:def 4;

then A49: (FreeSort X) . s meets (FreeSort X) . s1 ;

assume s <> s1 ; :: thesis: contradiction

hence contradiction by A49, Th12; :: thesis: verum

end;then A49: (FreeSort X) . s meets (FreeSort X) . s1 ;

assume s <> s1 ; :: thesis: contradiction

hence contradiction by A49, Th12; :: thesis: verum

then (h . s) . (root-tree t) = G . (root-tree t) by A43, A45, FUNCT_1:49

.= pi (F, the Sorts of U1,t) by A1, A40

.= f . (root-tree t) by A40, A42, Def19 ;

hence (h . s1) . (root-tree t) in the Sorts of U1 . s1 by A46, A48; :: thesis: verum

S

for s being object st s in the carrier of S holds

h . s is Function of ( the Sorts of (FreeMSA X) . s),( the Sorts of U1 . s)

proof

then reconsider h = h as ManySortedFunction of (FreeMSA X),U1 by PBOOLE:def 15;
let x be object ; :: thesis: ( x in the carrier of S implies h . x is Function of ( the Sorts of (FreeMSA X) . x),( the Sorts of U1 . x) )

assume x in the carrier of S ; :: thesis: h . x is Function of ( the Sorts of (FreeMSA X) . x),( the Sorts of U1 . x)

then reconsider s = x as SortSymbol of S ;

A51: dom G = TS (DTConMSA X) by FUNCT_2:def 1

.= union (rng the Sorts of (FreeMSA X)) by Th11 ;

dom the Sorts of (FreeMSA X) = the carrier of S by PARTFUN1:def 2;

then A52: the Sorts of (FreeMSA X) . s in rng the Sorts of (FreeMSA X) by FUNCT_1:def 3;

A53: h . s = G | ( the Sorts of (FreeMSA X) . s) by A3;

then A54: dom (h . s) = the Sorts of (FreeMSA X) . s by A51, A52, RELAT_1:62, ZFMISC_1:74;

A55: the Sorts of (FreeMSA X) . s c= dom G by A51, A52, ZFMISC_1:74;

rng (h . s) c= the Sorts of U1 . s

end;assume x in the carrier of S ; :: thesis: h . x is Function of ( the Sorts of (FreeMSA X) . x),( the Sorts of U1 . x)

then reconsider s = x as SortSymbol of S ;

A51: dom G = TS (DTConMSA X) by FUNCT_2:def 1

.= union (rng the Sorts of (FreeMSA X)) by Th11 ;

dom the Sorts of (FreeMSA X) = the carrier of S by PARTFUN1:def 2;

then A52: the Sorts of (FreeMSA X) . s in rng the Sorts of (FreeMSA X) by FUNCT_1:def 3;

A53: h . s = G | ( the Sorts of (FreeMSA X) . s) by A3;

then A54: dom (h . s) = the Sorts of (FreeMSA X) . s by A51, A52, RELAT_1:62, ZFMISC_1:74;

A55: the Sorts of (FreeMSA X) . s c= dom G by A51, A52, ZFMISC_1:74;

rng (h . s) c= the Sorts of U1 . s

proof

hence
h . x is Function of ( the Sorts of (FreeMSA X) . x),( the Sorts of U1 . x)
by A54, FUNCT_2:def 1, RELSET_1:4; :: thesis: verum
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in rng (h . s) or a in the Sorts of U1 . s )

assume a in rng (h . s) ; :: thesis: a in the Sorts of U1 . s

then consider T being object such that

A56: T in dom (h . s) and

A57: (h . s) . T = a by FUNCT_1:def 3;

reconsider T = T as Element of TS (DTConMSA X) by A55, A54, A56, FUNCT_2:def 1;

T in the Sorts of (FreeMSA X) . s by A53, A51, A52, A56, RELAT_1:62, ZFMISC_1:74;

hence a in the Sorts of U1 . s by A50, A57; :: thesis: verum

end;assume a in rng (h . s) ; :: thesis: a in the Sorts of U1 . s

then consider T being object such that

A56: T in dom (h . s) and

A57: (h . s) . T = a by FUNCT_1:def 3;

reconsider T = T as Element of TS (DTConMSA X) by A55, A54, A56, FUNCT_2:def 1;

T in the Sorts of (FreeMSA X) . s by A53, A51, A52, A56, RELAT_1:62, ZFMISC_1:74;

hence a in the Sorts of U1 . s by A50, A57; :: thesis: verum

take h ; :: thesis: ( h is_homomorphism FreeMSA X,U1 & h || (FreeGen X) = F )

thus h is_homomorphism FreeMSA X,U1 :: thesis: h || (FreeGen X) = F

proof

for x being object st x in the carrier of S holds
( rng the ResultSort of S c= the carrier of S & dom the Sorts of (FreeMSA X) = the carrier of S )
by PARTFUN1:def 2, RELAT_1:def 19;

then A58: ( dom the ResultSort of S = the carrier' of S & dom ( the Sorts of (FreeMSA X) * the ResultSort of S) = dom the ResultSort of S ) by FUNCT_2:def 1, RELAT_1:27;

let o be OperSymbol of S; :: according to MSUALG_3:def 7 :: thesis: ( Args (o,(FreeMSA X)) = {} or for b_{1} being Element of Args (o,(FreeMSA X)) holds (h . (the_result_sort_of o)) . ((Den (o,(FreeMSA X))) . b_{1}) = (Den (o,U1)) . (h # b_{1}) )

assume Args (o,(FreeMSA X)) <> {} ; :: thesis: for b_{1} being Element of Args (o,(FreeMSA X)) holds (h . (the_result_sort_of o)) . ((Den (o,(FreeMSA X))) . b_{1}) = (Den (o,U1)) . (h # b_{1})

let x be Element of Args (o,(FreeMSA X)); :: thesis: (h . (the_result_sort_of o)) . ((Den (o,(FreeMSA X))) . x) = (Den (o,U1)) . (h # x)

set rs = the_result_sort_of o;

set DA = Den (o,(FreeMSA X));

set D1 = Den (o,U1);

set OU = [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X));

set ar = the_arity_of o;

A59: the_arity_of o = the Arity of S . o by MSUALG_1:def 1;

A60: Args (o,(FreeMSA X)) = (((FreeSort X) #) * the Arity of S) . o by MSUALG_1:def 4;

then reconsider p = x as FinSequence of TS (DTConMSA X) by Th8;

A61: Sym (o,X) ==> roots p by A60, Th10;

then A62: @ (X,(Sym (o,X))) = o by Def20;

A63: dom (G * p) = dom p by FINSEQ_3:120;

A64: x in (((FreeSort X) #) * the Arity of S) . o by A60;

A65: for a being object st a in dom p holds

(G * p) . a = (h # x) . a

then A75: G * p = h # x by A63, A65, FUNCT_1:2, MSUALG_3:6;

A76: h . (the_result_sort_of o) = G | ( the Sorts of (FreeMSA X) . (the_result_sort_of o)) by A3;

A77: dom (DenOp (o,X)) = (((FreeSort X) #) * the Arity of S) . o by FUNCT_2:def 1;

(DenOp (o,X)) . p = (Sym (o,X)) -tree p by A61, Def12;

then ( rng (DenOp (o,X)) c= ((FreeSort X) * the ResultSort of S) . o & (Sym (o,X)) -tree p in rng (DenOp (o,X)) ) by A60, A77, FUNCT_1:def 3, RELAT_1:def 19;

then (Sym (o,X)) -tree p in ( the Sorts of (FreeMSA X) * the ResultSort of S) . o ;

then (Sym (o,X)) -tree p in the Sorts of (FreeMSA X) . ( the ResultSort of S . o) by A58, FUNCT_1:12;

then A78: (Sym (o,X)) -tree p in the Sorts of (FreeMSA X) . (the_result_sort_of o) by MSUALG_1:def 2;

dom the Sorts of (FreeMSA X) = the carrier of S by PARTFUN1:def 2;

then A79: the Sorts of (FreeMSA X) . (the_result_sort_of o) in rng the Sorts of (FreeMSA X) by FUNCT_1:def 3;

dom G = TS (DTConMSA X) by FUNCT_2:def 1

.= union (rng the Sorts of (FreeMSA X)) by Th11 ;

then A80: dom (h . (the_result_sort_of o)) = the Sorts of (FreeMSA X) . (the_result_sort_of o) by A76, A79, RELAT_1:62, ZFMISC_1:74;

Den (o,(FreeMSA X)) = (FreeOper X) . o by MSUALG_1:def 6

.= DenOp (o,X) by Def13 ;

then (Den (o,(FreeMSA X))) . x = (Sym (o,X)) -tree p by A61, Def12;

hence (h . (the_result_sort_of o)) . ((Den (o,(FreeMSA X))) . x) = G . ((Sym (o,X)) -tree p) by A78, A76, A80, FUNCT_1:47

.= pi ((@ (X,(Sym (o,X)))),U1,(G * p)) by A2, A61

.= (Den (o,U1)) . (h # x) by A62, A75, Def21 ;

:: thesis: verum

end;then A58: ( dom the ResultSort of S = the carrier' of S & dom ( the Sorts of (FreeMSA X) * the ResultSort of S) = dom the ResultSort of S ) by FUNCT_2:def 1, RELAT_1:27;

let o be OperSymbol of S; :: according to MSUALG_3:def 7 :: thesis: ( Args (o,(FreeMSA X)) = {} or for b

assume Args (o,(FreeMSA X)) <> {} ; :: thesis: for b

let x be Element of Args (o,(FreeMSA X)); :: thesis: (h . (the_result_sort_of o)) . ((Den (o,(FreeMSA X))) . x) = (Den (o,U1)) . (h # x)

set rs = the_result_sort_of o;

set DA = Den (o,(FreeMSA X));

set D1 = Den (o,U1);

set OU = [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X));

set ar = the_arity_of o;

A59: the_arity_of o = the Arity of S . o by MSUALG_1:def 1;

A60: Args (o,(FreeMSA X)) = (((FreeSort X) #) * the Arity of S) . o by MSUALG_1:def 4;

then reconsider p = x as FinSequence of TS (DTConMSA X) by Th8;

A61: Sym (o,X) ==> roots p by A60, Th10;

then A62: @ (X,(Sym (o,X))) = o by Def20;

A63: dom (G * p) = dom p by FINSEQ_3:120;

A64: x in (((FreeSort X) #) * the Arity of S) . o by A60;

A65: for a being object st a in dom p holds

(G * p) . a = (h # x) . a

proof

dom (h # x) = dom (the_arity_of o)
by MSUALG_3:6;
( rng (the_arity_of o) c= the carrier of S & dom the Sorts of (FreeMSA X) = the carrier of S )
by FINSEQ_1:def 4, PARTFUN1:def 2;

then A66: dom ( the Sorts of (FreeMSA X) * (the_arity_of o)) = dom (the_arity_of o) by RELAT_1:27;

set rt = roots p;

let a be object ; :: thesis: ( a in dom p implies (G * p) . a = (h # x) . a )

assume A67: a in dom p ; :: thesis: (G * p) . a = (h # x) . a

then reconsider n = a as Nat ;

A68: [[o, the carrier of S],(roots p)] in the Rules of (DTConMSA X) by A61, LANG1:def 1;

then reconsider rt = roots p as Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * by ZFMISC_1:87;

A69: len rt = len (the_arity_of o) by A68, Th5;

A70: ( (G * p) . n = G . (x . n) & (h # x) . n = (h . ((the_arity_of o) /. n)) . (x . n) ) by A63, A67, FINSEQ_3:120, MSUALG_3:def 6;

A71: h . ((the_arity_of o) /. n) = G | ( the Sorts of (FreeMSA X) . ((the_arity_of o) /. n)) by A3;

A72: Seg (len rt) = dom rt by FINSEQ_1:def 3;

A73: ( dom rt = dom p & Seg (len (the_arity_of o)) = dom (the_arity_of o) ) by FINSEQ_1:def 3, TREES_3:def 18;

p in product ((FreeSort X) * (the_arity_of o)) by A64, A59, Th1;

then A74: p . n in ((FreeSort X) * (the_arity_of o)) . n by A67, A66, A69, A72, A73, CARD_3:9;

((FreeSort X) * (the_arity_of o)) . n = the Sorts of (FreeMSA X) . ((the_arity_of o) . n) by A67, A66, A69, A72, A73, FUNCT_1:12

.= the Sorts of (FreeMSA X) . ((the_arity_of o) /. n) by A67, A69, A72, A73, PARTFUN1:def 6 ;

hence (G * p) . a = (h # x) . a by A70, A71, A74, FUNCT_1:49; :: thesis: verum

end;then A66: dom ( the Sorts of (FreeMSA X) * (the_arity_of o)) = dom (the_arity_of o) by RELAT_1:27;

set rt = roots p;

let a be object ; :: thesis: ( a in dom p implies (G * p) . a = (h # x) . a )

assume A67: a in dom p ; :: thesis: (G * p) . a = (h # x) . a

then reconsider n = a as Nat ;

A68: [[o, the carrier of S],(roots p)] in the Rules of (DTConMSA X) by A61, LANG1:def 1;

then reconsider rt = roots p as Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * by ZFMISC_1:87;

A69: len rt = len (the_arity_of o) by A68, Th5;

A70: ( (G * p) . n = G . (x . n) & (h # x) . n = (h . ((the_arity_of o) /. n)) . (x . n) ) by A63, A67, FINSEQ_3:120, MSUALG_3:def 6;

A71: h . ((the_arity_of o) /. n) = G | ( the Sorts of (FreeMSA X) . ((the_arity_of o) /. n)) by A3;

A72: Seg (len rt) = dom rt by FINSEQ_1:def 3;

A73: ( dom rt = dom p & Seg (len (the_arity_of o)) = dom (the_arity_of o) ) by FINSEQ_1:def 3, TREES_3:def 18;

p in product ((FreeSort X) * (the_arity_of o)) by A64, A59, Th1;

then A74: p . n in ((FreeSort X) * (the_arity_of o)) . n by A67, A66, A69, A72, A73, CARD_3:9;

((FreeSort X) * (the_arity_of o)) . n = the Sorts of (FreeMSA X) . ((the_arity_of o) . n) by A67, A66, A69, A72, A73, FUNCT_1:12

.= the Sorts of (FreeMSA X) . ((the_arity_of o) /. n) by A67, A69, A72, A73, PARTFUN1:def 6 ;

hence (G * p) . a = (h # x) . a by A70, A71, A74, FUNCT_1:49; :: thesis: verum

then A75: G * p = h # x by A63, A65, FUNCT_1:2, MSUALG_3:6;

A76: h . (the_result_sort_of o) = G | ( the Sorts of (FreeMSA X) . (the_result_sort_of o)) by A3;

A77: dom (DenOp (o,X)) = (((FreeSort X) #) * the Arity of S) . o by FUNCT_2:def 1;

(DenOp (o,X)) . p = (Sym (o,X)) -tree p by A61, Def12;

then ( rng (DenOp (o,X)) c= ((FreeSort X) * the ResultSort of S) . o & (Sym (o,X)) -tree p in rng (DenOp (o,X)) ) by A60, A77, FUNCT_1:def 3, RELAT_1:def 19;

then (Sym (o,X)) -tree p in ( the Sorts of (FreeMSA X) * the ResultSort of S) . o ;

then (Sym (o,X)) -tree p in the Sorts of (FreeMSA X) . ( the ResultSort of S . o) by A58, FUNCT_1:12;

then A78: (Sym (o,X)) -tree p in the Sorts of (FreeMSA X) . (the_result_sort_of o) by MSUALG_1:def 2;

dom the Sorts of (FreeMSA X) = the carrier of S by PARTFUN1:def 2;

then A79: the Sorts of (FreeMSA X) . (the_result_sort_of o) in rng the Sorts of (FreeMSA X) by FUNCT_1:def 3;

dom G = TS (DTConMSA X) by FUNCT_2:def 1

.= union (rng the Sorts of (FreeMSA X)) by Th11 ;

then A80: dom (h . (the_result_sort_of o)) = the Sorts of (FreeMSA X) . (the_result_sort_of o) by A76, A79, RELAT_1:62, ZFMISC_1:74;

Den (o,(FreeMSA X)) = (FreeOper X) . o by MSUALG_1:def 6

.= DenOp (o,X) by Def13 ;

then (Den (o,(FreeMSA X))) . x = (Sym (o,X)) -tree p by A61, Def12;

hence (h . (the_result_sort_of o)) . ((Den (o,(FreeMSA X))) . x) = G . ((Sym (o,X)) -tree p) by A78, A76, A80, FUNCT_1:47

.= pi ((@ (X,(Sym (o,X)))),U1,(G * p)) by A2, A61

.= (Den (o,U1)) . (h # x) by A62, A75, Def21 ;

:: thesis: verum

(h || (FreeGen X)) . x = F . x

proof

hence
h || (FreeGen X) = F
; :: thesis: verum
set hf = h || (FreeGen X);

let x be object ; :: thesis: ( x in the carrier of S implies (h || (FreeGen X)) . x = F . x )

assume x in the carrier of S ; :: thesis: (h || (FreeGen X)) . x = F . x

then reconsider s = x as SortSymbol of S ;

A81: dom (h . s) = the Sorts of (FreeMSA X) . s by FUNCT_2:def 1;

A82: dom ((h || (FreeGen X)) . s) = (FreeGen X) . s by FUNCT_2:def 1;

A83: (FreeGen X) . s = FreeGen (s,X) by Def16;

A84: (h || (FreeGen X)) . s = (h . s) | ((FreeGen X) . s) by Def1;

A85: for a being object st a in (FreeGen X) . s holds

((h || (FreeGen X)) . s) . a = (F . s) . a

hence (h || (FreeGen X)) . x = F . x by A82, A85, FUNCT_1:2; :: thesis: verum

end;let x be object ; :: thesis: ( x in the carrier of S implies (h || (FreeGen X)) . x = F . x )

assume x in the carrier of S ; :: thesis: (h || (FreeGen X)) . x = F . x

then reconsider s = x as SortSymbol of S ;

A81: dom (h . s) = the Sorts of (FreeMSA X) . s by FUNCT_2:def 1;

A82: dom ((h || (FreeGen X)) . s) = (FreeGen X) . s by FUNCT_2:def 1;

A83: (FreeGen X) . s = FreeGen (s,X) by Def16;

A84: (h || (FreeGen X)) . s = (h . s) | ((FreeGen X) . s) by Def1;

A85: for a being object st a in (FreeGen X) . s holds

((h || (FreeGen X)) . s) . a = (F . s) . a

proof

dom (F . s) = (FreeGen X) . s
by FUNCT_2:def 1;
let a be object ; :: thesis: ( a in (FreeGen X) . s implies ((h || (FreeGen X)) . s) . a = (F . s) . a )

A86: h . s = G | ( the Sorts of (FreeMSA X) . s) by A3;

assume A87: a in (FreeGen X) . s ; :: thesis: ((h || (FreeGen X)) . s) . a = (F . s) . a

then a in { (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s ) } by A83, Th13;

then consider t being Symbol of (DTConMSA X) such that

A88: ( a = root-tree t & t in Terminals (DTConMSA X) ) and

A89: t `2 = s ;

thus ((h || (FreeGen X)) . s) . a = (h . s) . a by A84, A82, A87, FUNCT_1:47

.= G . a by A81, A83, A87, A86, FUNCT_1:47

.= pi (F, the Sorts of U1,t) by A1, A88

.= (F . s) . a by A88, A89, Def19 ; :: thesis: verum

end;A86: h . s = G | ( the Sorts of (FreeMSA X) . s) by A3;

assume A87: a in (FreeGen X) . s ; :: thesis: ((h || (FreeGen X)) . s) . a = (F . s) . a

then a in { (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s ) } by A83, Th13;

then consider t being Symbol of (DTConMSA X) such that

A88: ( a = root-tree t & t in Terminals (DTConMSA X) ) and

A89: t `2 = s ;

thus ((h || (FreeGen X)) . s) . a = (h . s) . a by A84, A82, A87, FUNCT_1:47

.= G . a by A81, A83, A87, A86, FUNCT_1:47

.= pi (F, the Sorts of U1,t) by A1, A88

.= (F . s) . a by A88, A89, Def19 ; :: thesis: verum

hence (h || (FreeGen X)) . x = F . x by A82, A85, FUNCT_1:2; :: thesis: verum