let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra of S
for F being ManySortedFunction of A,(Trivial_Algebra S) holds F is_epimorphism A, Trivial_Algebra S
let A be non-empty MSAlgebra of 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 such that
A1: {XX} = the carrier of S --> {0 } by Th6;
A2: the Sorts of (Trivial_Algebra S) = {XX} by A1, MSAFREE2:def 12;
thus F is_homomorphism A, Trivial_Algebra S :: according to MSUALG_3:def 10 :: thesis: F is "onto"

proof

let o be OperSymbol of S; :: according to MSUALG_3:def 9 :: 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 Th25
.= (Den o,(Trivial_Algebra S)) . (F # x) by Th25 ; :: thesis: verum

end;

thus F is "onto" by A2, Th10; :: thesis: verum