theorem Th14: :: MSUALG_5:14

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for o being OperSymbol of S
for C1, C2 being MSCongruence of A
for C being MSEquivalence-like ManySortedRelation of A st C = C1 "\/" C2 holds
for x, y being Element of Args (o,A) st ( for n being Nat st n in dom x holds
[(x . n),(y . n)] in C . ((the_arity_of o) /. n) ) holds
[((Den (o,A)) . x),((Den (o,A)) . y)] in C . (the_result_sort_of o)