let S be non empty non void ManySortedSign ; :: thesis: for U0 being non-empty MSAlgebra over S
for B being strict non-empty MSAlgebra over S
for G being GeneratorSet of U0
for H being non-empty GeneratorSet of B
for f being ManySortedFunction of U0,B st H c= f .:.: G & f is_homomorphism U0,B holds
f is_epimorphism U0,B
let U0 be non-empty MSAlgebra over S; :: thesis: for B being strict non-empty MSAlgebra over S
for G being GeneratorSet of U0
for H being non-empty GeneratorSet of B
for f being ManySortedFunction of U0,B st H c= f .:.: G & f is_homomorphism U0,B holds
f is_epimorphism U0,B
let B be strict non-empty MSAlgebra over S; :: thesis: for G being GeneratorSet of U0
for H being non-empty GeneratorSet of B
for f being ManySortedFunction of U0,B st H c= f .:.: G & f is_homomorphism U0,B holds
f is_epimorphism U0,B
let G be GeneratorSet of U0; :: thesis: for H being non-empty GeneratorSet of B
for f being ManySortedFunction of U0,B st H c= f .:.: G & f is_homomorphism U0,B holds
f is_epimorphism U0,B
let H be non-empty GeneratorSet of B; :: thesis: for f being ManySortedFunction of U0,B st H c= f .:.: G & f is_homomorphism U0,B holds
f is_epimorphism U0,B
let f be ManySortedFunction of U0,B; :: thesis: ( H c= f .:.: G & f is_homomorphism U0,B implies f is_epimorphism U0,B )
assume that
A1: H c= f .:.: G and
A2: f is_homomorphism U0,B ; :: thesis: f is_epimorphism U0,B
reconsider I = the Sorts of (Image f) as non-empty MSSubset of B by MSUALG_2:def 9;
f .:.: G c= f .:.: the Sorts of U0 by EXTENS_1:2;
then H c= f .:.: the Sorts of U0 by A1, PBOOLE:13;
then H c= the Sorts of (Image f) by A2, MSUALG_3:def 12;
then H is ManySortedSubset of the Sorts of (Image f) by PBOOLE:def 18;
then A3: GenMSAlg H is MSSubAlgebra of GenMSAlg I by EXTENS_1:17;
reconsider I1 = the Sorts of (Image f) as non-empty MSSubset of (Image f) by PBOOLE:def 18;
( I is GeneratorSet of Image f & GenMSAlg I = GenMSAlg I1 ) by EXTENS_1:18, MSAFREE2:6;
then GenMSAlg I = Image f by MSAFREE:3;
then B is MSSubAlgebra of Image f by A3, MSAFREE:3;
then Image f = B by MSUALG_2:7;
hence f is_epimorphism U0,B by A2, MSUALG_3:19; :: thesis: verum