deffunc H_{1}( Element of S) -> Subset of ((FreeSort X) . $1) = FreeGen ($1,X);

set FM = FreeMSA X;

set D = DTConMSA X;

consider f being Function such that

A1: ( dom f = the carrier of S & ( for s being Element of S holds f . s = H_{1}(s) ) )
from FUNCT_1:sch 4();

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

f c= the Sorts of (FreeMSA X)

the Sorts of (GenMSAlg f) = the Sorts of (FreeMSA X)

take f ; :: thesis: for s being SortSymbol of S holds f . s = FreeGen (s,X)

thus for s being SortSymbol of S holds f . s = FreeGen (s,X) by A1; :: thesis: verum

set FM = FreeMSA X;

set D = DTConMSA X;

consider f being Function such that

A1: ( dom f = the carrier of S & ( for s being Element of S holds f . s = H

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

f c= the Sorts of (FreeMSA X)

proof

then reconsider f = f as MSSubset of (FreeMSA X) by PBOOLE:def 18;
let x be object ; :: according to PBOOLE:def 2 :: thesis: ( not x in the carrier of S or f . x c= the Sorts of (FreeMSA X) . x )

assume x in the carrier of S ; :: thesis: f . x c= the Sorts of (FreeMSA X) . x

then reconsider s = x as SortSymbol of S ;

f . s = FreeGen (s,X) by A1;

hence f . x c= the Sorts of (FreeMSA X) . x ; :: thesis: verum

end;assume x in the carrier of S ; :: thesis: f . x c= the Sorts of (FreeMSA X) . x

then reconsider s = x as SortSymbol of S ;

f . s = FreeGen (s,X) by A1;

hence f . x c= the Sorts of (FreeMSA X) . x ; :: thesis: verum

the Sorts of (GenMSAlg f) = the Sorts of (FreeMSA X)

proof

then reconsider f = f as GeneratorSet of FreeMSA X by Def4;
defpred S_{1}[ set ] means $1 in union (rng the Sorts of (GenMSAlg f));

the Sorts of (GenMSAlg f) is MSSubset of (FreeMSA X) by MSUALG_2:def 9;

then A2: the Sorts of (GenMSAlg f) c= the Sorts of (FreeMSA X) by PBOOLE:def 18;

A3: 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 s]

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

A48: union (rng the Sorts of (FreeMSA X)) c= union (rng the Sorts of (GenMSAlg f))

reconsider s = x as SortSymbol of S ;

thus the Sorts of (GenMSAlg f) . x c= the Sorts of (FreeMSA X) . x by A2; :: according to XBOOLE_0:def 10 :: thesis: the Sorts of (FreeMSA X) . x c= the Sorts of (GenMSAlg f) . x

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in the Sorts of (FreeMSA X) . x or a in the Sorts of (GenMSAlg f) . x )

assume A53: a in the Sorts of (FreeMSA X) . x ; :: thesis: a in the Sorts of (GenMSAlg f) . x

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

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

then a in union (rng the Sorts of (FreeMSA X)) by A53, TARSKI:def 4;

then consider A being set such that

A54: a in A and

A55: A in rng the Sorts of (GenMSAlg f) by A48, TARSKI:def 4;

consider b being object such that

A56: b in dom the Sorts of (GenMSAlg f) and

A57: the Sorts of (GenMSAlg f) . b = A by A55, FUNCT_1:def 3;

reconsider b = b as SortSymbol of S by A56;

end;the Sorts of (GenMSAlg f) is MSSubset of (FreeMSA X) by MSUALG_2:def 9;

then A2: the Sorts of (GenMSAlg f) c= the Sorts of (FreeMSA X) by PBOOLE:def 18;

A3: 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

A40:
for s being Symbol of (DTConMSA X) st s in Terminals (DTConMSA X) holds
set G = GenMSAlg f;

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

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

A4: nt ==> roots ts and

A5: 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]

reconsider sy = nt as Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) ;

A6: [nt,(roots ts)] in the Rules of (DTConMSA X) by A4, LANG1:def 1;

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

[sy,rt] in REL X by A4, LANG1:def 1;

