deffunc H1( Element of S) -> Subset of (() . \$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 = H1(s) ) ) from reconsider f = f as ManySortedSet of the carrier of S by ;
f c= the Sorts of ()
proof
let x be object ; :: according to PBOOLE:def 2 :: thesis: ( not x in the carrier of S or f . x c= the Sorts of () . x )
assume x in the carrier of S ; :: thesis: f . x c= the Sorts of () . x
then reconsider s = x as SortSymbol of S ;
f . s = FreeGen (s,X) by A1;
hence f . x c= the Sorts of () . x ; :: thesis: verum
end;
then reconsider f = f as MSSubset of () by PBOOLE:def 18;
the Sorts of () = the Sorts of ()
proof
defpred S1[ set ] means \$1 in union (rng the Sorts of ());
the Sorts of () is MSSubset of () by MSUALG_2:def 9;
then A2: the Sorts of () c= the Sorts of () by PBOOLE:def 18;
A3: for nt being Symbol of ()
for ts being FinSequence of TS () st nt ==> roots ts & ( for t being DecoratedTree of the carrier of () st t in rng ts holds
S1[t] ) holds
S1[nt -tree ts]
proof
set G = GenMSAlg f;
set OU = [: the carrier' of S,{ the carrier of S}:] \/ (Union ());
let nt be Symbol of (); :: thesis: for ts being FinSequence of TS () st nt ==> roots ts & ( for t being DecoratedTree of the carrier of () st t in rng ts holds
S1[t] ) holds
S1[nt -tree ts]

let ts be FinSequence of TS (); :: thesis: ( nt ==> roots ts & ( for t being DecoratedTree of the carrier of () st t in rng ts holds
S1[t] ) implies S1[nt -tree ts] )

assume that
A4: nt ==> roots ts and
A5: for t being DecoratedTree of the carrier of () st t in rng ts holds
S1[t] ; :: thesis: S1[nt -tree ts]
reconsider sy = nt as Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union ()) ;
A6: [nt,(roots ts)] in the Rules of () by ;
then reconsider rt = roots ts as Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union ())) * by ZFMISC_1:87;
[sy,rt] in REL X by ;
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 ;
then A9: len rt = len () by A7, A8, Th5;
reconsider B = the Sorts of () as MSSubset of () 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 () c= the carrier of S by FINSEQ_1:def 4;
then A12: dom (B * ()) = dom () by ;
A13: ( Seg (len rt) = dom rt & Seg (len ()) = dom () ) by FINSEQ_1:def 3;
then A14: dom ts = dom () by A6, A7, A8, A11, Th5;
A15: for x being object st x in dom (B * ()) holds
ts . x in (B * ()) . x
proof
let x be object ; :: thesis: ( x in dom (B * ()) implies ts . x in (B * ()) . x )
assume A16: x in dom (B * ()) ; :: thesis: ts . x in (B * ()) . x
then reconsider n = x as Nat ;
A17: ts . n in rng ts by ;
rng ts c= TS () by FINSEQ_1:def 4;
then reconsider T = ts . x as Element of TS () by A17;
S1[T] by A5, A17;
then consider A being set such that
A18: T in A and
A19: A in rng the Sorts of () by TARSKI:def 4;
set b = () /. n;
set A1 = { a where a is Element of TS () : ( ex x being set st
( x in X . (() /. n) & a = root-tree [x,(() /. n)] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a . {} & the_result_sort_of o = () /. n ) )
}
;
A20: { a where a is Element of TS () : ( ex x being set st
( x in X . (() /. n) & a = root-tree [x,(() /. n)] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a . {} & the_result_sort_of o = () /. n ) )
}
= FreeSort (X,(() /. n))
.= () . (() /. n) by Def11 ;
A21: ex t being DecoratedTree st
( t = ts . n & rt . n = t . {} ) by ;
consider s being object such that
A22: s in dom the Sorts of () and
A23: the Sorts of () . s = A by ;
reconsider s = s as SortSymbol of S by A22;
A24: ( rng rt c= [: the carrier' of S,{ the carrier of S}:] \/ (Union ()) & rt . n in rng rt ) by ;
A25: now :: thesis: T in () . (() /. n)
per cases ( rt . n in [: the carrier' of S,{ the carrier of S}:] or rt . n in Union () ) by ;
suppose A26: rt . n in [: the carrier' of S,{ the carrier of S}:] ; :: thesis: T in () . (() /. 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 = () . n by A6, A7, A8, A12, A11, A14, A16, A26, A27, Th5
.= () /. n by ;
hence T in () . (() /. n) by A20, A21, A27, A28; :: thesis: verum
end;
suppose A29: rt . n in Union () ; :: thesis: T in () . (() /. n)
then rt . n in coprod ((() . n),X) by A6, A7, A8, A12, A11, A14, A16, Th5;
then rt . n in coprod ((() /. n),X) by ;
then A30: ex a being set st
( a in X . (() /. n) & rt . n = [a,(() /. n)] ) by Def2;
reconsider tt = rt . n as Terminal of () by ;
T = root-tree tt by ;
hence T in () . (() /. n) by ; :: thesis: verum
end;
end;
end;
A31: now :: thesis: not () /. n <> s
assume (the_arity_of o) /. n <> s ; :: thesis: contradiction
then A32: (FreeSort X) . s misses () . (() /. n) by Th12;
the Sorts of () . s c= the Sorts of () . s by A2;
hence contradiction by A18, A23, A25, A32, XBOOLE_0:3; :: thesis: verum
end;
(B * ()) . x = B . (() . n) by
.= B . (() /. n) by ;
hence ts . x in (B * ()) . x by ; :: thesis: verum
end;
set AR = the Arity of S;
set RS = the ResultSort of S;
set BH = (B #) * the Arity of S;
set O = the carrier' of S;
A33: Den (o,()) = () . 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 ;
the Arity of S . o = the_arity_of o by MSUALG_1:def 1;
then ((B #) * the Arity of S) . o = product (B * ()) by Th1;
then A35: ts in ((B #) * the Arity of S) . o by ;
dom (DenOp (o,X)) = ((() #) * the Arity of S) . o by FUNCT_2:def 1;
then ts in dom (DenOp (o,X)) by ;
then ts in (dom (DenOp (o,X))) /\ (((B #) * the Arity of S) . o) by ;
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 ;
then A37: nt -tree ts in rng ((Den (o,())) | (((B #) * the Arity of S) . o)) by ;
( the ResultSort of S . o = the_result_sort_of o & dom (B * the ResultSort of S) = the carrier' of S ) by ;
then A38: (B * the ResultSort of S) . o = B . 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,())) | (((B #) * the Arity of S) . o)) c= (B * the ResultSort of S) . o by MSUALG_2:def 5;
B . in rng B by ;
hence S1[nt -tree ts] by ; :: thesis: verum
end;
A40: for s being Symbol of () st s in Terminals () holds
S1[ root-tree s]
proof
let t be Symbol of (); :: thesis: ( t in Terminals () implies S1[ root-tree t] )
assume t in Terminals () ; :: thesis: S1[ root-tree t]
then t in Union () by Th6;
then t in union (rng ()) by CARD_3:def 4;
then consider A being set such that
A41: t in A and
A42: A in rng () by TARSKI:def 4;
consider s being object such that
A43: s in dom () and
A44: (coprod X) . s = A by ;
reconsider s = s as SortSymbol of S by A43;
A = coprod (s,X) by ;
then ex a being set st
( a in X . s & t = [a,s] ) by ;
then A45: root-tree t in FreeGen (s,X) by Def15;
f is MSSubset of () by MSUALG_2:def 17;
then f c= the Sorts of () by PBOOLE:def 18;
then f . s c= the Sorts of () . s ;
then A46: FreeGen (s,X) c= the Sorts of () . s by A1;
dom the Sorts of () = the carrier of S by PARTFUN1:def 2;
then the Sorts of () . s in rng the Sorts of () by FUNCT_1:def 3;
hence S1[ root-tree t] by ; :: thesis: verum
end;
A47: for t being DecoratedTree of the carrier of () st t in TS () holds
S1[t] from A48: union (rng the Sorts of ()) c= union (rng the Sorts of ())
proof
set D = DTConMSA X;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union (rng the Sorts of ()) or x in union (rng the Sorts of ()) )
assume x in union (rng the Sorts of ()) ; :: thesis: x in union (rng the Sorts of ())
then consider A being set such that
A49: x in A and
A50: A in rng the Sorts of () by TARSKI:def 4;
consider s being object such that
A51: s in dom () and
A52: (FreeSort X) . s = A by ;
reconsider s = s as SortSymbol of S by A51;
A = FreeSort (X,s) by
.= { a where a is Element of TS () : ( 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 () 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 ()) by A47; :: thesis: verum
end;
let x be Element of S; :: according to PBOOLE:def 21 :: thesis: the Sorts of () . x = the Sorts of () . x
reconsider s = x as SortSymbol of S ;
thus the Sorts of () . x c= the Sorts of () . x by A2; :: according to XBOOLE_0:def 10 :: thesis: the Sorts of () . x c= the Sorts of () . x
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in the Sorts of () . x or a in the Sorts of () . x )
assume A53: a in the Sorts of () . x ; :: thesis: a in the Sorts of () . x
the carrier of S = dom the Sorts of () by PARTFUN1:def 2;
then the Sorts of () . s in rng the Sorts of () by FUNCT_1:def 3;
then a in union (rng the Sorts of ()) by ;
then consider A being set such that
A54: a in A and
A55: A in rng the Sorts of () by ;
consider b being object such that
A56: b in dom the Sorts of () and
A57: the Sorts of () . b = A by ;
reconsider b = b as SortSymbol of S by A56;
now :: thesis: not b <> s
assume b <> s ; :: thesis: contradiction
then (FreeSort X) . s misses () . b by Th12;
then A58: ((FreeSort X) . s) /\ (() . b) = {} ;
the Sorts of () . b c= the Sorts of () . b by A2;
hence contradiction by A53, A54, A57, A58, XBOOLE_0:def 4; :: thesis: verum
end;
hence a in the Sorts of () . x by ; :: thesis: verum
end;
then reconsider f = f as GeneratorSet of FreeMSA X by Def4;
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