:: deftheorem Defa defines vector_add VECTSP13:def 5 :
for R being Ring
for n being Nat
for b₃ being BinOp of (n -tuples_on the carrier of R) holds
( b₃ = vector_add (n,R) iff for u, v being Tuple of n, the carrier of R holds b₃ . (u,v) = u + v );