let S be non empty non void ManySortedSign ; for A being non-empty MSAlgebra over S
for F being ManySortedFunction of A,(Trivial_Algebra S) holds F is_epimorphism A, Trivial_Algebra S
let A be non-empty MSAlgebra over S; for F being ManySortedFunction of A,(Trivial_Algebra S) holds F is_epimorphism A, Trivial_Algebra S
let F be ManySortedFunction of A,(Trivial_Algebra S); F is_epimorphism A, Trivial_Algebra S
set I = the carrier of S;
consider XX being ManySortedSet of the carrier of S such that
A1:
{XX} = the carrier of S --> {0}
by Th5;
thus
F is_homomorphism A, Trivial_Algebra S
MSUALG_3:def 8 F 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 (F . (the_result_sort_of o)) . ((Den (o,A)) . b1) = (Den (o,(Trivial_Algebra S))) . (F # b1) )
assume
Args (
o,
A)
<> {}
;
for b1 being Element of Args (o,A) holds (F . (the_result_sort_of o)) . ((Den (o,A)) . b1) = (Den (o,(Trivial_Algebra S))) . (F # b1)
let x be
Element of
Args (
o,
A);
(F . (the_result_sort_of o)) . ((Den (o,A)) . x) = (Den (o,(Trivial_Algebra S))) . (F # x)
thus (F . (the_result_sort_of o)) . ((Den (o,A)) . x) =
0
by Th24
.=
(Den (o,(Trivial_Algebra S))) . (F # x)
by Th24
;
verum
end;
the Sorts of (Trivial_Algebra S) = {XX}
by A1, MSAFREE2:def 12;
hence
F is "onto"
by Th9; verum