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