for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra over S
for U2 being non-empty MSSubAlgebra of U1
for G being ManySortedFunction of U2,U1 st G = id the Sorts of U2 holds
G is_monomorphism U2,U1