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 ** (MSNat_Hom (A,C1)) = MSNat_Hom (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 ** (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 :: thesis: for i being object st i in the carrier of S holds
(G ** (MSNat_Hom (A,C1))) . i = (MSNat_Hom (A,C2)) . i

let i be object ; :: 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 3;
then A3: Class (C1,c) is Element of the Sorts of (QuotMSAlg (A,C1)) . s by MSUALG_4:def 6;
thus ((G . s) * ((MSNat_Hom (A,C1)) . s)) . c = (G . s) . (((MSNat_Hom (A,C1)) . s) . c) by FUNCT_2:15
.= (G . s) . ((MSNat_Hom (A,C1,s)) . c) by MSUALG_4:def 16
.= (G . s) . (Class (C1,c)) by MSUALG_4:def 15
.= Class (C2,c) by A1, A3
.= (MSNat_Hom (A,C2,s)) . c by MSUALG_4:def 15
.= ((MSNat_Hom (A,C2)) . s) . c by MSUALG_4:def 16 ; :: 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:63 ; :: thesis: verum

end;

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