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 x1, x2 being FinSequence of REAL st
( len x1 = n & len x2 = n & A * x1 = y & x2 * A = y ) ) holds
A is invertible
let A be Matrix of n,REAL; :: thesis: ( n > 0 & ( for y being FinSequence of REAL st len y = n holds
ex x1, x2 being FinSequence of REAL st
( len x1 = n & len x2 = n & A * x1 = y & x2 * A = y ) ) implies A is invertible )
assume that
A1: n > 0 and
A2: for y being FinSequence of REAL st len y = n holds
ex x1, x2 being FinSequence of REAL st
( len x1 = n & len x2 = n & A * x1 = y & x2 * A = y ) ; :: thesis: A is invertible
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 ex x1, x2 being FinSequence of REAL st
( len x1 = n & len x2 = n & A * x1 = y & x2 * A = y ) by A2;
hence ex x being FinSequence of REAL st
( len x = n & x * A = y ) ; :: thesis: verum

end;

then A3: ex B1 being Matrix of n,REAL st B1 * A = 1_Rmatrix n by Th93;
for y being FinSequence of REAL st len y = n holds
ex x being FinSequence of REAL st
( len x = n & A * x = y )

proof

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 len y = n ; :: thesis: ex x being FinSequence of REAL st
( len x = n & A * x = y )
then ex x1, x2 being FinSequence of REAL st
( len x1 = n & len x2 = n & A * x1 = y & x2 * A = y ) by A2;
hence ex x being FinSequence of REAL st
( len x = n & A * x = y ) ; :: thesis: verum

end;

then ex B2 being Matrix of n,REAL st A * B2 = 1_Rmatrix n by A1, Th96;
hence A is invertible by A3, Th80; :: thesis: verum