let S be non empty non void ManySortedSign ; :: thesis: for X being V5 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 V5 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;
then A2: ( 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 Def5, MSUALG_3:9;
dom X = the carrier of S by PBOOLE:def 3;
then A3: ( X * (id the carrier of S) = X & (FreeMSA X) | S,(id the carrier of S),(id the carrier' of S) = FreeMSA X ) by Th26, RELAT_1:78;

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 ;
A4: ( ((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;
( FreeMSA X = MSAlgebra(# (FreeSort X),(FreeOper X) #) & FreeGen X c= the Sorts of (FreeMSA X) ) by MSAFREE:def 16, 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 & ((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 A3, FUNCT_2:38;
then A6: ( dom (((id the Sorts of (FreeMSA X)) . s) | ((FreeGen X) . s)) = (FreeGen X) . s & 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;

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 A7: 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 A7, MSAFREE:def 18;
then consider x being set such that
A8: ( x in X . s & 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 A7, 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 A8, FUNCT_1:35
.= ((hom (id the carrier of S),(id the carrier' of S),X,S,S) . s) . b by A1, A3, A8, Def5
.= (((hom (id the carrier of S),(id the carrier' of S),X,S,S) . s) | ((FreeGen X) . s)) . a by A7, FUNCT_1:72 ; :: thesis: verum

end;

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 A3, A4, A6, FUNCT_1:9; :: thesis: verum

end;

then (id the Sorts of (FreeMSA X)) || (FreeGen X) = (hom (id the carrier of S),(id the carrier' of S),X,S,S) || (FreeGen (X * (id the carrier of S))) by PBOOLE:3;
hence hom (id the carrier of S),(id the carrier' of S),X,S,S = id the Sorts of (FreeMSA X) by A2, A3, EXTENS_1:23; :: thesis: verum