let S be non empty non void ManySortedSign ; for U1, U2 being non-empty MSAlgebra over S
for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds
( F is_epimorphism U1,U2 iff Image F = MSAlgebra(# the Sorts of U2, the Charact of U2 #) )
let U1, U2 be non-empty MSAlgebra over S; for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds
( F is_epimorphism U1,U2 iff Image F = MSAlgebra(# the Sorts of U2, the Charact of U2 #) )
let F be ManySortedFunction of U1,U2; ( F is_homomorphism U1,U2 implies ( F is_epimorphism U1,U2 iff Image F = MSAlgebra(# the Sorts of U2, the Charact of U2 #) ) )
set FF = F .:.: the Sorts of U1;
assume A1:
F is_homomorphism U1,U2
; ( F is_epimorphism U1,U2 iff Image F = MSAlgebra(# the Sorts of U2, the Charact of U2 #) )
thus
( F is_epimorphism U1,U2 implies Image F = MSAlgebra(# the Sorts of U2, the Charact of U2 #) )
( Image F = MSAlgebra(# the Sorts of U2, the Charact of U2 #) implies F is_epimorphism U1,U2 )
assume
Image F = MSAlgebra(# the Sorts of U2, the Charact of U2 #)
; F is_epimorphism U1,U2
then A6:
F .:.: the Sorts of U1 = the Sorts of U2
by A1, Def12;
for i being set st i in the carrier of S holds
rng (F . i) = the Sorts of U2 . i
then
F is "onto"
;
hence
F is_epimorphism U1,U2
by A1; verum