reconsider A = FreeGen the Sorts of MSA as free GeneratorSet of FreeEnv MSA by MSAFREE:16;
defpred S₁[ set , set ] 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 set st i in the carrier of S holds
ex j being set st S₁[i,j]

proof

let i be set ; :: thesis: ( i in the carrier of S implies ex j being set st S₁[i,j] )
assume i in the carrier of S ; :: thesis: ex j being set st S₁[i,j]
then reconsider s = i as SortSymbol of S ;
defpred S₂[ set , set ] means $1 = root-tree [$2,s];
A2: for e being set st e in A . s holds
ex u being set st
( u in the Sorts of MSA . s & S₂[e,u] )

proof

let e be set ; :: thesis: ( e in A . s implies ex u being set st
( u in the Sorts of MSA . s & S₂[e,u] ) )
assume e in A . s ; :: thesis: ex u being set st
( u in the Sorts of MSA . s & S₂[e,u] )
then e in FreeGen (s, the Sorts of MSA) by MSAFREE:def 16;
hence ex u being set st
( u in the Sorts of MSA . s & S₂[e,u] ) by MSAFREE:def 15; :: thesis: verum

end;

consider j being Function such that
A3: ( dom j = A . s & rng j c= the Sorts of MSA . s & ( for e being set st e in A . s holds
S₂[e,j . e] ) ) from FUNCT_1:sch 5(A2);
reconsider f = j as Function of (A . s),( the Sorts of MSA . s) by A3, FUNCT_2:def 1, RELSET_1:4;
take j ; :: thesis: S₁[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
A4: y in A . s and
A5: y = root-tree [x,s] and
x in the Sorts of MSA . s ; :: thesis: f . y = x
y = root-tree [(j . y),s] by A3, A4;
then [x,s] = [(j . y),s] by A5, TREES_4:4;
hence f . y = x by ZFMISC_1:27; :: thesis: verum

end;

consider f being ManySortedSet of the carrier of S such that
A6: for i being set st i in the carrier of S holds
S₁[i,f . i] from PBOOLE:sch 3(A1);

now

let x be set ; :: 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 by PARTFUN1:def 2;
then S₁[x,f . x] by A6;
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

let i be set ; :: 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 S₁[i,f . i] by A6;
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
A7: IT is_homomorphism FreeEnv MSA,MSA and
A8: 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 A7; :: 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 )
A9: 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 A6;
assume that
y in FreeSort ( the Sorts of MSA,s) and
A10: ( 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 A10, MSAFREE:def 15;
then A11: 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 A8, MSAFREE:def 1
.= x by A10, A11, A9 ;
:: thesis: verum