theorem
for
S1,
S2 being non
empty non
void ManySortedSign for
X being
V2()
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)