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 ** (MSNat_Hom A,C1) = MSNat_Hom 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 ** (MSNat_Hom A,C1) = MSNat_Hom 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 ** (MSNat_Hom A,C1) = MSNat_Hom A,C2
set sL = the Sorts of (QuotMSAlg A,C1);
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 ** (MSNat_Hom A,C1) = MSNat_Hom 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 ** (MSNat_Hom A,C1) = MSNat_Hom A,C2

now

let i be set ; :: thesis: ( i in the carrier of S implies (G ** (MSNat_Hom A,C1)) . i = (MSNat_Hom A,C2) . i )
assume i in the carrier of S ; :: thesis: (G ** (MSNat_Hom A,C1)) . i = (MSNat_Hom A,C2) . i
then reconsider s = i as SortSymbol of S ;
A2: for c being Element of the Sorts of A . s holds ((G . s) * ((MSNat_Hom A,C1) . s)) . c = ((MSNat_Hom A,C2) . s) . c

proof

let c be Element of the Sorts of A . s; :: thesis: ((G . s) * ((MSNat_Hom A,C1) . s)) . c = ((MSNat_Hom A,C2) . s) . c
Class (C1 . s),c in Class (C1 . s) by EQREL_1:def 5;
then A3: Class C1,c is Element of the Sorts of (QuotMSAlg A,C1) . s by MSUALG_4:def 8;
thus ((G . s) * ((MSNat_Hom A,C1) . s)) . c = (G . s) . (((MSNat_Hom A,C1) . s) . c) by FUNCT_2:21
.= (G . s) . ((MSNat_Hom A,C1,s) . c) by MSUALG_4:def 18
.= (G . s) . (Class C1,c) by MSUALG_4:def 17
.= Class C2,c by A1, A3
.= (MSNat_Hom A,C2,s) . c by MSUALG_4:def 17
.= ((MSNat_Hom A,C2) . s) . c by MSUALG_4:def 18 ; :: thesis: verum

end;

thus (G ** (MSNat_Hom A,C1)) . i = (G . s) * ((MSNat_Hom A,C1) . s) by MSUALG_3:2
.= (MSNat_Hom A,C2) . i by A2, FUNCT_2:113 ; :: thesis: verum

end;

hence G ** (MSNat_Hom A,C1) = MSNat_Hom A,C2 by PBOOLE:3; :: thesis: verum