:: deftheorem Def3 defines c3compl PARSP_1:def 3 :
for F being Field
for b₂ being UnOp of [: the carrier of F, the carrier of F, the carrier of F:] holds
( b₂ = c3compl F iff for x being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds b₂ . x = [(- (x `1_3)),(- (x `2_3)),(- (x `3_3))] );