let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra of S
for C1, C2 being MSCongruence of A
for G being ManySortedFunction of (QuotMSAlg A,C1),(QuotMSAlg A,C2) st ( for i being Element of S
for x being Element of the Sorts of (QuotMSAlg A,C1) . i
for xx being Element of the Sorts of A . i st x = Class C1,xx holds
(G . i) . x = Class C2,xx ) holds
G is_epimorphism QuotMSAlg A,C1, QuotMSAlg A,C2
let A be non-empty MSAlgebra of S; :: thesis: for C1, C2 being MSCongruence of A
for G being ManySortedFunction of (QuotMSAlg A,C1),(QuotMSAlg A,C2) st ( for i being Element of S
for x being Element of the Sorts of (QuotMSAlg A,C1) . i
for xx being Element of the Sorts of A . i st x = Class C1,xx holds
(G . i) . x = Class C2,xx ) holds
G is_epimorphism QuotMSAlg A,C1, QuotMSAlg A,C2
let C1, C2 be MSCongruence of A; :: thesis: for G being ManySortedFunction of (QuotMSAlg A,C1),(QuotMSAlg A,C2) st ( for i being Element of S
for x being Element of the Sorts of (QuotMSAlg A,C1) . i
for xx being Element of the Sorts of A . i st x = Class C1,xx holds
(G . i) . x = Class C2,xx ) holds
G is_epimorphism QuotMSAlg A,C1, QuotMSAlg A,C2
let G be ManySortedFunction of (QuotMSAlg A,C1),(QuotMSAlg A,C2); :: thesis: ( ( for i being Element of S
for x being Element of the Sorts of (QuotMSAlg A,C1) . i
for xx being Element of the Sorts of A . i st x = Class C1,xx holds
(G . i) . x = Class C2,xx ) implies G is_epimorphism QuotMSAlg A,C1, QuotMSAlg A,C2 )
assume A1: for i being Element of S
for x being Element of the Sorts of (QuotMSAlg A,C1) . i
for xx being Element of the Sorts of A . i st x = Class C1,xx holds
(G . i) . x = Class C2,xx ; :: thesis: G is_epimorphism QuotMSAlg A,C1, QuotMSAlg A,C2
MSNat_Hom A,C2 is_epimorphism A, QuotMSAlg A,C2 by MSUALG_4:3;
then A2: MSNat_Hom A,C2 is_homomorphism A, QuotMSAlg A,C2 by MSUALG_3:def 10;
G ** (MSNat_Hom A,C1) = MSNat_Hom A,C2 by A1, Th35;
hence G is_homomorphism QuotMSAlg A,C1, QuotMSAlg A,C2 by A2, Th20, MSUALG_4:3; :: according to MSUALG_3:def 10 :: thesis: G is "onto"
thus G is "onto" by A1, Lm1; :: thesis: verum