let S be non empty non void ManySortedSign ; :: thesis: for U1 being non-empty MSAlgebra of S
for U2 being strict non-empty MSAlgebra of S
for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds
( F is_epimorphism U1,U2 iff Image F = U2 )
let U1 be non-empty MSAlgebra of S; :: thesis: for U2 being strict non-empty MSAlgebra of S
for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds
( F is_epimorphism U1,U2 iff Image F = U2 )
let U2 be strict non-empty MSAlgebra of S; :: thesis: for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds
( F is_epimorphism U1,U2 iff Image F = U2 )
let F be ManySortedFunction of U1,U2; :: thesis: ( F is_homomorphism U1,U2 implies ( F is_epimorphism U1,U2 iff Image F = U2 ) )
set FF = F .:.: the Sorts of U1;
assume A1: F is_homomorphism U1,U2 ; :: thesis: ( F is_epimorphism U1,U2 iff Image F = U2 )
thus ( F is_epimorphism U1,U2 implies Image F = U2 ) :: thesis: ( Image F = U2 implies F is_epimorphism U1,U2 )

proof

assume F is_epimorphism U1,U2 ; :: thesis: Image F = U2
then A2: F is "onto" by Def10;

now

let i be set ; :: thesis: ( i in the carrier of S implies (F .:.: the Sorts of U1) . i = the Sorts of U2 . i )
assume A3: i in the carrier of S ; :: thesis: (F .:.: the Sorts of U1) . i = the Sorts of U2 . i
then reconsider f = F . i as Function of ( the Sorts of U1 . i),( the Sorts of U2 . i) by PBOOLE:def 15;
A4: rng f = the Sorts of U2 . i by A2, A3, Def3;
reconsider f = f as Function ;
( (F .:.: the Sorts of U1) . i = f .: ( the Sorts of U1 . i) & dom f = the Sorts of U1 . i ) by A3, FUNCT_2:def 1, PBOOLE:def 20;
hence (F .:.: the Sorts of U1) . i = the Sorts of U2 . i by A4, RELAT_1:113; :: thesis: verum

end;

then A5: F .:.: the Sorts of U1 = the Sorts of U2 by PBOOLE:3;
U2 is strict MSSubAlgebra of U2 by MSUALG_2:5;
hence Image F = U2 by A1, A5, Def14; :: thesis: verum

end;

assume Image F = U2 ; :: thesis: F is_epimorphism U1,U2
then A6: F .:.: the Sorts of U1 = the Sorts of U2 by A1, Def14;
for i being set st i in the carrier of S holds
rng (F . i) = the Sorts of U2 . i

proof

let i be set ; :: thesis: ( i in the carrier of S implies rng (F . i) = the Sorts of U2 . i )
assume i in the carrier of S ; :: thesis: rng (F . i) = the Sorts of U2 . i
then reconsider i = i as Element of S ;
reconsider f = F . i as Function of ( the Sorts of U1 . i),( the Sorts of U2 . i) ;
( f .: ( the Sorts of U1 . i) = the Sorts of U2 . i & dom f = the Sorts of U1 . i ) by A6, FUNCT_2:def 1, PBOOLE:def 20;
hence rng (F . i) = the Sorts of U2 . i by RELAT_1:113; :: thesis: verum

end;

then F is "onto" by Def3;
hence F is_epimorphism U1,U2 by A1, Def10; :: thesis: verum