theorem :: INSTALG1:42

for S1, S2 being non empty non void ManySortedSign
for X being non-empty ManySortedSet of the carrier of S2
for f being Function of the carrier of S1, the carrier of S2
for g being one-to-one Function st f,g form_morphism_between S1,S2 holds
hom (f,g,X,S1,S2) is_monomorphism FreeMSA (X * f),(FreeMSA X) | (S1,f,g)