:: deftheorem Def1 defines c3add PARSP_1:def 1 :
for F being Field
for b₂ being BinOp of [: the carrier of F, the carrier of F, the carrier of F:] holds
( b₂ = c3add F iff for x, y being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds b₂ . (x,y) = [((x `1_3) + (y `1_3)),((x `2_3) + (y `2_3)),((x `3_3) + (y `3_3))] );