theorem :: MATRIXC1:32
for x, y, z being FinSequence of COMPLEX st len x = len y & len y = len z holds
mlt ((x - y),z) = (mlt (x,z)) - (mlt (y,z))