let S be non empty non void ManySortedSign ; :: thesis: for U1, U2 being non-empty MSAlgebra of S
for F being ManySortedFunction of U1,U2 st F is_epimorphism U1,U2 holds
for U3 being non-empty MSAlgebra of S
for h1, h2 being ManySortedFunction of U2,U3 st h1 ** F = h2 ** F holds
h1 = h2
let U1, U2 be non-empty MSAlgebra of S; :: thesis: for F being ManySortedFunction of U1,U2 st F is_epimorphism U1,U2 holds
for U3 being non-empty MSAlgebra of S
for h1, h2 being ManySortedFunction of U2,U3 st h1 ** F = h2 ** F holds
h1 = h2
let F be ManySortedFunction of U1,U2; :: thesis: ( F is_epimorphism U1,U2 implies for U3 being non-empty MSAlgebra of S
for h1, h2 being ManySortedFunction of U2,U3 st h1 ** F = h2 ** F holds
h1 = h2 )
assume F is_epimorphism U1,U2 ; :: thesis: for U3 being non-empty MSAlgebra of S
for h1, h2 being ManySortedFunction of U2,U3 st h1 ** F = h2 ** F holds
h1 = h2
then A1: F is "onto" by MSUALG_3:def 8;
let U3 be non-empty MSAlgebra of S; :: thesis: for h1, h2 being ManySortedFunction of U2,U3 st h1 ** F = h2 ** F holds
h1 = h2
let h1, h2 be ManySortedFunction of U2,U3; :: thesis: ( h1 ** F = h2 ** F implies h1 = h2 )
assume h1 ** F = h2 ** F ; :: thesis: h1 = h2
hence h1 = h2 by A1, Th16; :: thesis: verum