let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra over 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 over 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)
MSNat_Hom (A,C2) is_epimorphism A, QuotMSAlg (A,C2) by MSUALG_4:3;
then A1: MSNat_Hom (A,C2) is_homomorphism A, 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 A2: 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)
G ** (MSNat_Hom (A,C1)) = MSNat_Hom (A,C2) by A2, Th34;
hence G is_homomorphism QuotMSAlg (A,C1), QuotMSAlg (A,C2) by A1, Th19, MSUALG_4:3; :: according to MSUALG_3:def 8 :: thesis: G is "onto"
thus G is "onto" by A2, Lm1; :: thesis: verum