thus ( C is A -Image implies ex h being ManySortedFunction of A,C st h is_epimorphism A,C ) :: thesis: ( ex h being ManySortedFunction of A,C st h is_epimorphism A,C implies C is A -Image )

proof

given B being non-empty MSAlgebra over S, h being ManySortedFunction of A,B such that A1: ( h is_homomorphism A,B & MSAlgebra(# the Sorts of C, the Charact of C #) = Image h ) ; :: according to MSAFREE4:def 4 :: thesis: ex h being ManySortedFunction of A,C st h is_epimorphism A,C
consider g0 being ManySortedFunction of A,(Image h) such that
A2: ( h = g0 & g0 is_epimorphism A, Image h ) by A1, MSUALG_3:21;
reconsider g = g0 as ManySortedFunction of A,C by A1;
take g ; :: thesis: g is_epimorphism A,C
thus g is_homomorphism A,C :: according to MSUALG_3:def 8 :: thesis: g is "onto"

proof

let o be OperSymbol of S; :: according to MSUALG_3:def 7 :: thesis: ( Args (o,A) = {} or for b₁ being Element of Args (o,A) holds (g . (the_result_sort_of o)) . ((Den (o,A)) . b₁) = (Den (o,C)) . (g # b₁) )
assume Args (o,A) <> {} ; :: thesis: for b₁ being Element of Args (o,A) holds (g . (the_result_sort_of o)) . ((Den (o,A)) . b₁) = (Den (o,C)) . (g # b₁)
let x be Element of Args (o,A); :: thesis: (g . (the_result_sort_of o)) . ((Den (o,A)) . x) = (Den (o,C)) . (g # x)
A3: ( Args (o,(Image h)) = Args (o,C) & Den (o,(Image h)) = Den (o,C) ) by A1;
g0 # x = (Frege (g0 * (the_arity_of o))) . x by MSUALG_3:def 5
.= g # x by MSUALG_3:def 5 ;
hence (g . (the_result_sort_of o)) . ((Den (o,A)) . x) = (Den (o,C)) . (g # x) by A2, A3, MSUALG_3:def 7; :: thesis: verum

end;

thus g is "onto" by A1, A2; :: thesis: verum

end;

given h being ManySortedFunction of A,C such that A4: h is_epimorphism A,C ; :: thesis: C is A -Image
take C ; :: according to MSAFREE4:def 4 :: thesis: ex h being ManySortedFunction of A,C st
( h is_homomorphism A,C & MSAlgebra(# the Sorts of C, the Charact of C #) = Image h )
take h ; :: thesis: ( h is_homomorphism A,C & MSAlgebra(# the Sorts of C, the Charact of C #) = Image h )
thus h is_homomorphism A,C by A4; :: thesis: MSAlgebra(# the Sorts of C, the Charact of C #) = Image h
thus MSAlgebra(# the Sorts of C, the Charact of C #) = Image h by A4, MSUALG_3:19; :: thesis: verum