let n be Nat; :: thesis: for A being Matrix of n,REAL st n > 0 & ( for y being FinSequence of REAL st len y = n holds
ex x being FinSequence of REAL st
( len x = n & A * x = y ) ) holds
ex B being Matrix of n,REAL st A * B = 1_Rmatrix n
let A be Matrix of n,REAL; :: thesis: ( n > 0 & ( for y being FinSequence of REAL st len y = n holds
ex x being FinSequence of REAL st
( len x = n & A * x = y ) ) implies ex B being Matrix of n,REAL st A * B = 1_Rmatrix n )
assume that
A1: n > 0 and
A2: for y being FinSequence of REAL st len y = n holds
ex x being FinSequence of REAL st
( len x = n & A * x = y ) ; :: thesis: ex B being Matrix of n,REAL st A * B = 1_Rmatrix n
for y being FinSequence of REAL st len y = n holds
ex x being FinSequence of REAL st
( len x = n & x * (A @) = y )
proof
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 len y = n ; :: thesis: ex x being FinSequence of REAL st
( len x = n & x * (A @) = y )
then consider x0 being FinSequence of REAL such that
A3: len x0 = n and
A4: A * x0 = y by A2;
x0 * (A @) = A * x0 by A1, A3, Th95;
hence ex x being FinSequence of REAL st
( len x = n & x * (A @) = y ) by A3, A4; :: thesis: verum
end;
then consider B being Matrix of n,REAL such that
A5: B * (A @) = 1_Rmatrix n by Th93;
(B * (A @)) @ = 1_Rmatrix n by A5, Th64;
then ((A @) @) * (B @) = 1_Rmatrix n by Th30;
then A * (B @) = 1_Rmatrix n by Th29;
hence ex B being Matrix of n,REAL st A * B = 1_Rmatrix n ; :: thesis: verum