let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra over S
for C being MSCongruence of A
for s being SortSymbol of S
for x, y being Element of the Sorts of A . s holds
( ((MSNat_Hom (A,C)) . s) . x = ((MSNat_Hom (A,C)) . s) . y iff [x,y] in C . s )
let A be non-empty MSAlgebra over S; :: thesis: for C being MSCongruence of A
for s being SortSymbol of S
for x, y being Element of the Sorts of A . s holds
( ((MSNat_Hom (A,C)) . s) . x = ((MSNat_Hom (A,C)) . s) . y iff [x,y] in C . s )
let C be MSCongruence of A; :: thesis: for s being SortSymbol of S
for x, y being Element of the Sorts of A . s holds
( ((MSNat_Hom (A,C)) . s) . x = ((MSNat_Hom (A,C)) . s) . y iff [x,y] in C . s )
let s be SortSymbol of S; :: thesis: for x, y being Element of the Sorts of A . s holds
( ((MSNat_Hom (A,C)) . s) . x = ((MSNat_Hom (A,C)) . s) . y iff [x,y] in C . s )
let x, y be Element of the Sorts of A . s; :: thesis: ( ((MSNat_Hom (A,C)) . s) . x = ((MSNat_Hom (A,C)) . s) . y iff [x,y] in C . s )
set f = (MSNat_Hom (A,C)) . s;
set g = MSNat_Hom (A,C,s);
A1: (MSNat_Hom (A,C)) . s = MSNat_Hom (A,C,s) by MSUALG_4:def 16;

hereby :: thesis: ( [x,y] in C . s implies ((MSNat_Hom (A,C)) . s) . x = ((MSNat_Hom (A,C)) . s) . y )

assume A2: ((MSNat_Hom (A,C)) . s) . x = ((MSNat_Hom (A,C)) . s) . y ; :: thesis: [x,y] in C . s
Class ((C . s),x) = (MSNat_Hom (A,C,s)) . x by MSUALG_4:def 15
.= Class ((C . s),y) by A1, A2, MSUALG_4:def 15 ;
hence [x,y] in C . s by EQREL_1:35; :: thesis: verum

end;

assume A3: [x,y] in C . s ; :: thesis: ((MSNat_Hom (A,C)) . s) . x = ((MSNat_Hom (A,C)) . s) . y
thus ((MSNat_Hom (A,C)) . s) . x = Class ((C . s),x) by A1, MSUALG_4:def 15
.= Class ((C . s),y) by A3, EQREL_1:35
.= ((MSNat_Hom (A,C)) . s) . y by A1, MSUALG_4:def 15 ; :: thesis: verum