theorem Th73: :: MATGRP_0:61

for n being Nat
for L being non empty doubleLoopStr
for A, B being Matrix of n,L
for X, Y being Element of (Matrix_ring (n,L)) st A = X & B = Y holds
A + B = X + Y by Def6;