let S be non empty non void ManySortedSign ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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 #) ) :: thesis: ( Image F = MSAlgebra(# the Sorts of U2, the Charact of U2 #) implies F is_epimorphism U1,U2 )
proof
assume F is_epimorphism U1,U2 ; :: thesis: Image F = MSAlgebra(# the Sorts of U2, the Charact of U2 #)
then A2: F is "onto" ;
now :: thesis: for i being object st i in the carrier of S holds
(F .:.: the Sorts of U1) . i = the Sorts of U2 . i
let i be object ; :: 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;
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;
MSAlgebra(# the Sorts of U2, the Charact of U2 #) is strict MSSubAlgebra of U2 by MSUALG_2:5;
hence Image F = MSAlgebra(# the Sorts of U2, the Charact of U2 #) by A1, A5, Def12; :: thesis: verum
end;
assume Image F = MSAlgebra(# the Sorts of U2, the Charact of U2 #) ; :: thesis: 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
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" ;
hence F is_epimorphism U1,U2 by A1; :: thesis: verum