let n be Nat; :: thesis: for x being FinSequence of REAL
for A being Matrix of n,REAL st n > 0 & len x = n holds
x * (A @) = A * x
let x be FinSequence of REAL ; :: thesis: for A being Matrix of n,REAL st n > 0 & len x = n holds
x * (A @) = A * x
let A be Matrix of n,REAL; :: thesis: ( n > 0 & len x = n implies x * (A @) = A * x )
A1: ( len A = n & width A = n ) by MATRIX_0:24;
assume ( n > 0 & len x = n ) ; :: thesis: x * (A @) = A * x
hence x * (A @) = A * x by A1, MATRIXR1:53; :: thesis: verum