let S be non empty non void ManySortedSign ; :: thesis: for X being non-empty ManySortedSet of the carrier of S holds hom ((id the carrier of S),(id the carrier' of S),X,S,S) = id the Sorts of (FreeMSA X)
let X be non-empty ManySortedSet of the carrier of S; :: thesis: hom ((id the carrier of S),(id the carrier' of S),X,S,S) = id the Sorts of (FreeMSA X)
set f = id the carrier of S;
set h = hom ((id the carrier of S),(id the carrier' of S),X,S,S);
set I = id the Sorts of (FreeMSA X);
set g = id the carrier' of S;
A1: id the carrier of S, id the carrier' of S form_morphism_between S,S by PUA2MSS1:28;
dom X = the carrier of S by PARTFUN1:def 2;
then A2: X * (id the carrier of S) = X by RELAT_1:52;
A3: (FreeMSA X) | (S,(id the carrier of S),(id the carrier' of S)) = FreeMSA X by Th25;

A4: now :: thesis: for i being object st i in the carrier of S holds
((id the Sorts of (FreeMSA X)) || (FreeGen X)) . i = ((hom ((id the carrier of S),(id the carrier' of S),X,S,S)) || (FreeGen (X * (id the carrier of S)))) . i

let i be object ; :: thesis: ( i in the carrier of S implies ((id the Sorts of (FreeMSA X)) || (FreeGen X)) . i = ((hom ((id the carrier of S),(id the carrier' of S),X,S,S)) || (FreeGen (X * (id the carrier of S)))) . i )
assume i in the carrier of S ; :: thesis: ((id the Sorts of (FreeMSA X)) || (FreeGen X)) . i = ((hom ((id the carrier of S),(id the carrier' of S),X,S,S)) || (FreeGen (X * (id the carrier of S)))) . i
then reconsider s = i as SortSymbol of S ;
FreeGen X c= the Sorts of (FreeMSA X) by PBOOLE:def 18;
then A5: (FreeGen X) . s c= the Sorts of (FreeMSA X) . s ;
then ((id the Sorts of (FreeMSA X)) . s) | ((FreeGen X) . s) is Function of ((FreeGen X) . s),( the Sorts of (FreeMSA X) . s) by FUNCT_2:32;
then A6: dom (((id the Sorts of (FreeMSA X)) . s) | ((FreeGen X) . s)) = (FreeGen X) . s by FUNCT_2:def 1;

A7: now :: thesis: for a being object st a in (FreeGen X) . s holds
(((id the Sorts of (FreeMSA X)) . s) | ((FreeGen X) . s)) . a = (((hom ((id the carrier of S),(id the carrier' of S),X,S,S)) . s) | ((FreeGen X) . s)) . a

let a be object ; :: thesis: ( a in (FreeGen X) . s implies (((id the Sorts of (FreeMSA X)) . s) | ((FreeGen X) . s)) . a = (((hom ((id the carrier of S),(id the carrier' of S),X,S,S)) . s) | ((FreeGen X) . s)) . a )
assume A8: a in (FreeGen X) . s ; :: thesis: (((id the Sorts of (FreeMSA X)) . s) | ((FreeGen X) . s)) . a = (((hom ((id the carrier of S),(id the carrier' of S),X,S,S)) . s) | ((FreeGen X) . s)) . a
then reconsider b = a as Element of (FreeMSA X),s by A5;
b in FreeGen (s,X) by A8, MSAFREE:def 16;
then consider x being set such that
A9: x in X . s and
A10: b = root-tree [x,s] by MSAFREE:def 15;
thus (((id the Sorts of (FreeMSA X)) . s) | ((FreeGen X) . s)) . a = ((id the Sorts of (FreeMSA X)) . s) . b by A8, FUNCT_1:49
.= (id ( the Sorts of (FreeMSA X) . s)) . b by MSUALG_3:def 1
.= b
.= root-tree [x,((id the carrier of S) . s)] by A10
.= ((hom ((id the carrier of S),(id the carrier' of S),X,S,S)) . s) . b by A1, A2, A9, A10, Def5
.= (((hom ((id the carrier of S),(id the carrier' of S),X,S,S)) . s) | ((FreeGen X) . s)) . a by A8, FUNCT_1:49 ; :: thesis: verum

end;

((hom ((id the carrier of S),(id the carrier' of S),X,S,S)) . s) | ((FreeGen X) . s) is Function of ((FreeGen X) . s),( the Sorts of (FreeMSA X) . s) by A2, A3, A5, FUNCT_2:32;
then A11: dom (((hom ((id the carrier of S),(id the carrier' of S),X,S,S)) . s) | ((FreeGen X) . s)) = (FreeGen X) . s by FUNCT_2:def 1;
( ((id the Sorts of (FreeMSA X)) || (FreeGen X)) . s = ((id the Sorts of (FreeMSA X)) . s) | ((FreeGen X) . s) & ((hom ((id the carrier of S),(id the carrier' of S),X,S,S)) || (FreeGen (X * (id the carrier of S)))) . s = ((hom ((id the carrier of S),(id the carrier' of S),X,S,S)) . s) | ((FreeGen (X * (id the carrier of S))) . s) ) by MSAFREE:def 1;
hence ((id the Sorts of (FreeMSA X)) || (FreeGen X)) . i = ((hom ((id the carrier of S),(id the carrier' of S),X,S,S)) || (FreeGen (X * (id the carrier of S)))) . i by A2, A6, A11, A7; :: thesis: verum

end;

( id the Sorts of (FreeMSA X) is_homomorphism FreeMSA X, FreeMSA X & hom ((id the carrier of S),(id the carrier' of S),X,S,S) is_homomorphism FreeMSA (X * (id the carrier of S)),(FreeMSA X) | (S,(id the carrier of S),(id the carrier' of S)) ) by A1, Def5, MSUALG_3:9;
hence hom ((id the carrier of S),(id the carrier' of S),X,S,S) = id the Sorts of (FreeMSA X) by A2, A3, A4, EXTENS_1:19, PBOOLE:3; :: thesis: verum