:: Determinant and Inverse of Matrices of Real Elements
:: by Nobuyuki Tamura and Yatsuka Nakamura
::
:: Received July 17, 2007
:: Copyright (c) 2007-2021 Association of Mizar Users

Lm1: for F1, F2 being FinSequence of REAL
for j being Nat st len F1 = len F2 holds
(F1 - F2) . j = (F1 . j) - (F2 . j)

proof end;

theorem Th1: :: MATRIXR2:1

for x, y being FinSequence of REAL st len x = len y & x + y = 0* (len x) holds
( x = - y & y = - x )

proof end;

Lm2: for D being non empty set
for i being Nat
for A being Matrix of D st 1 <= i & i <= len A holds
Line (A,i) = A . i

proof end;

theorem Th2: :: MATRIXR2:2

for D being non empty set
for i, j being Nat
for A being Matrix of D
for p being FinSequence of D st p = A . i & 1 <= i & i <= len A & 1 <= j & j <= width A & len p = width A holds
A * (i,j) = p . j

proof end;

theorem Th3: :: MATRIXR2:3

for i, j being Nat
for a being Real
for A being Matrix of REAL st [i,j] in Indices A holds
(a * A) * (i,j) = a * (A * (i,j))

proof end;

theorem :: MATRIXR2:4

for n being Nat
for A, B being Matrix of n,REAL holds
( len (A * B) = len A & width (A * B) = width B & len (A * B) = n & width (A * B) = n )

proof end;

theorem Th5: :: MATRIXR2:5

for a being Real
for A being Matrix of REAL holds
( len (a * A) = len A & width (a * A) = width A )

proof end;

theorem Th6: :: MATRIXR2:6

for A, B being Matrix of REAL st len A = len B & width A = width B holds
( len (A - B) = len A & width (A - B) = width A & ( for i, j being Nat st [i,j] in Indices A holds
(A - B) * (i,j) = (A * (i,j)) - (B * (i,j)) ) )

proof end;

definition

let n be Nat;
let A, B be Matrix of n,REAL;
:: original: *
redefine func A * B -> Matrix of n,REAL;
coherence
A * B is Matrix of n,REAL ;

end;

theorem Th7: :: MATRIXR2:7

for A, B being Matrix of REAL st len A = len B & width A = width B & len A > 0 holds
A + (B - B) = A

proof end;

theorem :: MATRIXR2:8

for A, B being Matrix of REAL st len A = len B & width A = width B & len A > 0 holds
(A + B) - B = A

proof end;

Lm3: for i, j being Nat
for A being Matrix of REAL st [i,j] in Indices A holds
(- A) * (i,j) = - (A * (i,j))

proof end;

theorem Th9: :: MATRIXR2:9

for A being Matrix of REAL holds (- 1) * A = - A

proof end;

theorem Th10: :: MATRIXR2:10

for A being Matrix of REAL
for i, j being Nat st [i,j] in Indices A holds
(- A) * (i,j) = - (A * (i,j))

proof end;

theorem :: MATRIXR2:11

for a, b being Real
for A being Matrix of REAL holds (a * b) * A = a * (b * A)

proof end;

theorem Th12: :: MATRIXR2:12

for a, b being Real
for A being Matrix of REAL holds (a + b) * A = (a * A) + (b * A)

proof end;

theorem :: MATRIXR2:13

for a, b being Real
for A being Matrix of REAL holds (a - b) * A = (a * A) - (b * A)

proof end;

theorem Th14: :: MATRIXR2:14

for n being Nat
for K being Field
for A being Matrix of K st n > 0 & len A > 0 holds
(0. (K,n,(len A))) * A = 0. (K,n,(width A))

proof end;

theorem Th15: :: MATRIXR2:15

for K being Field
for A, C being Matrix of K st len A = width C & len C > 0 & len A > 0 holds
(- C) * A = - (C * A)

proof end;

theorem Th16: :: MATRIXR2:16

for K being Field
for A, B, C being Matrix of K st len B = len C & width B = width C & len A = width B & len B > 0 & len A > 0 holds
(B - C) * A = (B * A) - (C * A)

proof end;

theorem :: MATRIXR2:17

