let n be Element of 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 )
A2: len (Inv A) = n by MATRIX_1:25;
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 A3: 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 ;
A4: len x0 = width (Inv A) by A2, A3, MATRIXR1:62
.= n by MATRIX_1:25 ;
then x0 * A = y by A1, A3, Th89;
hence ex x being FinSequence of REAL st
( len x = n & x * A = y ) by A4; :: thesis: verum