let n be Nat; :: thesis: for A being Matrix of n,REAL st A is invertible holds
for y being FinSequence of REAL st len y = n holds
ex x being FinSequence of REAL st
( len x = n & x * A = y )
let A be Matrix of n,REAL; :: thesis: ( A is invertible implies for y being FinSequence of REAL st len y = n holds
ex x being FinSequence of REAL st
( len x = n & x * A = y ) )
assume A1: A is invertible ; :: thesis: for y being FinSequence of REAL st len y = n holds
ex x being FinSequence of REAL st
( len x = n & x * A = y )
let y be FinSequence of REAL ; :: thesis: ( len y = n implies ex x being FinSequence of REAL st
( len x = n & x * A = y ) )
assume A2: len y = n ; :: thesis: ex x being FinSequence of REAL st
( len x = n & x * A = y )
reconsider x0 = y * (Inv A) as FinSequence of REAL ;
len (Inv A) = n by MATRIX_0:24;
then A3: len x0 = width (Inv A) by A2, MATRIXR1:62
.= n by MATRIX_0:24 ;
then x0 * A = y by A1, A2, Th89;
hence ex x being FinSequence of REAL st
( len x = n & x * A = y ) by A3; :: thesis: verum