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

proof

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

end;

A8: len (Inv A) = n by MATRIX_0:24;
( x = (Inv A) * y implies A * x = y )

proof

assume A9: x = (Inv A) * y ; :: thesis: A * x = y
thus y = (1_Rmatrix n) * y by A3, A4, Th86
.= (A * (Inv A)) * y by A1, Def6
.= A * x by A3, A4, A8, A5, A9, Th59 ; :: thesis: verum

end;

hence ( x = (Inv A) * y implies A * x = y ) ; :: thesis: verum