for A, B, C being Matrix of REAL st len A = len B & width A = width B & len C = width A & len A > 0 & len C > 0 holds
(A - B) * C = (A * C) - (B * C) by Th16;

theorem Th18: :: MATRIXR2:18

for K being Field
for m being Nat
for A, C being Matrix of K st width A > 0 & len A > 0 holds
A * (0. (K,(width A),m)) = 0. (K,(len A),m)

proof end;

theorem Th19: :: MATRIXR2:19

for K being Field
for A, C being Matrix of K st width A = len C & len A > 0 & len C > 0 holds
A * (- C) = - (A * C)

proof end;

theorem Th20: :: MATRIXR2:20

for K being Field
for A, B, C being Matrix of K st len B = len C & width B = width C & len B = width A & len B > 0 & len A > 0 holds
A * (B - C) = (A * B) - (A * C)

proof end;

theorem :: MATRIXR2:21

for A, B, C being Matrix of REAL st len A = len B & width A = width B & width C = len A & len C > 0 & len A > 0 holds
C * (A - B) = (C * A) - (C * B) by Th20;

theorem Th22: :: MATRIXR2:22

for A, B, C being Matrix of REAL st len A = len B & width A = width B & len C = len A & width C = width A & ( for i, j being Nat st [i,j] in Indices A holds
C * (i,j) = (A * (i,j)) - (B * (i,j)) ) holds
C = A - B

proof end;

theorem Th23: :: MATRIXR2:23

for x1, x2 being FinSequence of REAL st len x1 = len x2 holds
LineVec2Mx (x1 - x2) = (LineVec2Mx x1) - (LineVec2Mx x2)

proof end;

theorem Th24: :: MATRIXR2:24

for x1, x2 being FinSequence of REAL st len x1 = len x2 & len x1 > 0 holds
ColVec2Mx (x1 - x2) = (ColVec2Mx x1) - (ColVec2Mx x2)

proof end;

theorem Th25: :: MATRIXR2:25

for A, B being Matrix of REAL st len A = len B & width A = width B holds
for i being Nat st 1 <= i & i <= len A holds
Line ((A - B),i) = (Line (A,i)) - (Line (B,i))

proof end;

theorem Th26: :: MATRIXR2:26

for A, B being Matrix of REAL st len A = len B & width A = width B holds
for i being Nat st 1 <= i & i <= width A holds
Col ((A - B),i) = (Col (A,i)) - (Col (B,i))

proof end;

theorem :: MATRIXR2:27

for k, n, m, l being Nat
for A being Matrix of n,k,REAL
for B being Matrix of k,m,REAL
for C being Matrix of m,l,REAL st n > 0 & k > 0 & m > 0 holds
(A * B) * C = A * (B * C)

proof end;

theorem Th28: :: MATRIXR2:28

for n being Nat
for A, B, C being Matrix of n,REAL holds (A * B) * C = A * (B * C)

proof end;

theorem Th29: :: MATRIXR2:29

for D being non empty set
for n being Nat
for A being Matrix of n,D holds (A @) @ = A

proof end;

theorem Th30: :: MATRIXR2:30

for n being Nat
for A, B being Matrix of n,REAL holds (A * B) @ = (B @) * (A @)

proof end;

theorem Th31: :: MATRIXR2:31

for n, m being Nat
for A being Matrix of REAL st len A = n & width A = m holds
(- A) + A = 0_Rmatrix (n,m)

proof end;

definition

let n be Nat;
let A be Matrix of n,REAL;
:: original: MXR2MXF
redefine func MXR2MXF A -> Matrix of n,F_Real;
coherence
MXR2MXF A is Matrix of n,F_Real ;

end;

definition

let n be Nat;
let A be Matrix of n,REAL;

func Det A -> Real equals :: MATRIXR2:def 1
Det (MXR2MXF A);

coherence
Det (MXR2MXF A) is Real ;

end;

:: deftheorem defines Det MATRIXR2:def 1 :
for n being Nat
for A being Matrix of n,REAL holds Det A = Det (MXR2MXF A);

theorem :: MATRIXR2:32

for A being Matrix of 2,REAL holds Det A = ((A * (1,1)) * (A * (2,2))) - ((A * (1,2)) * (A * (2,1)))

