:: deftheorem Def6 defines matrix_add MATGRP_0:def 6 :
for n being Nat
for L being non empty doubleLoopStr
for b₃ being BinOp of (n -Matrices_over L) holds
( b₃ = matrix_add (n,L) iff for A, B being Element of n -Matrices_over L holds b₃ . (A,B) = A + B );