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 that
A1: len A > 0 and
A2: width A > 0 and
A3: ( width A = len x or len (A @) = len x ) ; :: thesis: A * x = x * (A @)
( len (A @) = width A & width (A @) = len A ) by A2, MATRIX_0:54;
then ((A @) @) * x = x * (A @) by A1, A2, A3, Th52;
hence A * x = x * (A @) by A1, A2, MATRIX_0:57; :: thesis: verum