theorem :: INSTALG1:43

for S being non empty non void ManySortedSign
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)