theorem Th20: :: MATRIXJ1:20

for D being non empty set
for M1, M2 being Matrix of D holds Sum (Width <*M1,M2*>) = (width M1) + (width M2)