let S be non empty non void ManySortedSign ; :: thesis: for U0 being non-empty MSAlgebra of S
for B being strict non-empty MSAlgebra of S
for G being GeneratorSet of U0
for H being V2() 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 of S; :: thesis: for B being strict non-empty MSAlgebra of S
for G being GeneratorSet of U0
for H being V2() 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 of S; :: thesis: for G being GeneratorSet of U0
for H being V2() 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 V2() 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 V2() 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 V2() MSSubset of B by MSUALG_2:def 10;
the Sorts of (Image f) is ManySortedSubset of the Sorts of (Image f)

proof

thus the Sorts of (Image f) c= the Sorts of (Image f) ; :: according to PBOOLE:def 23 :: thesis: verum

end;

then reconsider I1 = the Sorts of (Image f) as V2() MSSubset of (Image f) ;
A3: I is GeneratorSet of Image f by MSAFREE2:9;
GenMSAlg I = GenMSAlg I1 by EXTENS_1:22;
then A4: GenMSAlg I = Image f by A3, MSAFREE:3;
H is ManySortedSubset of the Sorts of (Image f)

proof

f .:.: G c= f .:.: the Sorts of U0 by EXTENS_1:6;
then H c= f .:.: the Sorts of U0 by A1, PBOOLE:15;
hence H c= the Sorts of (Image f) by A2, MSUALG_3:def 14; :: according to PBOOLE:def 23 :: thesis: verum

end;

then GenMSAlg H is MSSubAlgebra of GenMSAlg I by EXTENS_1:21;
then B is MSSubAlgebra of Image f by A4, MSAFREE:3;
then Image f = B by MSUALG_2:8;
hence f is_epimorphism U0,B by A2, MSUALG_3:19; :: thesis: verum