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 )

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

hence F is_epimorphism U1,U2 by A1; :: thesis: verum

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
Image F = MSAlgebra(# the Sorts of U2, the Charact of U2 #)
; :: thesis: F is_epimorphism U1,U2
assume
F is_epimorphism U1,U2
; :: thesis: Image F = MSAlgebra(# the Sorts of U2, the Charact of U2 #)

then A2: F is "onto" ;

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;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

then A5:
F .:.: the Sorts of U1 = the Sorts of U2
by PBOOLE:3;(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;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

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

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

then
F is "onto"
;
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;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

hence F is_epimorphism U1,U2 by A1; :: thesis: verum