theorem :: MATRIXC1:34

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