let S1 be OrderSortedSign; :: thesis: for U1, U2 being non-empty OSAlgebra of S1

for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 & F is order-sorted holds

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

( F = G & G is order-sorted & G is_epimorphism U1, Image F )

let U1, U2 be non-empty OSAlgebra of S1; :: thesis: for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 & F is order-sorted holds

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

( F = G & G is order-sorted & G is_epimorphism U1, Image F )

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

( F = G & G is order-sorted & G is_epimorphism U1, Image F ) )

assume that

A1: F is_homomorphism U1,U2 and

A2: F is order-sorted ; :: thesis: ex G being ManySortedFunction of U1,(Image F) st

( F = G & G is order-sorted & G is_epimorphism U1, Image F )

consider G being ManySortedFunction of U1,(Image F) such that

A3: ( F = G & G is_epimorphism U1, Image F ) by A1, MSUALG_3:21;

take G ; :: thesis: ( F = G & G is order-sorted & G is_epimorphism U1, Image F )

thus ( F = G & G is order-sorted & G is_epimorphism U1, Image F ) by A2, A3; :: thesis: verum

for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 & F is order-sorted holds

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

( F = G & G is order-sorted & G is_epimorphism U1, Image F )

let U1, U2 be non-empty OSAlgebra of S1; :: thesis: for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 & F is order-sorted holds

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

( F = G & G is order-sorted & G is_epimorphism U1, Image F )

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

( F = G & G is order-sorted & G is_epimorphism U1, Image F ) )

assume that

A1: F is_homomorphism U1,U2 and

A2: F is order-sorted ; :: thesis: ex G being ManySortedFunction of U1,(Image F) st

( F = G & G is order-sorted & G is_epimorphism U1, Image F )

consider G being ManySortedFunction of U1,(Image F) such that

A3: ( F = G & G is_epimorphism U1, Image F ) by A1, MSUALG_3:21;

take G ; :: thesis: ( F = G & G is order-sorted & G is_epimorphism U1, Image F )

thus ( F = G & G is order-sorted & G is_epimorphism U1, Image F ) by A2, A3; :: thesis: verum