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