reconsider A = FreeGen the Sorts of MSA as free GeneratorSet of FreeEnv MSA by MSAFREE:16;
defpred S1[ object , object ] means ex s being SortSymbol of S ex f being Function of (A . s),( the Sorts of MSA . s) st
( f = \$2 & s = \$1 & ( for x, y being set st y in A . s & y = root-tree [x,s] & x in the Sorts of MSA . s holds
f . y = x ) );
A1: for i being object st i in the carrier of S holds
ex j being object st S1[i,j]
proof
let i be object ; :: thesis: ( i in the carrier of S implies ex j being object st S1[i,j] )
assume i in the carrier of S ; :: thesis: ex j being object st S1[i,j]
then reconsider s = i as SortSymbol of S ;
defpred S2[ object , object ] means \$1 = root-tree [\$2,s];
A2: for e being object st e in A . s holds
ex u being object st
( u in the Sorts of MSA . s & S2[e,u] )
proof
let e be object ; :: thesis: ( e in A . s implies ex u being object st
( u in the Sorts of MSA . s & S2[e,u] ) )

assume e in A . s ; :: thesis: ex u being object st
( u in the Sorts of MSA . s & S2[e,u] )

then e in FreeGen (s, the Sorts of MSA) by MSAFREE:def 16;
then consider a being set such that
A3: ( a in the Sorts of MSA . s & e = root-tree [a,s] ) by MSAFREE:def 15;
thus ex u being object st
( u in the Sorts of MSA . s & S2[e,u] ) by A3; :: thesis: verum
end;
consider j being Function such that
A4: ( dom j = A . s & rng j c= the Sorts of MSA . s & ( for e being object st e in A . s holds
S2[e,j . e] ) ) from reconsider f = j as Function of (A . s),( the Sorts of MSA . s) by ;
take j ; :: thesis: S1[i,j]
take s ; :: thesis: ex f being Function of (A . s),( the Sorts of MSA . s) st
( f = j & s = i & ( for x, y being set st y in A . s & y = root-tree [x,s] & x in the Sorts of MSA . s holds
f . y = x ) )

take f ; :: thesis: ( f = j & s = i & ( for x, y being set st y in A . s & y = root-tree [x,s] & x in the Sorts of MSA . s holds
f . y = x ) )

thus ( f = j & s = i ) ; :: thesis: for x, y being set st y in A . s & y = root-tree [x,s] & x in the Sorts of MSA . s holds
f . y = x

let x, y be set ; :: thesis: ( y in A . s & y = root-tree [x,s] & x in the Sorts of MSA . s implies f . y = x )
assume that
A5: y in A . s and
A6: y = root-tree [x,s] and
x in the Sorts of MSA . s ; :: thesis: f . y = x
y = root-tree [(j . y),s] by A4, A5;
then [x,s] = [(j . y),s] by ;
hence f . y = x by XTUPLE_0:1; :: thesis: verum
end;
consider f being ManySortedSet of the carrier of S such that
A7: for i being object st i in the carrier of S holds
S1[i,f . i] from
now :: thesis: for x being object st x in dom f holds
f . x is Function
let x be object ; :: thesis: ( x in dom f implies f . x is Function )
assume x in dom f ; :: thesis: f . x is Function
then x in the carrier of S ;
then S1[x,f . x] by A7;
hence f . x is Function ; :: thesis: verum
end;
then reconsider f = f as ManySortedFunction of the carrier of S by FUNCOP_1:def 6;
now :: thesis: for i being object st i in the carrier of S holds
f . i is Function of (A . i),( the Sorts of MSA . i)
let i be object ; :: thesis: ( i in the carrier of S implies f . i is Function of (A . i),( the Sorts of MSA . i) )
assume i in the carrier of S ; :: thesis: f . i is Function of (A . i),( the Sorts of MSA . i)
then S1[i,f . i] by A7;
hence f . i is Function of (A . i),( the Sorts of MSA . i) ; :: thesis: verum
end;
then reconsider f = f as ManySortedFunction of A, the Sorts of MSA by PBOOLE:def 15;
consider IT being ManySortedFunction of (FreeEnv MSA),MSA such that
A8: IT is_homomorphism FreeEnv MSA,MSA and
A9: IT || A = f by MSAFREE:def 5;
take IT ; :: thesis: ( IT is_homomorphism FreeEnv MSA,MSA & ( for s being SortSymbol of S
for x, y being set st y in FreeSort ( the Sorts of MSA,s) & y = root-tree [x,s] & x in the Sorts of MSA . s holds
(IT . s) . y = x ) )

thus IT is_homomorphism FreeEnv MSA,MSA by A8; :: thesis: for s being SortSymbol of S
for x, y being set st y in FreeSort ( the Sorts of MSA,s) & y = root-tree [x,s] & x in the Sorts of MSA . s holds
(IT . s) . y = x

let s be SortSymbol of S; :: thesis: for x, y being set st y in FreeSort ( the Sorts of MSA,s) & y = root-tree [x,s] & x in the Sorts of MSA . s holds
(IT . s) . y = x

let x, y be set ; :: thesis: ( y in FreeSort ( the Sorts of MSA,s) & y = root-tree [x,s] & x in the Sorts of MSA . s implies (IT . s) . y = x )
A10: ex t being SortSymbol of S ex g being Function of (A . t),( the Sorts of MSA . t) st
( g = f . s & t = s & ( for x, y being set st y in A . t & y = root-tree [x,t] & x in the Sorts of MSA . t holds
g . y = x ) ) by A7;
assume that
y in FreeSort ( the Sorts of MSA,s) and
A11: ( y = root-tree [x,s] & x in the Sorts of MSA . s ) ; :: thesis: (IT . s) . y = x
y in FreeGen (s, the Sorts of MSA) by ;
then A12: y in A . s by MSAFREE:def 16;
hence (IT . s) . y = ((IT . s) | (A . s)) . y by FUNCT_1:49
.= (f . s) . y by
.= x by ;
:: thesis: verum