theorem Th31: :: MATRIXC1:33

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))