let S be non empty non void ManySortedSign ; :: thesis: for U1, U2 being non-empty MSAlgebra over S

for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds

ex G being ManySortedFunction of U1,(Image F) st

( F = G & G is_epimorphism U1, Image F )

let U1, U2 be non-empty MSAlgebra over S; :: thesis: for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds

ex G being ManySortedFunction of U1,(Image F) st

( F = G & G is_epimorphism U1, Image F )

let F be ManySortedFunction of U1,U2; :: thesis: ( F is_homomorphism U1,U2 implies ex G being ManySortedFunction of U1,(Image F) st

( F = G & G is_epimorphism U1, Image F ) )

assume A1: F is_homomorphism U1,U2 ; :: thesis: ex G being ManySortedFunction of U1,(Image F) st

( F = G & G is_epimorphism U1, Image F )

then reconsider G = F as ManySortedFunction of U1,(Image F) by Lm3;

take G ; :: thesis: ( F = G & G is_epimorphism U1, Image F )

thus ( F = G & G is_epimorphism U1, Image F ) by A1, Th20; :: thesis: verum

for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds

ex G being ManySortedFunction of U1,(Image F) st

( F = G & G is_epimorphism U1, Image F )

let U1, U2 be non-empty MSAlgebra over S; :: thesis: for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds

ex G being ManySortedFunction of U1,(Image F) st

( F = G & G is_epimorphism U1, Image F )

let F be ManySortedFunction of U1,U2; :: thesis: ( F is_homomorphism U1,U2 implies ex G being ManySortedFunction of U1,(Image F) st

( F = G & G is_epimorphism U1, Image F ) )

assume A1: F is_homomorphism U1,U2 ; :: thesis: ex G being ManySortedFunction of U1,(Image F) st

( F = G & G is_epimorphism U1, Image F )

then reconsider G = F as ManySortedFunction of U1,(Image F) by Lm3;

take G ; :: thesis: ( F = G & G is_epimorphism U1, Image F )

thus ( F = G & G is_epimorphism U1, Image F ) by A1, Th20; :: thesis: verum