let n be Element of 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 A1: ( 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 ) ) ) ; :: 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 consider x1, x2 being FinSequence of REAL such that
A2: ( len x1 = n & len x2 = n & A * x1 = y & x2 * A = y ) by A1;
thus ex x being FinSequence of REAL st
( len x = n & x * A = y ) by A2; :: thesis: verum

end;

then consider B1 being Matrix of n, REAL such that
A3: 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 consider x1, x2 being FinSequence of REAL such that
A4: ( len x1 = n & len x2 = n & A * x1 = y & x2 * A = y ) by A1;
thus ex x being FinSequence of REAL st
( len x = n & A * x = y ) by A4; :: thesis: verum

end;

then consider B2 being Matrix of n, REAL such that
A5: A * B2 = 1_Rmatrix n by A1, Th96;
thus A is invertible by A3, A5, Th80; :: thesis: verum