theorem :: EXTENS_1:15

for S being non empty non void ManySortedSign
for U1, U2 being non-empty MSAlgebra over S
for F being ManySortedFunction of U1,U2 st F is_epimorphism U1,U2 holds
for U3 being non-empty MSAlgebra over S
for h1, h2 being ManySortedFunction of U2,U3 st h1 ** F = h2 ** F holds
h1 = h2 by Th12;