let n be Nat; :: thesis: for A being Matrix of n,REAL st n > 0 & 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 & A * x = y )
let A be Matrix of n,REAL; :: thesis: ( n > 0 & 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 & A * x = y ) )
assume that
A1: n > 0 and
A2: 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 & A * x = y )
let y be FinSequence of REAL ; :: thesis: ( len y = n implies ex x being FinSequence of REAL st
( len x = n & A * x = y ) )
assume A3: len y = n ; :: thesis: ex x being FinSequence of REAL st
( len x = n & A * x = y )
reconsider x0 = (Inv A) * y as FinSequence of REAL ;
( len (Inv A) = n & width (Inv A) = n ) by MATRIX_0:24;
then A4: len x0 = n by A1, A3, MATRIXR1:61;
then A * x0 = y by A1, A2, A3, Th87;
hence ex x being FinSequence of REAL st
( len x = n & A * x = y ) by A4; :: thesis: verum