:: deftheorem Def9 defines QuotOpSeq ALG_1:def 9 :
for U1 being Universal_Algebra
for E being Congruence of U1
for b₃ being PFuncFinSequence of (Class E) holds
( b₃ = QuotOpSeq (U1,E) iff ( len b₃ = len the charact of U1 & ( for n being Nat st n in dom b₃ holds
for o1 being operation of U1 st the charact of U1 . n = o1 holds
b₃ . n = QuotOp (o1,E) ) ) );