let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra of 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 of 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 18;

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 17
.= Class (C . s),y by A1, A2, MSUALG_4:def 17 ;
hence [x,y] in C . s by EQREL_1:44; :: 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 17
.= Class (C . s),y by A3, EQREL_1:44
.= ((MSNat_Hom A,C) . s) . y by A1, MSUALG_4:def 17 ; :: thesis: verum