let S be non empty non void ManySortedSign ; :: thesis: 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; :: thesis: 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); :: thesis: 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 :: according to MSUALG_3:def 8 :: thesis: F 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 (F . (the_result_sort_of o)) . ((Den (o,A)) . b₁) = (Den (o,(Trivial_Algebra S))) . (F # b₁) )
assume Args (o,A) <> {} ; :: thesis: for b₁ being Element of Args (o,A) holds (F . (the_result_sort_of o)) . ((Den (o,A)) . b₁) = (Den (o,(Trivial_Algebra S))) . (F # b₁)
let x be Element of Args (o,A); :: thesis: (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 ; :: thesis: verum

end;

the Sorts of (Trivial_Algebra S) = {XX} by A1, MSAFREE2:def 12;
hence F is "onto" by Th9; :: thesis: verum