theorem Th57: :: MATRIXC1:59

for x, y being FinSequence of COMPLEX
for M being Matrix of COMPLEX st len x = width M & len y = len M & width M > 0 & len M > 0 holds
|((M * x),y)| = |(x,((M @") * y))|