:: deftheorem Def7 defines Congruence ALG_1:def 7 :
for U1 being Universal_Algebra
for b₂ being Equivalence_Relation of U1 holds
( b₂ is Congruence of U1 iff for n being Nat
for o1 being operation of U1 st n in dom the charact of U1 & o1 = the charact of U1 . n holds
for x, y being FinSequence of U1 st x in dom o1 & y in dom o1 & [x,y] in ExtendRel b₂ holds
[(o1 . x),(o1 . y)] in b₂ );