:: deftheorem Def12 defines complop PRVECT_1:def 13 :
for g being non empty non-empty-addLoopStr-yielding FinSequence
for b₂ being UnOps of carr g holds
( b₂ = complop g iff ( len b₂ = len (carr g) & ( for i being Element of dom (carr g) holds b₂ . i = comp (g . i) ) ) );