let n be 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 that
A1: A is invertible and
A2: len x = n and
A3: len y = n ; :: thesis: ( x * A = y iff x = y * (Inv A) )
A4: ( len A = n & len (Inv A) = n ) by MATRIX_0:24;
A5: width A = n by MATRIX_0:24;
thus ( x * A = y implies x = y * (Inv A) ) :: thesis: ( x = y * (Inv A) implies x * A = y )

proof

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

end;

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