let n be Element of NAT ; :: thesis: for x, y being FinSequence of REAL
for A being Matrix of n, REAL st A is invertible & len x = n & len y = n holds
( x * A = y iff x = y * (Inv A) )
let x, y be FinSequence of REAL ; :: thesis: for A being Matrix of n, REAL st A is invertible & len x = n & len y = n holds
( x * A = y iff x = y * (Inv A) )
let A be Matrix of n, REAL ; :: thesis: ( A is invertible & len x = n & len y = n implies ( x * A = y iff x = y * (Inv A) ) )
assume A1: ( A is invertible & len x = n & len y = n ) ; :: thesis: ( x * A = y iff x = y * (Inv A) )
A2: ( len A = n & width A = n ) by MATRIX_1:25;
A3: ( len (Inv A) = n & width (Inv A) = n ) by MATRIX_1:25;
thus ( x * A = y implies x = y * (Inv A) ) :: thesis: ( x = y * (Inv A) implies x * A = y )

proof

assume A4: x * A = y ; :: thesis: x = y * (Inv A)
thus x = x * (1_Rmatrix n) by A1, Th88
.= x * (A * (Inv A)) by A1, Def6
.= y * (Inv A) by A1, A2, A3, A4, Th57 ; :: thesis: verum

end;

assume A5: x = y * (Inv A) ; :: thesis: x * A = y
thus y = y * (1_Rmatrix n) by A1, Th88
.= y * ((Inv A) * A) by A1, Def6
.= x * A by A1, A2, A3, A5, Th57 ; :: thesis: verum