proof end;

theorem Th33: :: MATRIXR2:33

for n being Nat
for s1, s2, s3 being FinSequence st len s1 = n & len s2 = n & len s3 = n holds
<*s1,s2,s3*> is tabular

proof end;

theorem Th34: :: MATRIXR2:34

for D being non empty set
for n being Nat
for p1, p2, p3 being FinSequence of D st len p1 = n & len p2 = n & len p3 = n holds
<*p1,p2,p3*> is Matrix of 3,n,D

proof end;

theorem Th35: :: MATRIXR2:35

for D being non empty set
for a1, a2, a3, b1, b2, b3, c1, c2, c3 being Element of D holds <*<*a1,a2,a3*>,<*b1,b2,b3*>,<*c1,c2,c3*>*> is Matrix of 3,D

proof end;

theorem Th36: :: MATRIXR2:36

for D being non empty set
for n being Nat
for A being Matrix of n,D
for p being FinSequence of D
for i being Nat st p = A . i & i in Seg n holds
len p = n

proof end;

theorem Th37: :: MATRIXR2:37

for D being non empty set
for A being Matrix of 3,D holds A = <*<*(A * (1,1)),(A * (1,2)),(A * (1,3))*>,<*(A * (2,1)),(A * (2,2)),(A * (2,3))*>,<*(A * (3,1)),(A * (3,2)),(A * (3,3))*>*>

proof end;

theorem :: MATRIXR2:38

for A being Matrix of 3,REAL holds Det A = (((((((A * (1,1)) * (A * (2,2))) * (A * (3,3))) - (((A * (1,3)) * (A * (2,2))) * (A * (3,1)))) - (((A * (1,1)) * (A * (2,3))) * (A * (3,2)))) + (((A * (1,2)) * (A * (2,3))) * (A * (3,1)))) - (((A * (1,2)) * (A * (2,1))) * (A * (3,3)))) + (((A * (1,3)) * (A * (2,1))) * (A * (3,2)))

proof end;

theorem :: MATRIXR2:39

for f being Permutation of (Seg 0) holds f = <*> NAT ;

Lm4: idseq 0 is Permutation of (Seg 0)
by FINSEQ_2:55;

theorem Th40: :: MATRIXR2:40

Permutations 0 = {(<*> NAT)}

proof end;

theorem Th41: :: MATRIXR2:41

for K being Ring
for A being Matrix of 0 ,K holds Det A = 1. K

proof end;

theorem :: MATRIXR2:42

for A being Matrix of 0 ,REAL holds Det A = 1

proof end;

:: Removing condition n>=1 from MATRIX7:37

theorem Th43: :: MATRIXR2:43

for K being Field
for n being Nat
for A being Matrix of n,K holds Det A = Det (A @)

proof end;

theorem :: MATRIXR2:44

for n being Nat
for A being Matrix of n,REAL holds Det A = Det (A @) by Th43;

:: Removing condition n>0 from MATRIX11:62

theorem Th45: :: MATRIXR2:45

for n being Nat
for K being Field
for A, B being Matrix of n,K holds Det (A * B) = (Det A) * (Det B)

proof end;

theorem Th46: :: MATRIXR2:46

for n being Nat
for A, B being Matrix of n,REAL holds Det (A * B) = (Det A) * (Det B)

proof end;

theorem :: MATRIXR2:47

for x, y being FinSequence of REAL
for A being Matrix of REAL st len x = len A & len y = len x & len x > 0 holds
(x - y) * A = (x * A) - (y * A)

proof end;

theorem :: MATRIXR2:48

for x, y being FinSequence of REAL
for A being Matrix of REAL st len x = width A & len y = len x & len x > 0 & len A > 0 holds
A * (x - y) = (A * x) - (A * y)

proof end;

theorem :: MATRIXR2:49

for x being FinSequence of REAL
for A being Matrix of REAL st len A = len x & len x > 0 & width A > 0 holds
(- x) * A = - (x * A)

proof end;

theorem :: MATRIXR2:50

for x being FinSequence of REAL
for A being Matrix of REAL st len x = width A & len x > 0 holds
A * (- x) = - (A * x)

