:: deftheorem Def8 defines QuotOp ALG_1:def 8 :
for U1 being Universal_Algebra
for E being Congruence of U1
for o being operation of U1
for b₄ being non empty homogeneous quasi_total PartFunc of ((Class E) *),(Class E) holds
( b₄ = QuotOp (o,E) iff ( dom b₄ = (arity o) -tuples_on (Class E) & ( for y being FinSequence of Class E st y in dom b₄ holds
for x being FinSequence of the carrier of U1 st x is_representatives_FS y holds
b₄ . y = Class (E,(o . x)) ) ) );