for R being Relation
for X, Y being set st X c= Y holds
(R | Y) .: X = R .: X

for I being set
for A being ManySortedSet of I
for B being V3 ManySortedSet of I
for F being ManySortedFunction of A,B
for X being ManySortedSubset of A st A c= X holds
F || X = F

for I being set
for A, B being ManySortedSet of I
for M being ManySortedSubset of A
for F being ManySortedFunction of A,B holds F .:.: M c= F .:.: A

for I being set
for A being ManySortedSet of I
for B being V3 ManySortedSet of I
for F being ManySortedFunction of A,B
for M1, M2 being ManySortedSubset of A st M1 c= M2 holds
(F || M2) .:.: M1 = F .:.: M1

for I being set
for A being ManySortedSet of I
for B, C being V3 ManySortedSet of I
for F being ManySortedFunction of A,B
for G being ManySortedFunction of B,C
for X being ManySortedSubset of A holds (G ** F) || X = G ** (F || X)

for I being set
for A, B being ManySortedSet of I st A is_transformable_to B holds
for F being ManySortedFunction of A,B
for C being ManySortedSet of I st B is ManySortedSubset of C holds
F is ManySortedFunction of A,C

for I being set
for A being ManySortedSet of I
for B being V3 ManySortedSet of I
for F being ManySortedFunction of A,B
for X being ManySortedSubset of A st F is "1-1" holds
F || X is "1-1"

for I being set
for A being ManySortedSet of I
for B being V3 ManySortedSet of I
for F being ManySortedFunction of A,B
for X being ManySortedSubset of A holds doms (F || X) c= doms F

for I being set
for A being ManySortedSet of I
for B being V3 ManySortedSet of I
for F being ManySortedFunction of A,B
for X being ManySortedSubset of A holds rngs (F || X) c= rngs F

for I being set
for A, B being ManySortedSet of I
for F being ManySortedFunction of A,B holds
( F is "onto" iff rngs F = B )

for S being non empty non void ManySortedSign
for X being V3 ManySortedSet of the carrier of S holds rngs (Reverse X) = X

for I being set
for A being ManySortedSet of I
for B, C being V3 ManySortedSet of I
for F being ManySortedFunction of A,B
for G being ManySortedFunction of B,C
for X being V3 ManySortedSubset of B st rngs F c= X holds
(G || X) ** F = G ** F

for I being set
for A being ManySortedSet of I
for B being V3 ManySortedSet of I
for F being ManySortedFunction of A,B holds
( F is "onto" iff for C being V3 ManySortedSet of I
for G, H being ManySortedFunction of B,C st G ** F = H ** F holds
G = H )

for I being set
for A being ManySortedSet of I
for B being V3 ManySortedSet of I
for F being ManySortedFunction of A,B st A is non-empty & B is non-empty holds
( F is "1-1" iff for C being ManySortedSet of I
for G, H being ManySortedFunction of C,A st F ** G = F ** H holds
G = H )

for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra of S
for X being V3 ManySortedSet of the carrier of S
for h1, h2 being ManySortedFunction of (FreeMSA X),U1 st h1 is_homomorphism FreeMSA X,U1 & h2 is_homomorphism FreeMSA X,U1 & h1 || (FreeGen X) = h2 || (FreeGen X) holds
h1 = h2

for S being non empty non void ManySortedSign
for U1, U2 being non-empty MSAlgebra of S
for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 & F is_epimorphism U1,U2 holds
for U3 being non-empty MSAlgebra of S
for h1, h2 being ManySortedFunction of U2,U3 st h1 is_homomorphism U2,U3 & h2 is_homomorphism U2,U3 & h1 ** F = h2 ** F holds
h1 = h2

for S being non empty non void ManySortedSign
for U2, U3 being non-empty MSAlgebra of S
for F being ManySortedFunction of U2,U3 st F is_homomorphism U2,U3 holds
( F is_monomorphism U2,U3 iff for U1 being non-empty MSAlgebra of S
for h1, h2 being ManySortedFunction of U1,U2 st h1 is_homomorphism U1,U2 & h2 is_homomorphism U1,U2 & F ** h1 = F ** h2 holds
h1 = h2 )

for S being non empty non void ManySortedSign
for U1 being MSAlgebra of S
for A, B being MSSubset of U1 st A is ManySortedSubset of B holds
GenMSAlg A is MSSubAlgebra of GenMSAlg B

for S being non empty non void ManySortedSign
for U1 being MSAlgebra of S
for U2 being MSSubAlgebra of U1
for B1 being MSSubset of U1
for B2 being MSSubset of U2 st B1 = B2 holds
GenMSAlg B1 = GenMSAlg B2

for S being non empty non void ManySortedSign
for U1 being strict non-empty MSAlgebra of S
for U2 being non-empty MSAlgebra of S
for Gen being GeneratorSet of U1
for h1, h2 being ManySortedFunction of U1,U2 st h1 is_homomorphism U1,U2 & h2 is_homomorphism U1,U2 & h1 || Gen = h2 || Gen holds
h1 = h2