proof end;

theorem :: MATRIXR2:51

for x being FinSequence of REAL
for A being Matrix of REAL st len x = len A & len x > 0 holds
x * (- A) = - (x * A)

proof end;

theorem :: MATRIXR2:52

for x being FinSequence of REAL
for A being Matrix of REAL st len x = width A & len A > 0 & len x > 0 holds
(- A) * x = - (A * x)

proof end;

theorem :: MATRIXR2:53

for a being Real
for x being FinSequence of REAL
for A being Matrix of REAL st width A = len x & len x > 0 holds
A * (a * x) = a * (A * x)

proof end;

theorem :: MATRIXR2:54

for x being FinSequence of REAL
for A, B being Matrix of REAL st len x = len A & len A = len B & width A = width B & len A > 0 holds
x * (A - B) = (x * A) - (x * B)

proof end;

theorem :: MATRIXR2:55

for x being FinSequence of REAL
for A, B being Matrix of REAL st len x = width A & len A = len B & width A = width B & len x > 0 & len A > 0 holds
(A - B) * x = (A * x) - (B * x)

proof end;

theorem Th56: :: MATRIXR2:56

for x being FinSequence of REAL
for A being Matrix of REAL st len A = len x holds
(LineVec2Mx x) * A = LineVec2Mx (x * A)

proof end;

theorem Th57: :: MATRIXR2:57

for x being FinSequence of REAL
for A, B being Matrix of REAL st len x = len A & width A = len B holds
x * (A * B) = (x * A) * B

proof end;

theorem Th58: :: MATRIXR2:58

for x being FinSequence of REAL
for A being Matrix of REAL st width A = len x & len x > 0 & len A > 0 holds
A * (ColVec2Mx x) = ColVec2Mx (A * x)

proof end;

theorem Th59: :: MATRIXR2:59

for x being FinSequence of REAL
for A, B being Matrix of REAL st len x = width B & width A = len B & len x > 0 & len B > 0 holds
(A * B) * x = A * (B * x)

proof end;

theorem :: MATRIXR2:60

for k, n, m being Nat
for B being Matrix of n,m,REAL
for A being Matrix of m,k,REAL st n > 0 holds
for i, j being Nat st [i,j] in Indices (B * A) holds
(B * A) * (i,j) = ((Line (B,i)) * A) . j

proof end;

theorem Th61: :: MATRIXR2:61

for n being Nat
for A, B being Matrix of n,REAL
for i, j being Nat st [i,j] in Indices (B * A) holds
(B * A) * (i,j) = ((Line (B,i)) * A) . j

proof end;

theorem :: MATRIXR2:62

for n being Nat
for A, B being Matrix of n,REAL st n > 0 holds
for i, j being Nat st [i,j] in Indices (A * B) holds
(A * B) * (i,j) = (A * (Col (B,j))) . i

proof end;

definition

let n be Nat;

func 1_Rmatrix n -> Matrix of n,REAL equals :: MATRIXR2:def 2
MXF2MXR (1. (F_Real,n));

correctness
coherence
MXF2MXR (1. (F_Real,n)) is Matrix of n,REAL;
;

end;

:: deftheorem defines 1_Rmatrix MATRIXR2:def 2 :
for n being Nat holds 1_Rmatrix n = MXF2MXR (1. (F_Real,n));

theorem Th63: :: MATRIXR2:63

for n being Nat holds
( ( for i being Nat st [i,i] in Indices (1_Rmatrix n) holds
(1_Rmatrix n) * (i,i) = 1 ) & ( for i, j being Nat st [i,j] in Indices (1_Rmatrix n) & i <> j holds
(1_Rmatrix n) * (i,j) = 0 ) )

proof end;

theorem Th64: :: MATRIXR2:64

for n being Nat holds (1_Rmatrix n) @ = 1_Rmatrix n

proof end;

theorem Th65: :: MATRIXR2:65

for n, m being Nat st n > 0 holds
(0_Rmatrix (n,m)) + (0_Rmatrix (n,m)) = 0_Rmatrix (n,m)

proof end;

theorem :: MATRIXR2:66

