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

proof

let i be object ; :: thesis: ( i in the carrier of S implies ex j being object st S₁[i,j] )
assume i in the carrier of S ; :: thesis: ex j being object st S₁[i,j]
then reconsider s = i as SortSymbol of S ;
defpred S₂[ 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 & S₂[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 & S₂[e,u] ) )
assume e in A . s ; :: thesis: ex u being object st
( u in the Sorts of MSA . s & S₂[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 & S₂[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
S₂[e,j . e] ) ) from FUNCT_1:sch 6(A2);
reconsider f = j as Function of (A . s),( the Sorts of MSA . s) by A4, 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
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 A6, TREES_4:4;
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
S₁[i,f . i] from PBOOLE:sch 3(A1);

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 S₁[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 S₁[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 A11, MSAFREE:def 15;
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 A9, MSAFREE:def 1
.= x by A11, A12, A10 ;
:: thesis: verum