theorem Th15: :: OSALG_3:15

for S1 being OrderSortedSign
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 )