for n, m being Nat
for a being Real st n > 0 holds
a * (0_Rmatrix (n,m)) = 0_Rmatrix (n,m)

proof end;

theorem Th67: :: MATRIXR2:67

for K being Field
for A being Matrix of K holds A * (1. (K,(width A))) = A

proof end;

theorem Th68: :: MATRIXR2:68

for K being Field
for A being Matrix of K holds (1. (K,(len A))) * A = A

proof end;

theorem :: MATRIXR2:69

for n, m being Nat
for A being Matrix of REAL holds
( ( n = width A implies A * (1_Rmatrix n) = A ) & ( m = len A implies (1_Rmatrix m) * A = A ) ) by Th67, Th68;

theorem Th70: :: MATRIXR2:70

for n being Nat
for A being Matrix of n,REAL holds (1_Rmatrix n) * A = A

proof end;

theorem Th71: :: MATRIXR2:71

for n being Nat
for A being Matrix of n,REAL holds A * (1_Rmatrix n) = A

proof end;

theorem Th72: :: MATRIXR2:72

for n being Nat holds Det (1_Rmatrix n) = 1

proof end;

definition

let n be Nat;

func 0_Rmatrix n -> Matrix of n,REAL equals :: MATRIXR2:def 3
0_Rmatrix (n,n);

correctness
coherence
0_Rmatrix (n,n) is Matrix of n,REAL;
;

end;

:: deftheorem defines 0_Rmatrix MATRIXR2:def 3 :
for n being Nat holds 0_Rmatrix n = 0_Rmatrix (n,n);

theorem :: MATRIXR2:73

for n being Nat st n > 0 holds
Det (0_Rmatrix n) = 0

proof end;

definition

let n, i be Nat;

func Base_FinSeq (n,i) -> FinSequence of REAL equals :: MATRIXR2:def 4
(n |-> 0) +* (i,1);

coherence
(n |-> 0) +* (i,1) is FinSequence of REAL

proof end;

end;

:: deftheorem defines Base_FinSeq MATRIXR2:def 4 :
for n, i being Nat holds Base_FinSeq (n,i) = (n |-> 0) +* (i,1);

theorem Th74: :: MATRIXR2:74

for n, i being Nat holds len (Base_FinSeq (n,i)) = n

proof end;

theorem Th75: :: MATRIXR2:75

for n, i being Nat st 1 <= i & i <= n holds
(Base_FinSeq (n,i)) . i = 1

proof end;

theorem Th76: :: MATRIXR2:76

for n, i, j being Nat st 1 <= j & j <= n & i <> j holds
(Base_FinSeq (n,i)) . j = 0

proof end;

theorem :: MATRIXR2:77

( Base_FinSeq (1,1) = <*1*> & Base_FinSeq (2,1) = <*1,0*> & Base_FinSeq (2,2) = <*0,1*> & Base_FinSeq (3,1) = <*1,0,0*> & Base_FinSeq (3,2) = <*0,1,0*> & Base_FinSeq (3,3) = <*0,0,1*> )

proof end;

theorem Th78: :: MATRIXR2:78

for i, n being Nat st 1 <= i & i <= n holds
(1_Rmatrix n) . i = Base_FinSeq (n,i)

proof end;

definition

let n be Nat;
let A be Matrix of n,REAL;

attr A is invertible means :: MATRIXR2:def 5
ex B being Matrix of n,REAL st
( B * A = 1_Rmatrix n & A * B = 1_Rmatrix n );

end;

:: deftheorem defines invertible MATRIXR2:def 5 :
for n being Nat
for A being Matrix of n,REAL holds
( A is invertible iff ex B being Matrix of n,REAL st
( B * A = 1_Rmatrix n & A * B = 1_Rmatrix n ) );

definition

let n be Nat;
let A be Matrix of n,REAL;
assume A1: A is invertible ;

func Inv A -> Matrix of n,REAL means :Def6: :: MATRIXR2:def 6
( it * A = 1_Rmatrix n & A * it = 1_Rmatrix n );

