for S being non empty non void ManySortedSign
for o being OperSymbol of S
for A being non-empty MSAlgebra over S
for R being MSCongruence of A
for x being set st x in (((Class R) #) * the Arity of S) . o holds
ex a being Element of Args (o,A) st x = R # a