thus
( C is A -Image implies ex h being ManySortedFunction of A,C st h is_epimorphism A,C )
( 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 )
;
MSAFREE4:def 4 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
;
g is_epimorphism A,C
thus
g is_homomorphism A,
C
MSUALG_3:def 8 g is "onto" proof
let o be
OperSymbol of
S;
MSUALG_3:def 7 ( Args (o,A) = {} or for b1 being Element of Args (o,A) holds (g . (the_result_sort_of o)) . ((Den (o,A)) . b1) = (Den (o,C)) . (g # b1) )
assume
Args (
o,
A)
<> {}
;
for b1 being Element of Args (o,A) holds (g . (the_result_sort_of o)) . ((Den (o,A)) . b1) = (Den (o,C)) . (g # b1)
let x be
Element of
Args (
o,
A);
(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;
verum
end;
thus
g is
"onto"
by A1, A2;
verum
end;
given h being ManySortedFunction of A,C such that A4:
h is_epimorphism A,C
; C is A -Image
take
C
; MSAFREE4:def 4 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
; ( h is_homomorphism A,C & MSAlgebra(# the Sorts of C, the Charact of C #) = Image h )
thus
h is_homomorphism A,C
by A4; 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; verum