let n be Nat; :: thesis: for a being Real
for M being Matrix of n,REAL
for x being FinSequence of REAL st n > 0 & len x = n holds
a * (M * x) = (a * M) * x
let a be Real; :: thesis: for M being Matrix of n,REAL
for x being FinSequence of REAL st n > 0 & len x = n holds
a * (M * x) = (a * M) * x
let M be Matrix of n,REAL; :: thesis: for x being FinSequence of REAL st n > 0 & len x = n holds
a * (M * x) = (a * M) * x
let x be FinSequence of REAL ; :: thesis: ( n > 0 & len x = n implies a * (M * x) = (a * M) * x )
assume that
A1: n > 0 and
A2: len x = n ; :: thesis: a * (M * x) = (a * M) * x
width M = n by MATRIX_0:24;
then M * (a * x) = a * (M * x) by A1, A2, MATRIXR1:59;
hence a * (M * x) = (a * M) * x by A1, A2, Th50; :: thesis: verum