existence
ex b₁ being Matrix of n,REAL st
( b₁ * A = 1_Rmatrix n & A * b₁ = 1_Rmatrix n ) by A1;
uniqueness
for b₁, b₂ being Matrix of n,REAL st b₁ * A = 1_Rmatrix n & A * b₁ = 1_Rmatrix n & b₂ * A = 1_Rmatrix n & A * b₂ = 1_Rmatrix n holds
b₁ = b₂

proof end;

end;

:: deftheorem Def6 defines Inv MATRIXR2:def 6 :
for n being Nat
for A being Matrix of n,REAL st A is invertible holds
for b₃ being Matrix of n,REAL holds
( b₃ = Inv A iff ( b₃ * A = 1_Rmatrix n & A * b₃ = 1_Rmatrix n ) );

registration

let n be Nat;

cluster 1_Rmatrix n -> invertible ;

coherence
1_Rmatrix n is invertible

proof end;

end;

theorem :: MATRIXR2:79

for n being Nat holds Inv (1_Rmatrix n) = 1_Rmatrix n

proof end;

theorem Th80: :: MATRIXR2:80

for n being Nat
for A, B1, B2 being Matrix of n,REAL st B1 * A = 1_Rmatrix n & A * B2 = 1_Rmatrix n holds
( B1 = B2 & A is invertible )

proof end;

theorem :: MATRIXR2:81

for n being Nat
for A being Matrix of n,REAL st A is invertible holds
Det (Inv A) = (Det A) "

proof end;

theorem :: MATRIXR2:82

for n being Nat
for A being Matrix of n,REAL st A is invertible holds
Det A <> 0

proof end;

theorem :: MATRIXR2:83

for n being Nat
for A, B being Matrix of n,REAL st A is invertible & B is invertible holds
( A * B is invertible & Inv (A * B) = (Inv B) * (Inv A) )

proof end;

theorem :: MATRIXR2:84

for n being Nat
for A being Matrix of n,REAL st A is invertible holds
Inv (Inv A) = A

proof end;

theorem :: MATRIXR2:85

( 1_Rmatrix 0 = 0_Rmatrix 0 & 1_Rmatrix 0 = {} )

proof end;

theorem Th86: :: MATRIXR2:86

for n being Nat
for x being FinSequence of REAL st len x = n & n > 0 holds
(1_Rmatrix n) * x = x

proof end;

theorem Th87: :: MATRIXR2:87

for n being Nat
for x, y being FinSequence of REAL
for A being Matrix of n,REAL st A is invertible & len x = n & len y = n & n > 0 holds
( A * x = y iff x = (Inv A) * y )

proof end;

theorem Th88: :: MATRIXR2:88

for n being Nat
for x being FinSequence of REAL st len x = n holds
x * (1_Rmatrix n) = x

proof end;

theorem Th89: :: MATRIXR2:89

for n being Nat
for x, y being FinSequence of REAL
for A being Matrix of n,REAL st A is invertible & len x = n & len y = n holds
( x * A = y iff x = y * (Inv A) )

proof end;

theorem :: MATRIXR2:90

for n being Nat
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 )

proof end;

theorem :: MATRIXR2:91

for n being Nat
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 )

proof end;

theorem :: MATRIXR2:92

for n being Nat
for A being Matrix of n,REAL
for x, y being FinSequence of REAL st len x = n & len y = n & x * A = y holds
for j being Nat st 1 <= j & j <= n holds
y . j = |(x,(Col (A,j)))|

proof end;

theorem Th93: :: MATRIXR2:93

for n being Nat
for A being Matrix of n,REAL st ( for y being FinSequence of REAL st len y = n holds
ex x being FinSequence of REAL st
( len x = n & x * A = y ) ) holds
ex B being Matrix of n,REAL st B * A = 1_Rmatrix n

proof end;

theorem :: MATRIXR2:94

for n being Nat
for x being FinSequence of REAL
for A being Matrix of n,REAL st n > 0 & len x = n holds
(A @) * x = x * A

proof end;

theorem Th95: :: MATRIXR2:95

for n being Nat
for x being FinSequence of REAL
for A being Matrix of n,REAL st n > 0 & len x = n holds
x * (A @) = A * x

proof end;

theorem Th96: :: MATRIXR2:96

for n being Nat
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

proof end;

theorem :: MATRIXR2:97

for n being Nat
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

proof end;