let x be FinSequence of REAL ; :: thesis: for A being Matrix of REAL st len A > 0 & width A > 0 & ( width A = len x or len (A @ ) = len x ) holds
A * x = x * (A @ )
let A be Matrix of REAL ; :: thesis: ( len A > 0 & width A > 0 & ( width A = len x or len (A @ ) = len x ) implies A * x = x * (A @ ) )
assume A1: ( len A > 0 & width A > 0 & ( width A = len x or len (A @ ) = len x ) ) ; :: thesis: A * x = x * (A @ )
then ( len (A @ ) = width A & width (A @ ) = len A ) by MATRIX_2:12;
then ((A @ ) @ ) * x = x * (A @ ) by A1, Th52;
hence A * x = x * (A @ ) by A1, MATRIX_2:15; :: thesis: verum