theorem Th13: :: MSUALG_5:13

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 x1, y1 being object
for n being Element of NAT
for a1, a2, b1 being FinSequence st len a1 = n & len a1 = len a2 & ( for k being Element of NAT st k in dom a1 holds
[(a1 . k),(a2 . k)] in C . ((the_arity_of o) /. k) ) & [((Den (o,A)) . ((a1 ^ <*x1*>) ^ b1)),((Den (o,A)) . ((a2 ^ <*x1*>) ^ b1))] in C . (the_result_sort_of o) & [x1,y1] in C . ((the_arity_of o) /. (n + 1)) holds
for x being Element of Args (o,A) st x = (a1 ^ <*x1*>) ^ b1 holds
[((Den (o,A)) . x),((Den (o,A)) . ((a2 ^ <*y1*>) ^ b1))] in C . (the_result_sort_of o)