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 ) )
assume A1: F is_homomorphism U1,U2 ; :: thesis: ( F is_epimorphism U1,U2 iff Image F = U2 )
set FF = F .:.: the Sorts of U1;
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 18;
A4: rng f = the Sorts of U2 . i by A2, A3, Def3;
reconsider f = f as Function ;
A5: (F .:.: the Sorts of U1) . i = f .: (the Sorts of U1 . i) by A3, PBOOLE:def 25;
( the Sorts of U2 . i = {} implies the Sorts of U1 . i = {} ) by A3;
then dom f = the Sorts of U1 . i by FUNCT_2:def 1;
hence (F .:.: the Sorts of U1) . i = the Sorts of U2 . i by A4, A5, RELAT_1:146; :: thesis: verum

end;

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

end;

assume Image F = U2 ; :: thesis: F is_epimorphism U1,U2
then A7: 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) ;
A8: f .: (the Sorts of U1 . i) = the Sorts of U2 . i by A7, PBOOLE:def 25;
dom f = the Sorts of U1 . i by FUNCT_2:def 1;
hence rng (F . i) = the Sorts of U2 . i by A8, RELAT_1:146; :: thesis: verum

end;

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