:: deftheorem defines QuotArgs MSUALG_4:def 11 :
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for R being MSCongruence of A
for b₄ being ManySortedFunction of ( the Sorts of A #) * the Arity of S,((Class R) #) * the Arity of S holds
( b₄ = QuotArgs R iff for o being OperSymbol of S holds b₄ . o = QuotArgs (R,o) );