theorem Th56: :: MATRIX_4:56

for K being Ring
for x, y, z being FinSequence of K st len x = len y & len y = len z holds
mlt ((x + y),z) = (mlt (x,z)) + (mlt (y,z))