let S be non empty non void ManySortedSign ; 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 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 over S; for B being strict non-empty MSAlgebra over 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 over 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 G be 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 H be 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 f be ManySortedFunction of U0,B; ( 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
; f is_epimorphism U0,B
reconsider I = the Sorts of (Image f) as V2() 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 V2() 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; verum