then sy in [: the carrier' of S,{ the carrier of S}:] by Def7;

then consider o being OperSymbol of S, x2 being Element of { the carrier of S} such that

A7: sy = [o,x2] by DOMAIN_1:1;

set ar = the_arity_of o;

set rs = the_result_sort_of o;

A8: x2 = the carrier of S by TARSKI:def 1;

[nt,(roots ts)] in REL X by A4, LANG1:def 1;

then A9: len rt = len (the_arity_of o) by A7, A8, Th5;

reconsider B = the Sorts of (GenMSAlg f) as MSSubset of (FreeMSA X) by MSUALG_2:def 9;

A10: dom B = the carrier of S by PARTFUN1:def 2;

A11: dom (roots ts) = dom ts by TREES_3:def 18;

rng (the_arity_of o) c= the carrier of S by FINSEQ_1:def 4;

then A12: dom (B * (the_arity_of o)) = dom (the_arity_of o) by A10, RELAT_1:27;

A13: ( Seg (len rt) = dom rt & Seg (len (the_arity_of o)) = dom (the_arity_of o) ) by FINSEQ_1:def 3;

then A14: dom ts = dom (the_arity_of o) by A6, A7, A8, A11, Th5;

A15: for x being object st x in dom (B * (the_arity_of o)) holds

ts . x in (B * (the_arity_of o)) . x

set RS = the ResultSort of S;

set BH = (B #) * the Arity of S;

set O = the carrier' of S;

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

.= DenOp (o,X) by Def13 ;

A34: ( Sym (o,X) = [o, the carrier of S] & nt = [o, the carrier of S] ) by A7, TARSKI:def 1;

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

then ((B #) * the Arity of S) . o = product (B * (the_arity_of o)) by Th1;

then A35: ts in ((B #) * the Arity of S) . o by A12, A11, A9, A13, A15, CARD_3:9;

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

then ts in dom (DenOp (o,X)) by A4, A34, Th10;

then ts in (dom (DenOp (o,X))) /\ (((B #) * the Arity of S) . o) by A35, XBOOLE_0:def 4;

then A36: ts in dom ((DenOp (o,X)) | (((B #) * the Arity of S) . o)) by RELAT_1:61;

then ((DenOp (o,X)) | (((B #) * the Arity of S) . o)) . ts = (DenOp (o,X)) . ts by FUNCT_1:47

.= nt -tree ts by A4, A34, Def12 ;

then A37: nt -tree ts in rng ((Den (o,(FreeMSA X))) | (((B #) * the Arity of S) . o)) by A33, A36, FUNCT_1:def 3;

( the ResultSort of S . o = the_result_sort_of o & dom (B * the ResultSort of S) = the carrier' of S ) by MSUALG_1:def 2, PARTFUN1:def 2;

then A38: (B * the ResultSort of S) . o = B . (the_result_sort_of o) by FUNCT_1:12;

B is opers_closed by MSUALG_2:def 9;

then B is_closed_on o by MSUALG_2:def 6;

then A39: rng ((Den (o,(FreeMSA X))) | (((B #) * the Arity of S) . o)) c= (B * the ResultSort of S) . o by MSUALG_2:def 5;

B . (the_result_sort_of o) in rng B by A10, FUNCT_1:def 3;

hence S_{1}[nt -tree ts]
by A39, A37, A38, TARSKI:def 4; :: thesis: verum

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

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

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

A4: nt ==> roots ts and

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

S

reconsider sy = nt as Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) ;

A6: [nt,(roots ts)] in the Rules of (DTConMSA X) by A4, LANG1:def 1;

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

[sy,rt] in REL X by A4, LANG1:def 1;

then sy in [: the carrier' of S,{ the carrier of S}:] by Def7;

then consider o being OperSymbol of S, x2 being Element of { the carrier of S} such that

A7: sy = [o,x2] by DOMAIN_1:1;

set ar = the_arity_of o;

set rs = the_result_sort_of o;

A8: x2 = the carrier of S by TARSKI:def 1;

[nt,(roots ts)] in REL X by A4, LANG1:def 1;

then A9: len rt = len (the_arity_of o) by A7, A8, Th5;

reconsider B = the Sorts of (GenMSAlg f) as MSSubset of (FreeMSA X) by MSUALG_2:def 9;

A10: dom B = the carrier of S by PARTFUN1:def 2;

A11: dom (roots ts) = dom ts by TREES_3:def 18;

rng (the_arity_of o) c= the carrier of S by FINSEQ_1:def 4;

then A12: dom (B * (the_arity_of o)) = dom (the_arity_of o) by A10, RELAT_1:27;

A13: ( Seg (len rt) = dom rt & Seg (len (the_arity_of o)) = dom (the_arity_of o) ) by FINSEQ_1:def 3;

then A14: dom ts = dom (the_arity_of o) by A6, A7, A8, A11, Th5;

A15: for x being object st x in dom (B * (the_arity_of o)) holds

ts . x in (B * (the_arity_of o)) . x

proof

set AR = the Arity of S;
let x be object ; :: thesis: ( x in dom (B * (the_arity_of o)) implies ts . x in (B * (the_arity_of o)) . x )

assume A16: x in dom (B * (the_arity_of o)) ; :: thesis: ts . x in (B * (the_arity_of o)) . x

then reconsider n = x as Nat ;

A17: ts . n in rng ts by A12, A11, A9, A13, A16, FUNCT_1:def 3;

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

then reconsider T = ts . x as Element of TS (DTConMSA X) by A17;

S_{1}[T]
by A5, A17;

then consider A being set such that

A18: T in A and

A19: A in rng the Sorts of (GenMSAlg f) by TARSKI:def 4;

set b = (the_arity_of o) /. n;

set A1 = { a where a is Element of TS (DTConMSA X) : ( ex x being set st

( x in X . ((the_arity_of o) /. n) & a = root-tree [x,((the_arity_of o) /. n)] ) or ex o being OperSymbol of S st

( [o, the carrier of S] = a . {} & the_result_sort_of o = (the_arity_of o) /. n ) ) } ;

A20: { a where a is Element of TS (DTConMSA X) : ( ex x being set st

( x in X . ((the_arity_of o) /. n) & a = root-tree [x,((the_arity_of o) /. n)] ) or ex o being OperSymbol of S st

( [o, the carrier of S] = a . {} & the_result_sort_of o = (the_arity_of o) /. n ) ) } = FreeSort (X,((the_arity_of o) /. n))

.= (FreeSort X) . ((the_arity_of o) /. n) by Def11 ;

A21: ex t being DecoratedTree st

( t = ts . n & rt . n = t . {} ) by A12, A11, A9, A13, A16, TREES_3:def 18;

consider s being object such that

A22: s in dom the Sorts of (GenMSAlg f) and

A23: the Sorts of (GenMSAlg f) . s = A by A19, FUNCT_1:def 3;

reconsider s = s as SortSymbol of S by A22;

A24: ( rng rt c= [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) & rt . n in rng rt ) by A12, A9, A13, A16, FINSEQ_1:def 4, FUNCT_1:def 3;

.= B . ((the_arity_of o) /. n) by A12, A16, PARTFUN1:def 6 ;

hence ts . x in (B * (the_arity_of o)) . x by A18, A23, A31; :: thesis: verum

end;assume A16: x in dom (B * (the_arity_of o)) ; :: thesis: ts . x in (B * (the_arity_of o)) . x

then reconsider n = x as Nat ;

A17: ts . n in rng ts by A12, A11, A9, A13, A16, FUNCT_1:def 3;

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

then reconsider T = ts . x as Element of TS (DTConMSA X) by A17;

S

then consider A being set such that

A18: T in A and

A19: A in rng the Sorts of (GenMSAlg f) by TARSKI:def 4;

set b = (the_arity_of o) /. n;

set A1 = { a where a is Element of TS (DTConMSA X) : ( ex x being set st

( x in X . ((the_arity_of o) /. n) & a = root-tree [x,((the_arity_of o) /. n)] ) or ex o being OperSymbol of S st

( [o, the carrier of S] = a . {} & the_result_sort_of o = (the_arity_of o) /. n ) ) } ;

A20: { a where a is Element of TS (DTConMSA X) : ( ex x being set st

( x in X . ((the_arity_of o) /. n) & a = root-tree [x,((the_arity_of o) /. n)] ) or ex o being OperSymbol of S st

( [o, the carrier of S] = a . {} & the_result_sort_of o = (the_arity_of o) /. n ) ) } = FreeSort (X,((the_arity_of o) /. n))

.= (FreeSort X) . ((the_arity_of o) /. n) by Def11 ;

A21: ex t being DecoratedTree st

( t = ts . n & rt . n = t . {} ) by A12, A11, A9, A13, A16, TREES_3:def 18;

consider s being object such that

A22: s in dom the Sorts of (GenMSAlg f) and

A23: the Sorts of (GenMSAlg f) . s = A by A19, FUNCT_1:def 3;

reconsider s = s as SortSymbol of S by A22;

A24: ( rng rt c= [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X)) & rt . n in rng rt ) by A12, A9, A13, A16, FINSEQ_1:def 4, FUNCT_1:def 3;

A25: now :: thesis: T in (FreeSort X) . ((the_arity_of o) /. n)end;

per cases
( rt . n in [: the carrier' of S,{ the carrier of S}:] or rt . n in Union (coprod X) )
by A24, XBOOLE_0:def 3;

end;

suppose A26:
rt . n in [: the carrier' of S,{ the carrier of S}:]
; :: thesis: T in (FreeSort X) . ((the_arity_of o) /. n)

then consider o1 being OperSymbol of S, x2 being Element of { the carrier of S} such that

A27: rt . n = [o1,x2] by DOMAIN_1:1;

A28: x2 = the carrier of S by TARSKI:def 1;

then the_result_sort_of o1 = (the_arity_of o) . n by A6, A7, A8, A12, A11, A14, A16, A26, A27, Th5

.= (the_arity_of o) /. n by A12, A16, PARTFUN1:def 6 ;

hence T in (FreeSort X) . ((the_arity_of o) /. n) by A20, A21, A27, A28; :: thesis: verum

end;A27: rt . n = [o1,x2] by DOMAIN_1:1;

A28: x2 = the carrier of S by TARSKI:def 1;

then the_result_sort_of o1 = (the_arity_of o) . n by A6, A7, A8, A12, A11, A14, A16, A26, A27, Th5

.= (the_arity_of o) /. n by A12, A16, PARTFUN1:def 6 ;

hence T in (FreeSort X) . ((the_arity_of o) /. n) by A20, A21, A27, A28; :: thesis: verum

suppose A29:
rt . n in Union (coprod X)
; :: thesis: T in (FreeSort X) . ((the_arity_of o) /. n)

then
rt . n in coprod (((the_arity_of o) . n),X)
by A6, A7, A8, A12, A11, A14, A16, Th5;

then rt . n in coprod (((the_arity_of o) /. n),X) by A12, A16, PARTFUN1:def 6;

then A30: ex a being set st

( a in X . ((the_arity_of o) /. n) & rt . n = [a,((the_arity_of o) /. n)] ) by Def2;

reconsider tt = rt . n as Terminal of (DTConMSA X) by A29, Th6;

T = root-tree tt by A21, DTCONSTR:9;

hence T in (FreeSort X) . ((the_arity_of o) /. n) by A20, A30; :: thesis: verum

end;then rt . n in coprod (((the_arity_of o) /. n),X) by A12, A16, PARTFUN1:def 6;

then A30: ex a being set st

( a in X . ((the_arity_of o) /. n) & rt . n = [a,((the_arity_of o) /. n)] ) by Def2;

reconsider tt = rt . n as Terminal of (DTConMSA X) by A29, Th6;

T = root-tree tt by A21, DTCONSTR:9;

hence T in (FreeSort X) . ((the_arity_of o) /. n) by A20, A30; :: thesis: verum

A31: now :: thesis: not (the_arity_of o) /. n <> s

(B * (the_arity_of o)) . x =
B . ((the_arity_of o) . n)
by A16, FUNCT_1:12
assume
(the_arity_of o) /. n <> s
; :: thesis: contradiction

then A32: (FreeSort X) . s misses (FreeSort X) . ((the_arity_of o) /. n) by Th12;

the Sorts of (GenMSAlg f) . s c= the Sorts of (FreeMSA X) . s by A2;

hence contradiction by A18, A23, A25, A32, XBOOLE_0:3; :: thesis: verum

end;then A32: (FreeSort X) . s misses (FreeSort X) . ((the_arity_of o) /. n) by Th12;

the Sorts of (GenMSAlg f) . s c= the Sorts of (FreeMSA X) . s by A2;

hence contradiction by A18, A23, A25, A32, XBOOLE_0:3; :: thesis: verum

.= B . ((the_arity_of o) /. n) by A12, A16, PARTFUN1:def 6 ;

hence ts . x in (B * (the_arity_of o)) . x by A18, A23, A31; :: thesis: verum

set RS = the ResultSort of S;

set BH = (B #) * the Arity of S;

set O = the carrier' of S;

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

.= DenOp (o,X) by Def13 ;

A34: ( Sym (o,X) = [o, the carrier of S] & nt = [o, the carrier of S] ) by A7, TARSKI:def 1;

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

then ((B #) * the Arity of S) . o = product (B * (the_arity_of o)) by Th1;

then A35: ts in ((B #) * the Arity of S) . o by A12, A11, A9, A13, A15, CARD_3:9;

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

then ts in dom (DenOp (o,X)) by A4, A34, Th10;

then ts in (dom (DenOp (o,X))) /\ (((B #) * the Arity of S) . o) by A35, XBOOLE_0:def 4;

then A36: ts in dom ((DenOp (o,X)) | (((B #) * the Arity of S) . o)) by RELAT_1:61;

then ((DenOp (o,X)) | (((B #) * the Arity of S) . o)) . ts = (DenOp (o,X)) . ts by FUNCT_1:47

.= nt -tree ts by A4, A34, Def12 ;

then A37: nt -tree ts in rng ((Den (o,(FreeMSA X))) | (((B #) * the Arity of S) . o)) by A33, A36, FUNCT_1:def 3;

( the ResultSort of S . o = the_result_sort_of o & dom (B * the ResultSort of S) = the carrier' of S ) by MSUALG_1:def 2, PARTFUN1:def 2;

then A38: (B * the ResultSort of S) . o = B . (the_result_sort_of o) by FUNCT_1:12;

B is opers_closed by MSUALG_2:def 9;

then B is_closed_on o by MSUALG_2:def 6;

then A39: rng ((Den (o,(FreeMSA X))) | (((B #) * the Arity of S) . o)) c= (B * the ResultSort of S) . o by MSUALG_2:def 5;

B . (the_result_sort_of o) in rng B by A10, FUNCT_1:def 3;

hence S

S

proof

A47:
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 t in Terminals (DTConMSA X) ; :: thesis: S_{1}[ root-tree t]

then t in Union (coprod X) by Th6;

then t in union (rng (coprod X)) by CARD_3:def 4;

then consider A being set such that

A41: t in A and

A42: A in rng (coprod X) by TARSKI:def 4;

consider s being object such that

A43: s in dom (coprod X) and

A44: (coprod X) . s = A by A42, FUNCT_1:def 3;

reconsider s = s as SortSymbol of S by A43;

A = coprod (s,X) by A44, Def3;

then ex a being set st

( a in X . s & t = [a,s] ) by A41, Def2;

then A45: root-tree t in FreeGen (s,X) by Def15;

f is MSSubset of (GenMSAlg f) by MSUALG_2:def 17;

then f c= the Sorts of (GenMSAlg f) by PBOOLE:def 18;

then f . s c= the Sorts of (GenMSAlg f) . s ;

then A46: FreeGen (s,X) c= the Sorts of (GenMSAlg f) . s by A1;

dom the Sorts of (GenMSAlg f) = the carrier of S by PARTFUN1:def 2;

then the Sorts of (GenMSAlg f) . s in rng the Sorts of (GenMSAlg f) by FUNCT_1:def 3;

hence S_{1}[ root-tree t]
by A46, A45, TARSKI:def 4; :: thesis: verum

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

then t in Union (coprod X) by Th6;

then t in union (rng (coprod X)) by CARD_3:def 4;

then consider A being set such that

A41: t in A and

A42: A in rng (coprod X) by TARSKI:def 4;

consider s being object such that

A43: s in dom (coprod X) and

A44: (coprod X) . s = A by A42, FUNCT_1:def 3;

reconsider s = s as SortSymbol of S by A43;

A = coprod (s,X) by A44, Def3;

then ex a being set st

( a in X . s & t = [a,s] ) by A41, Def2;

then A45: root-tree t in FreeGen (s,X) by Def15;

f is MSSubset of (GenMSAlg f) by MSUALG_2:def 17;

then f c= the Sorts of (GenMSAlg f) by PBOOLE:def 18;

then f . s c= the Sorts of (GenMSAlg f) . s ;

then A46: FreeGen (s,X) c= the Sorts of (GenMSAlg f) . s by A1;

dom the Sorts of (GenMSAlg f) = the carrier of S by PARTFUN1:def 2;

then the Sorts of (GenMSAlg f) . s in rng the Sorts of (GenMSAlg f) by FUNCT_1:def 3;

hence S

S

A48: union (rng the Sorts of (FreeMSA X)) c= union (rng the Sorts of (GenMSAlg f))

proof

let x be Element of S; :: according to PBOOLE:def 21 :: thesis: the Sorts of (GenMSAlg f) . x = the Sorts of (FreeMSA X) . x
set D = DTConMSA X;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union (rng the Sorts of (FreeMSA X)) or x in union (rng the Sorts of (GenMSAlg f)) )

assume x in union (rng the Sorts of (FreeMSA X)) ; :: thesis: x in union (rng the Sorts of (GenMSAlg f))

then consider A being set such that

A49: x in A and

A50: A in rng the Sorts of (FreeMSA X) by TARSKI:def 4;

consider s being object such that

A51: s in dom (FreeSort X) and

A52: (FreeSort X) . s = A by A50, FUNCT_1:def 3;

reconsider s = s as SortSymbol of S by A51;

A = FreeSort (X,s) by A52, Def11

.= { a where a is Element of TS (DTConMSA X) : ( ex x being set st

( x in X . s & a = root-tree [x,s] ) or ex o1 being OperSymbol of S st

( [o1, the carrier of S] = a . {} & the_result_sort_of o1 = s ) ) } ;

then ex a being Element of TS (DTConMSA X) st

( a = x & ( ex x being set st

( x in X . s & a = root-tree [x,s] ) or ex o1 being OperSymbol of S st

( [o1, the carrier of S] = a . {} & the_result_sort_of o1 = s ) ) ) by A49;

hence x in union (rng the Sorts of (GenMSAlg f)) by A47; :: thesis: verum

end;let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union (rng the Sorts of (FreeMSA X)) or x in union (rng the Sorts of (GenMSAlg f)) )

assume x in union (rng the Sorts of (FreeMSA X)) ; :: thesis: x in union (rng the Sorts of (GenMSAlg f))

then consider A being set such that

A49: x in A and

A50: A in rng the Sorts of (FreeMSA X) by TARSKI:def 4;

consider s being object such that

A51: s in dom (FreeSort X) and

A52: (FreeSort X) . s = A by A50, FUNCT_1:def 3;

reconsider s = s as SortSymbol of S by A51;

A = FreeSort (X,s) by A52, Def11

.= { a where a is Element of TS (DTConMSA X) : ( ex x being set st

( x in X . s & a = root-tree [x,s] ) or ex o1 being OperSymbol of S st

( [o1, the carrier of S] = a . {} & the_result_sort_of o1 = s ) ) } ;

then ex a being Element of TS (DTConMSA X) st

( a = x & ( ex x being set st

( x in X . s & a = root-tree [x,s] ) or ex o1 being OperSymbol of S st

( [o1, the carrier of S] = a . {} & the_result_sort_of o1 = s ) ) ) by A49;

hence x in union (rng the Sorts of (GenMSAlg f)) by A47; :: thesis: verum

reconsider s = x as SortSymbol of S ;

thus the Sorts of (GenMSAlg f) . x c= the Sorts of (FreeMSA X) . x by A2; :: according to XBOOLE_0:def 10 :: thesis: the Sorts of (FreeMSA X) . x c= the Sorts of (GenMSAlg f) . x

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in the Sorts of (FreeMSA X) . x or a in the Sorts of (GenMSAlg f) . x )

assume A53: a in the Sorts of (FreeMSA X) . x ; :: thesis: a in the Sorts of (GenMSAlg f) . x

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

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

then a in union (rng the Sorts of (FreeMSA X)) by A53, TARSKI:def 4;

then consider A being set such that

A54: a in A and

A55: A in rng the Sorts of (GenMSAlg f) by A48, TARSKI:def 4;

consider b being object such that

A56: b in dom the Sorts of (GenMSAlg f) and

A57: the Sorts of (GenMSAlg f) . b = A by A55, FUNCT_1:def 3;

reconsider b = b as SortSymbol of S by A56;

now :: thesis: not b <> s

hence
a in the Sorts of (GenMSAlg f) . x
by A54, A57; :: thesis: verumassume
b <> s
; :: thesis: contradiction

then (FreeSort X) . s misses (FreeSort X) . b by Th12;

then A58: ((FreeSort X) . s) /\ ((FreeSort X) . b) = {} ;

the Sorts of (GenMSAlg f) . b c= the Sorts of (FreeMSA X) . b by A2;

hence contradiction by A53, A54, A57, A58, XBOOLE_0:def 4; :: thesis: verum

end;then (FreeSort X) . s misses (FreeSort X) . b by Th12;

then A58: ((FreeSort X) . s) /\ ((FreeSort X) . b) = {} ;

the Sorts of (GenMSAlg f) . b c= the Sorts of (FreeMSA X) . b by A2;

hence contradiction by A53, A54, A57, A58, XBOOLE_0:def 4; :: thesis: verum

take f ; :: thesis: for s being SortSymbol of S holds f . s = FreeGen (s,X)

thus for s being SortSymbol of S holds f . s = FreeGen (s,X) by A1; :: thesis: verum