let S be non empty non void ManySortedSign ; 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; 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; 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)); ( ( 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)
; 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; MSUALG_3:def 8 G is "onto"
thus
G is "onto"
by A2, Lm1; verum