let S be non empty non void ManySortedSign ; :: thesis: for X being V16() 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 V16() 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:29;
dom X = the carrier of S by PARTFUN1:def 4;
then A2: X * (id the carrier of S) = X by RELAT_1:78;
A3: (FreeMSA X) | S,(id the carrier of S),(id the carrier' of S) = FreeMSA X by Th26;

A4: now

let i be set ; :: 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 23;
then A5: (FreeGen X) . s c= the Sorts of (FreeMSA X) . s by PBOOLE:def 5;
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:38;
then A6: dom (((id the Sorts of (FreeMSA X)) . s) | ((FreeGen X) . s)) = (FreeGen X) . s by FUNCT_2:def 1;

A7: now

let a be set ; :: 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 18;
then consider x being set such that
A9: x in X . s and
A10: b = root-tree [x,s] by MSAFREE:def 17;
thus (((id the Sorts of (FreeMSA X)) . s) | ((FreeGen X) . s)) . a = ((id the Sorts of (FreeMSA X)) . s) . b by A8, FUNCT_1:72
.= (id (the Sorts of (FreeMSA X) . s)) . b by MSUALG_3:def 1
.= b by FUNCT_1:35
.= root-tree [x,((id the carrier of S) . s)] by A10, FUNCT_1:35
.= ((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:72 ; :: 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:38;
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, FUNCT_1:9; :: 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:23, PBOOLE:3; :: thesis: verum