:: Determinant and Inverse of Matrices of Real Elements
::  by Nobuyuki Tamura and Yatsuka Nakamura
::
:: Received July 17, 2007
:: Copyright (c) 2007-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, XBOOLE_0, SUBSET_1, VECTSP_1, FINSEQ_1, ARYTM_1,
      FUNCT_1, FINSEQ_2, ARYTM_3, EUCLID, MATRIX_1, XXREAL_0, INCSP_1, RELAT_1,
      TREES_1, TARSKI, XREAL_0, ORDINAL1, MATRIXR1, CARD_1, NAT_1, REAL_1,
      SUPINF_2, QC_LANG1, ZFMISC_1, FVSUM_1, MATRIX_3, FUNCT_2, MATRIX_2,
      MESFUNC1, GROUP_1, ABIAN, BINOP_1, ALGSTR_0, SETWISEO, CARD_3, RVSUM_1,
      FUNCT_4, AFINSQ_1, PRALG_1, PARTFUN1, MATRIXR2;
 notations TARSKI, XBOOLE_0, SUBSET_1, XXREAL_0, ZFMISC_1, ORDINAL1, NUMBERS,
      ENUMSET1, SETWOP_2, XCMPLX_0, XREAL_0, REAL_1, FUNCT_1, PARTFUN1,
      BINOP_1, FUNCT_2, FINSEQ_1, FINSEQ_2, FINSEQ_4, FUNCT_7, STRUCT_0,
      ALGSTR_0, MATRIX_1, FVSUM_1, FINSEQ_7, SETWISEO, GROUP_1, MATRIX_2,
      MATRIX_3, MATRIX_6, MATRIXR1, EUCLID, MATRIX_7, MATRIX_4, RVSUM_1,
      VECTSP_1, MATRPROB;
 constructors FVSUM_1, BINOP_2, FINSEQ_7, SETWISEO, FINSOP_1, FINSEQ_4,
      MATRIX_7, MATRIXR1, MATRIX_6, REAL_1, SEQ_1, RVSUM_1, EUCLID, RELSET_1;
 registrations FINSEQ_2, NAT_1, RELSET_1, MEMBERED, STRUCT_0, VECTSP_1,
      NUMBERS, XXREAL_0, MATRIX_2, FINSEQ_1, FVSUM_1, FINSET_1, XBOOLE_0,
      VALUED_0, CARD_1, FUNCT_7;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
 definitions TARSKI, MATRIX_1, STRUCT_0, RLVECT_1, VECTSP_1, MATRIXR1,
      FINSEQ_1, VALUED_1;
 theorems MATRIX_3, VECTSP_1, MATRIX_1, MATRIX_4, GROUP_1, XREAL_0, FUNCT_1,
      FINSEQ_1, NAT_1, FINSEQ_7, MATRIX_2, FINSEQ_2, TARSKI, FINSOP_1, FVSUM_1,
      SETWISEO, XBOOLE_0, ENUMSET1, XCMPLX_0, ZFMISC_1, MATRIX_7, MATRIXR1,
      FINSEQ_3, XXREAL_0, RVSUM_1, ORDINAL1, MATRIX10, MATRIX11, MATRPROB,
      FINSEQ_4, MATRIX_9, MATRIXC1, PARTFUN1, FUNCT_7, CARD_1;
 schemes FINSEQ_4;

begin :: Preliminaries

reserve x for set,
  D for non empty set,
  k,n,m,i,j,l for Element of NAT ,
  K for Field;

Lm1: for F1,F2 being FinSequence of REAL,j st len F1=len F2 holds (F1-F2).j=F1
.j - F2.j
proof
  let F1,F2 be FinSequence of REAL,j;
  reconsider n=len F1 as Element of NAT;
  reconsider G1=F1 as Element of n-tuples_on REAL by FINSEQ_2:92;
  assume len F1=len F2;
  then reconsider G2=F2 as Element of n-tuples_on REAL by FINSEQ_2:92;
  (G1-G2).j=(G1.j) - (G2.j) by RVSUM_1:27;
  hence thesis;
end;

theorem Th1:
  for x,y being FinSequence of REAL st len x=len y & x+y=0*(len x)
  holds x=-y & y=-x
proof
  let x,y be FinSequence of REAL;
  assume that
A1: len x=len y and
A2: x+y=0*(len x);
A3: x=0*(len x) -y by A1,A2,MATRIXR1:14;
  hence x=-y by A1,MATRIXR1:6;
  thus -x=--y by A1,A3,MATRIXR1:6
    .=y;
end;

Lm2: for A being Matrix of D st 1<=i & i<=len A holds Line(A,i)=A.i
proof
  let A be Matrix of D;
  assume 1<=i & i<=len A;
  then i in dom A by FINSEQ_3:25;
  hence thesis by MATRIX_2:16;
end;

theorem Th2:
  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
  let A be Matrix of D;
  let p be FinSequence of D;
  assume that
A1: p=A.i and
A2: 1<=i & i<=len A and
A3: 1<=j & j<=width A and
A4: len p=width A;
A5: j in Seg width A by A3;
  then j in dom p by A4,FINSEQ_1:def 3;
  then rng p c= D & p.j in rng p by FINSEQ_1:def 4,FUNCT_1:def 3;
  then reconsider xp=p.j as Element of D;
A6: xp=p.j;
  i in dom A by A2,FINSEQ_3:25;
  then [i,j] in Indices A by A5,ZFMISC_1:87;
  hence thesis by A1,A6,MATRIX_1:def 5;
end;

theorem Th3:
  for a being real number, A being Matrix of REAL st [i,j] in
  Indices A holds (a*A)*(i,j) = a*(A*(i,j))
proof
  let a be real number,A be Matrix of REAL;
  assume
A1: [i,j] in Indices A;
  reconsider aa=a as Element of F_Real by XREAL_0:def 1;
  (a*A)*(i,j) = (MXF2MXR (aa*(MXR2MXF A)))*(i,j) by MATRIXR1:def 7
    .= aa*((MXR2MXF A)*(i,j)) by A1,MATRIX_3:def 5
    .= a*(A*(i,j));
  hence thesis;
end;

theorem Th4:
  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
  let A,B be Matrix of n,REAL;
A1: len B=n by MATRIX_1:25;
A2: len A=n by MATRIX_1:25;
  per cases;
  suppose
A3: n>0;
    then width MXR2MXF A =n by MATRIX_1:23
      .=len MXR2MXF B by MATRIX_1:25;
    then len (A*B)=len A & width (A*B)=width B by MATRIX_3:def 4;
    hence thesis by A1,A3,MATRIX_1:20,25;
  end;
  suppose
A4: n<=0;
    then
A5: width (MXR2MXF A) =0 by A2,MATRIX_1:def 3
      .=len (MXR2MXF B) by A4,MATRIX_1:25;
    then len (A*B) = len A by MATRIX_3:def 4;
    hence thesis by A2,A4,A5,MATRIX_1:def 3,MATRIX_3:def 4;
  end;
end;

theorem Th5:
  for a being real number,A being Matrix of REAL holds len (a*A)=
  len A & width (a*A)=width A
proof
  let a be real number,A be Matrix of REAL;
  reconsider ea=a as Element of F_Real by XREAL_0:def 1;
A1: width (a*A)= width MXR2MXF MXF2MXR (ea*(MXR2MXF A)) by MATRIXR1:def 7
    .= width A by MATRIX_3:def 5;
  len (a*A)= len MXR2MXF MXF2MXR (ea*(MXR2MXF A)) by MATRIXR1:def 7
    .= len A by MATRIX_3:def 5;
  hence thesis by A1;
end;

begin :: Calculation of Matrices

theorem Th6:
  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 holds [i,j] in Indices
  A implies (A-B)*(i,j) = A*(i,j) - B*(i,j)
proof
  let A,B be Matrix of REAL;
  assume
A1: len A=len B & width A=width B;
  thus len (A - B) =len (MXF2MXR ((MXR2MXF A)+-(MXR2MXF B))) by MATRIX_4:def 1
    .=len A by MATRIX_3:def 3;
  thus width (A - B) =width (MXF2MXR ((MXR2MXF A)+-(MXR2MXF B))) by
MATRIX_4:def 1
    .=width A by MATRIX_3:def 3;
  thus thesis by A1,MATRIX10:3;
end;

definition
  let n;
  let A,B be Matrix of n,REAL;
  redefine func A*B -> Matrix of n,REAL;
  coherence
  proof
A1: len A=n & width B=n by MATRIX_1:24;
    len (A*B)=len A & width (A*B)=width B by Th4;
    hence thesis by A1,MATRIX_2:7;
  end;
end;

theorem Th7:
  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
  let A,B be Matrix of REAL;
  assume len A=len B & width A=width B & len A>0;
  hence A=A+(0_Rmatrix(len B,width B)) by MATRIXR1:36
    .=MXF2MXR (MXR2MXF A)+ MXF2MXR ((MXR2MXF B)+(-(MXR2MXF B))) by MATRIX_4:2
    .=A + (B - B) by MATRIX_4:def 1;
end;

theorem
  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
  let A,B be Matrix of REAL;
  assume that
A1: len A=len B & width A=width B and
A2: len A>0;
  thus A + B - B =A + B+ - B by MATRIX_4:def 1
    .= A + (B +- B) by A1,MATRIX_3:3
    .= A+(B-B) by MATRIX_4:def 1
    .=A by A1,A2,Th7;
end;

Lm3: for A being Matrix of REAL st [i,j] in Indices A holds (-A)*(i,j)= -(A*(i
,j))
proof
  let A be Matrix of REAL;
  assume [i,j] in Indices A;
  then (-A)*(i,j) = -((MXR2MXF A)*(i,j)) by MATRIX_3:def 2;
  hence thesis;
end;

theorem Th9:
  for A being Matrix of REAL holds (-1)*A = -A
proof
  let A be Matrix of REAL;
A1: width ((-1)*A) = width A by Th5;
A2: len (((-1) qua real number)*A) = len A by Th5;
A3: now
    let i,j be Nat;
    reconsider i0=i,j0=j as Element of NAT by ORDINAL1:def 12;
    assume
A4: [i,j] in Indices ((-1)*A);
    then
A5: 1<=j0 & j0<=width A by A1,MATRIXC1:1;
    1<= i0 & i0<=len A by A2,A4,MATRIXC1:1;
    then
A6: [i0,j0] in Indices A by A5,MATRIXC1:1;
    hence ((-1)*A)*(i,j) = (-1)*(A*(i0,j0)) by Th3
      .= -(A*(i,j))
      .= (-A)*(i,j) by A6,Lm3;
  end;
  len (-A) = len A & width (-A) = width A by MATRIX_3:def 2;
  hence thesis by A2,A1,A3,MATRIX_1:21;
end;

theorem Th10:
  for A being (Matrix of REAL), i,j being Element of NAT st [i,j]
  in Indices A holds (-A)*(i,j)=-(A*(i,j))
proof
  let A be (Matrix of REAL), i,j be Element of NAT;
  assume
A1: [i,j] in Indices A;
  -A=(-1)*A by Th9;
  then (-A)*(i,j)= (-1)*(A*(i,j)) by A1,MATRIXR1:29;
  hence thesis;
end;

theorem
  for a,b being Real,A being Matrix of REAL holds (a*b)*A=a*(b*A)
proof
  let a,b be Real,A be Matrix of REAL;
A1: len ((a*b)*A)=len A & width ((a*b)*A)=width A by Th5;
A2: len (a*(b*A))=len (b*A) by Th5;
A3: width (a*(b*A))=width (b*A) by Th5;
  then
A4: width (a*(b*A)) =width A by Th5;
A5: len (b*A)=len A & width (b*A)=width A by Th5;
A6: for i,j being Nat st [i,j] in Indices (a*(b*A)) holds (a*(b*A))*(i,j)=((
  a*b)*A)*(i,j)
  proof
    let i,j be Nat;
    assume
A7: [i,j] in Indices (a*(b*A));
A8: Indices ((b*A))=Indices (A) by A5,MATRIX_4:55;
    reconsider i0=i,j0=j as Element of NAT by ORDINAL1:def 12;
A9: Indices (a*(b*A))=Indices ((b*A)) by A2,A3,MATRIX_4:55;
    then (a*(b*A))*(i,j) = (a*((b*A)*(i0,j0))) by A7,Th3
      .= (a*(b*(A*(i0,j0)))) by A7,A9,A8,Th3
      .= (a*b)*(A*(i0,j0))
      .= ((a*b)*A)*(i,j) by A7,A9,A8,Th3;
    hence thesis;
  end;
  len (a*(b*A)) =len A by A2,Th5;
  hence thesis by A1,A4,A6,MATRIX_1:21;
end;

theorem Th12:
  for a,b being Real,A being Matrix of REAL holds (a+b)*A=a*A + b* A
proof
  let a,b be Real, A be Matrix of REAL;
A1: len (a*A)=len A & width (a*A)=width A by MATRIXR1:27;
A2: len ((a+b)*A)=len A & width ((a+b)*A)=width A by MATRIXR1:27;
A3: for i,j being Nat st [i,j] in Indices ((a+b)*A) holds ((a+b)*A)*(i,j)=(a
  *A + b*A)*(i,j)
  proof
    let i,j be Nat;
    assume
A4: [i,j] in Indices ((a+b)*A);
    reconsider i0=i,j0=j as Element of NAT by ORDINAL1:def 12;
A5: Indices ((a+b)*A)=Indices A by A2,MATRIX_4:55;
    Indices (a*A)=Indices A by A1,MATRIX_4:55;
    then (a*A + b*A)*(i,j) =(a*A)*(i0,j0)+(b*A)*(i0,j0) by A4,A5,MATRIXR1:25
      .=a*(A*(i0,j0))+(b*A)*(i0,j0) by A4,A5,MATRIXR1:29
      .=a*(A*(i0,j0))+b*(A*(i0,j0)) by A4,A5,MATRIXR1:29
      .=(a+b)*(A*(i,j));
    hence thesis by A4,A5,MATRIXR1:29;
  end;
  len (a*A + b*A) = len (a*A) & width (a*A + b*A) =width (a*A) by
MATRIX_3:def 3;
  hence thesis by A2,A1,A3,MATRIX_1:21;
end;

theorem
  for a,b being Real,A being Matrix of REAL holds (a-b)*A=a*A - b*A
proof
  let a,b be Real, A be Matrix of REAL;
A1: len ((a-b)*A)=len (A) & width ((a-b)*A)=width A by MATRIXR1:27;
A2: len (a*A)=len A & width (a*A)=width (A) by MATRIXR1:27;
A3: len (b*A)=len A & width (b*A)=width A by MATRIXR1:27;
A4: for i,j being Nat st [i,j] in Indices ((a-b)*A) holds ((a-b)*A)*(i,j)=(a
  *A - b*A)*(i,j)
  proof
    let i,j be Nat;
    assume
A5: [i,j] in Indices ((a-b)*A);
    reconsider i0=i,j0=j as Element of NAT by ORDINAL1:def 12;
A6: Indices ((a-b)*A)=Indices A by A1,MATRIX_4:55;
    Indices (a*A)=Indices A by A2,MATRIX_4:55;
    then (a*A - b*A)*(i,j) =(a*A)*(i0,j0)-(b*A)*(i0,j0) by A2,A3,A5,A6,Th6
      .=a*(A*(i0,j0))-(b*A)*(i0,j0) by A5,A6,MATRIXR1:29
      .=a*(A*(i0,j0))-b*(A*(i0,j0)) by A5,A6,MATRIXR1:29
      .=(a-b)*(A*(i,j));
    hence thesis by A5,A6,MATRIXR1:29;
  end;
A7: width (a*A - b*A) =width (MXF2MXR ((MXR2MXF (a*A))+-(MXR2MXF (b*A)))) by
MATRIX_4:def 1
    .=width (a*A) by MATRIX_3:def 3;
  len (a*A - b*A) =len (MXF2MXR ((MXR2MXF (a*A))+-(MXR2MXF (b*A)))) by
MATRIX_4:def 1
    .=len (a*A) by MATRIX_3:def 3;
  hence thesis by A1,A7,A2,A4,MATRIX_1:21;
end;

theorem Th14:
  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
  let A be Matrix of K;
  assume that
A1: n>0 and
A2: len A >0;
A3: len 0.(K,n,len A)=n by MATRIX_1:def 2;
  then
A4: width 0.(K,n,len A)=len A by A1,MATRIX_1:20;
  then
A5: len ((0.(K,n,len A))*A)=n by A3,MATRIX_3:def 4;
A6: width ((0.(K,n,len A))*A)=width A by A4,MATRIX_3:def 4;
  0.(K,n,len A)*A + 0.(K,n,len A)*A =(0.(K,n,len A)+ 0.(K,n,len A))*A by A1,A2
,A3,A4,MATRIX_4:63
    .=0.(K,n,len A)*A by MATRIX_3:4;
  hence thesis by A5,A6,MATRIX_4:6;
end;

theorem Th15:
  for A,C being Matrix of K st len A=width C & len C>0 & len A>0
  holds (-C)*A = -(C*A)
proof
  let A,C be Matrix of K;
  assume that
A1: len A=width C and
A2: len C>0 and
A3: len A>0;
A4: len C=len (-C) by MATRIX_3:def 2;
A5: width (-C)=width C by MATRIX_3:def 2;
  then width ((-C)*A)=width A by A1,MATRIX_3:def 4;
  then
A6: width (C*A)=width ((-C)*A) by A1,MATRIX_3:def 4;
  reconsider D=C as Matrix of (len C),(width C),K by A2,MATRIX_1:20;
A7: width (-C)=width C by MATRIX_3:def 2;
  then
A8: len ((-C)*A)=len (-C) & width ((-C)*A)=width A by A1,MATRIX_3:def 4;
  len (-C)=len ((-C)*A) by A1,A5,MATRIX_3:def 4;
  then
A9: len (C*A)=len ((-C)*A) by A1,A4,MATRIX_3:def 4;
  len C = len (-C) by MATRIX_3:def 2;
  then C*A +((-C)*A) =(D+-D)*A by A1,A2,A3,A7,MATRIX_4:63
    .= 0.(K,len C,width C)*A by MATRIX_3:5
    .= 0.(K,len C,width A) by A1,A2,A3,Th14;
  hence thesis by A4,A8,A9,A6,MATRIX_4:8;
end;

theorem Th16:
  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
  let A,B,C be Matrix of K;
  assume
A1: len B=len C & width B=width C & len A=width B & len B>0 & len A>0;
A2: width (-C)=width C & len C=len (-C) by MATRIX_3:def 2;
  thus (B-C)*A=(B+-C)*A by MATRIX_4:def 1
    .=B*A +(-C)*A by A1,A2,MATRIX_4:63
    .=B*A +-(C*A) by A1,Th15
    .=B*A -(C*A) by MATRIX_4:def 1;
end;

theorem
  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:
  for m being Element of NAT,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
  let m be Element of NAT, A,C be Matrix of K;
  assume that
A1: width A>0 and
A2: len A >0;
A3: len (0.(K,width A,m))= width A by MATRIX_1:def 2;
  then m=width 0.(K,width A,m) by A1,MATRIX_1:20;
  then
A4: width (A*((0.(K,width A,m))))=m by A3,MATRIX_3:def 4;
  width (0.(K,width A,m))=m by A1,A3,MATRIX_1:20;
  then
A5: A*(0.(K,width A,m)) + A*(0.(K,width A,m)) =A*( 0.(K,width A,m)+ 0.(K,
  width A,m)) by A1,A2,A3,MATRIX_4:62
    .=A*(0.(K,width A,m)) by MATRIX_3:4;
  len (A*(0.(K,width A,m)))=len A by A3,MATRIX_3:def 4;
  hence thesis by A4,A5,MATRIX_4:6;
end;

theorem Th19:
  for A,C being Matrix of K st width A=len C & len A>0 & len C>0
  holds A*(-C) = -(A*C)
proof
  let A,C be Matrix of K;
  assume that
A1: width A=len C and
A2: len A>0 and
A3: len C>0;
A4: len C=len (-C) by MATRIX_3:def 2;
  then
A5: len A=len (A*(-C)) by A1,MATRIX_3:def 4;
  width (-C)=width C by MATRIX_3:def 2;
  then
A6: width (A*(-C))=width C by A1,A4,MATRIX_3:def 4;
  reconsider D=C as Matrix of (len C),(width C),K by A3,MATRIX_1:20;
A7: len (A*C)=len A & width (A*C)=width C by A1,MATRIX_3:def 4;
  len C = len (-C) & width (-C)=width C by MATRIX_3:def 2;
  then A*C +(A*(-C)) =A*(D+-D) by A1,A2,A3,MATRIX_4:62
    .= A*(0.(K,len C,width C)) by MATRIX_3:5
    .= 0.(K,len A,width C) by A1,A2,A3,Th18;
  hence thesis by A7,A5,A6,MATRIX_4:8;
end;

theorem Th20:
  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
  let A,B,C be Matrix of K;
  assume that
A1: len B=len C and
A2: width B=width C and
A3: len B=width A & len B>0 & len A>0;
A4: width (-C)=width C & len C=len (-C) by MATRIX_3:def 2;
  thus A*(B-C)=A*(B+-C) by MATRIX_4:def 1
    .=A*B +A*(-C) by A1,A2,A3,A4,MATRIX_4:62
    .=A*B +-(A*C) by A1,A3,Th19
    .=A*B -(A*C) by MATRIX_4:def 1;
end;

theorem
  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:
  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 Element of NAT st [i,j] in
  Indices A holds C*(i,j) = A*(i,j) - B*(i,j)) holds C=A-B
proof
  let A,B,C be Matrix of REAL;
  assume that
A1: len A=len B & width A=width B and
A2: len C =len A & width C=width A and
A3: for i,j being Element of NAT st [i,j] in Indices A holds C*(i,j) = A
  *(i,j) - B*(i,j);
A4: Indices B=Indices A by A1,MATRIX_4:55;
  for i,j being Nat st [i,j] in Indices A holds C*(i,j) = A*(i,j) +((-B)*(
  i,j))
  proof
    let i,j be Nat;
    reconsider i0=i,j0=j as Element of NAT by ORDINAL1:def 12;
    assume
A5: [i,j] in Indices A;
    hence C*(i,j) = A*(i0,j0) - B*(i0,j0) by A3
      .=A*(i0,j0) +-B*(i0,j0)
      .=A*(i,j)+(-B)*(i,j) by A4,A5,Th10;
  end;
  then C=(A+-B) by A2,MATRIXR1:26;
  hence thesis by MATRIX_4:def 1;
end;

theorem Th23:
  for x1,x2 being FinSequence of REAL st len x1=len x2 holds
  LineVec2Mx (x1-x2)=LineVec2Mx (x1)-LineVec2Mx (x2)
proof
  let x1,x2 be FinSequence of REAL;
A1: width LineVec2Mx x1=len x1 & len LineVec2Mx x1=1 by MATRIXR1:def 10;
A2: Seg width LineVec2Mx x1=Seg len x1 by MATRIXR1:def 10
    .= dom x1 by FINSEQ_1:def 3;
A3: dom LineVec2Mx x1=Seg len LineVec2Mx x1 by FINSEQ_1:def 3
    .=Seg 1 by MATRIXR1:def 10;
  assume
A4: len x1=len x2;
  then
A5: dom x1 = dom x2 by FINSEQ_3:29;
A6: width LineVec2Mx x2=len x2 & len LineVec2Mx x2=1 by MATRIXR1:def 10;
  then
A7: Indices LineVec2Mx x2=Indices LineVec2Mx x1 by A4,A1,MATRIX_4:55;
A8: len (x1-x2)=len x1 by A4,RVSUM_1:116;
  then
A9: dom (x1-x2)=dom x1 by FINSEQ_3:29;
A10: width LineVec2Mx (x1-x2)=len (x1-x2) & len LineVec2Mx (x1-x2)=1 by
MATRIXR1:def 10;
  then
A11: Indices LineVec2Mx (x1-x2)=Indices LineVec2Mx x1 by A4,A1,MATRIX_4:55
,RVSUM_1:116;
  for i,j holds [i,j] in Indices LineVec2Mx x1 implies (LineVec2Mx (x1-x2
  ))*(i,j) = (LineVec2Mx x1)*(i,j) - (LineVec2Mx x2)*(i,j)
  proof
    let i,j;
    assume
A12: [i,j] in Indices LineVec2Mx x1;
    then consider q1 being FinSequence of REAL such that
    q1 = (LineVec2Mx x1).i and
A13: (LineVec2Mx x1)*(i,j) = q1.j by MATRIX_1:def 5;
    i in Seg 1 by A3,A12,ZFMISC_1:87;
    then 1<=i & i<=1 by FINSEQ_1:1;
    then
A14: i=1 by XXREAL_0:1;
A15: j in dom x1 by A2,A12,ZFMISC_1:87;
    then
A16: q1.j=x1.j by A14,A13,MATRIXR1:def 10;
    consider p being FinSequence of REAL such that
    p = (LineVec2Mx (x1-x2)).i and
A17: (LineVec2Mx (x1-x2))*(i,j) = p.j by A11,A12,MATRIX_1:def 5;
    consider q2 being FinSequence of REAL such that
    q2 = (LineVec2Mx x2).i and
A18: (LineVec2Mx x2)*(i,j) =q2.j by A7,A12,MATRIX_1:def 5;
A19: q2.j=x2.j by A5,A15,A14,A18,MATRIXR1:def 10;
    p.j=(x1-x2).j by A9,A15,A14,A17,MATRIXR1:def 10;
    hence thesis by A4,A17,A13,A16,A18,A19,Lm1;
  end;
  hence thesis by A4,A8,A10,A1,A6,Th22;
end;

theorem Th24:
  for x1,x2 being FinSequence of REAL st len x1=len x2 & len x1>0
  holds ColVec2Mx (x1-x2)=ColVec2Mx (x1)-ColVec2Mx (x2)
proof
  let x1,x2 be FinSequence of REAL;
  assume that
A1: len x1=len x2 and
A2: len x1>0;
A3: width ColVec2Mx x1=1 by A2,MATRIXR1:def 9;
A4: Seg width ColVec2Mx x1=Seg 1 by A2,MATRIXR1:def 9;
A5: dom x1=dom x2 by A1,FINSEQ_3:29;
A6: len (x1-x2)=len x1 by A1,RVSUM_1:116;
  then
A7: dom (x1-x2)=dom x1 by FINSEQ_3:29;
A8: len ColVec2Mx x1=len x1 by A2,MATRIXR1:def 9;
  then
A9: dom ColVec2Mx x1=dom x1 by FINSEQ_3:29;
A10: len ColVec2Mx x2=len x2 & width ColVec2Mx x2=1 by A1,A2,MATRIXR1:def 9;
  then
A11: Indices ColVec2Mx x2=Indices ColVec2Mx x1 by A1,A8,A3,MATRIX_4:55;
A12: len ColVec2Mx (x1-x2)=len (x1-x2) & width ColVec2Mx (x1-x2)=1 by A2,A6,
MATRIXR1:def 9;
  then
A13: Indices ColVec2Mx (x1-x2)=Indices ColVec2Mx x1 by A1,A8,A3,MATRIX_4:55
,RVSUM_1:116;
  for i,j st [i,j] in Indices ColVec2Mx x1 holds (ColVec2Mx (x1-x2))*(i,j
  ) = (ColVec2Mx x1)*(i,j) - (ColVec2Mx x2)*(i,j)
  proof
    let i,j;
    assume
A14: [i,j] in Indices ColVec2Mx x1;
    then consider q1 being FinSequence of REAL such that
A15: q1 = (ColVec2Mx x1).i and
A16: (ColVec2Mx x1)*(i,j)=q1.j by MATRIX_1:def 5;
    j in Seg 1 by A4,A14,ZFMISC_1:87;
    then 1<=j & j<=1 by FINSEQ_1:1;
    then
A17: j=1 by XXREAL_0:1;
A18: i in dom x1 by A9,A14,ZFMISC_1:87;
    then (ColVec2Mx x1).i=<* x1.i *> by A2,MATRIXR1:def 9;
    then
A19: q1.j=x1.i by A17,A15,FINSEQ_1:40;
    consider p being FinSequence of REAL such that
A20: p = (ColVec2Mx (x1-x2)).i and
A21: (ColVec2Mx (x1-x2))*(i,j) = p.j by A13,A14,MATRIX_1:def 5;
    consider q2 being FinSequence of REAL such that
A22: q2 = (ColVec2Mx x2).i and
A23: (ColVec2Mx x2)*(i,j)=q2.j by A11,A14,MATRIX_1:def 5;
    (ColVec2Mx x2).i=<* x2.i *> by A1,A2,A5,A18,MATRIXR1:def 9;
    then
A24: q2.j=x2.i by A17,A22,FINSEQ_1:40;
    (ColVec2Mx (x1-x2)).i=<* (x1-x2).i *> by A2,A6,A7,A18,MATRIXR1:def 9;
    then p.j=(x1-x2).i by A17,A20,FINSEQ_1:40;
    hence thesis by A1,A21,A16,A19,A23,A24,Lm1;
  end;
  hence thesis by A1,A6,A8,A12,A3,A10,Th22;
end;

theorem Th25:
  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
  let A,B be Matrix of REAL;
  assume that
A1: len A=len B and
A2: width A=width B;
A3: width (A-B)=width A by A1,A2,Th6;
  let i be Nat;
A4: len Line(A,i)=width A by MATRIX_1:def 7;
A5: len Line(B,i)=width B by MATRIX_1:def 7;
  assume 1<=i & i<=len A;
  then
A6: i in dom A by FINSEQ_3:25;
A7: for j being Nat st j in Seg width (A-B) holds (Line(A,i)-Line(B,i)).j =
  (A-B)*(i,j)
  proof
    reconsider i2=i as Element of NAT by ORDINAL1:def 12;
    let j be Nat;
    reconsider j2=j as Element of NAT by ORDINAL1:def 12;
A8: (Line(A,i2)-Line(B,i2)).j=Line(A,i2).j2-Line(B,i2).j2 by A2,A4,A5,Lm1;
    assume
A9: j in Seg width (A-B);
    then [i,j] in Indices A by A6,A3,ZFMISC_1:87;
    then
A10: (A-B)*(i2,j2) = A*(i2,j2) - B*(i2,j2) by A1,A2,Th6;
A11: j in Seg width A by A1,A2,A9,Th6;
    then Line(A,i).j=A*(i,j) by MATRIX_1:def 7;
    hence thesis by A2,A11,A10,A8,MATRIX_1:def 7;
  end;
  len (Line(A,i)-Line(B,i))=len Line(A,i) by A2,A4,A5,RVSUM_1:116;
  hence thesis by A4,A3,A7,MATRIX_1:def 7;
end;

theorem Th26:
  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
  let A,B be Matrix of REAL;
  assume that
A1: len A=len B and
A2: width A=width B;
A3: len (A-B)=len A by A1,A2,Th6;
  let i be Nat;
A4: len Col(A,i)=len A by MATRIX_1:def 8;
  assume 1<=i & i<=width A;
  then
A5: i in Seg width A by FINSEQ_1:1;
A6: len Col(B,i)=len B by MATRIX_1:def 8;
A7: dom A=dom B by A1,FINSEQ_3:29;
A8: for j being Nat st j in dom (A-B) holds (Col(A,i)-Col(B,i)).j = (A-B)*(
  j,i)
  proof
    let j be Nat;
    assume j in dom (A-B);
    then j in Seg len (A-B) by FINSEQ_1:def 3;
    then
A9: j in dom A by A3,FINSEQ_1:def 3;
    then
A10: [j,i] in Indices A by A5,ZFMISC_1:87;
    reconsider j as Element of NAT by ORDINAL1:def 12;
    Col(A,i).j=A*(j,i) & Col(B,i).j=B*(j,i) by A7,A9,MATRIX_1:def 8;
    then Col(A,i).j-Col(B,i).j=(A-B)*(j,i) by A1,A2,A5,A10,Th6;
    hence thesis by A1,A4,A6,Lm1;
  end;
  len (Col(A,i)-Col(B,i))=len (Col(A,i)) by A1,A4,A6,RVSUM_1:116;
  hence thesis by A4,A3,A8,MATRIX_1:def 8;
end;

theorem
  for A being Matrix of n,k,REAL, B being Matrix of k,m,REAL,C being
  Matrix of m,l,REAL st n>0 & k>0 & m>0 holds A*B*C=A*(B*C)
proof
  let A be Matrix of n,k,REAL, B be Matrix of k,m,REAL,C be Matrix of m,l,REAL;
  assume that
A1: n>0 and
A2: k>0 and
A3: m>0;
A4: width B=m & len C=m by A2,A3,MATRIX_1:23;
  width A=k & len B=k by A1,A2,MATRIX_1:23;
  hence thesis by A4,MATRIX_3:33;
end;

theorem Th28:
  for A,B,C being Matrix of n,REAL holds A*B*C=A*(B*C)
proof
  let A,B,C be Matrix of n,REAL;
A1: width B=n & len C=n by MATRIX_1:24;
  width A=n & len B=n by MATRIX_1:24;
  hence thesis by A1,MATRIX_3:33;
end;

theorem Th29:
  for A being Matrix of n,D holds (A@)@=A
proof
  let A be Matrix of n,D;
  reconsider N=A@ as Matrix of n,D;
A1: len A=n & width A=n by MATRIX_1:24;
A2: Indices (N@)=[:Seg n,Seg n :] by MATRIX_1:24
    .=Indices A by MATRIX_1:24;
A3: for i,j being Nat st [i,j] in Indices (N@) holds (N@)*(i,j) = A*(i,j)
  proof
    let i,j be Nat;
    assume
A4: [i,j] in Indices (N@);
    then [j,i] in Indices N by MATRIX_1:def 6;
    then (N@)*(i,j)=N*(j,i) by MATRIX_1:def 6;
    hence thesis by A2,A4,MATRIX_1:def 6;
  end;
  len (N@)=n & width (N@)=n by MATRIX_1:24;
  hence thesis by A1,A3,MATRIX_1:21;
end;

theorem Th30:
  for A,B being Matrix of n,REAL holds (A*B)@ = (B@)*(A@)
proof
  let A,B be Matrix of n,REAL;
A1: len A=n by MATRIX_1:24;
A2: width A=n & len B=n by MATRIX_1:24;
A3: len (A*B)=n by MATRIX_1:24;
A4: width B=n by MATRIX_1:24;
A5: len (B@)=n by MATRIX_1:24;
  then
A6: len ((B@)*(A@))=len (B@) by MATRIX_1:24;
A7: width (B@)=n by MATRIX_1:24
    .=len (A@) by MATRIX_1:24;
A8: width (A*B)=n by MATRIX_1:24;
A9: width (A@)=n by MATRIX_1:24;
  then
A10: width ((B@)*(A@))=width (A@) by MATRIX_1:24;
A11: now
    let i,j be Nat;
A12: Indices ((A*B)@)=[:Seg n,Seg n :] by MATRIX_1:24;
    assume
A13: [i,j] in Indices ((A*B)@);
    then j in Seg len (A*B) by A3,A12,ZFMISC_1:87;
    then
A14: j in dom (A*B) by FINSEQ_1:def 3;
    i in Seg width (A*B) by A8,A13,A12,ZFMISC_1:87;
    then
A15: [j,i]in Indices (A*B) by A14,ZFMISC_1:87;
    Seg width (A@) = dom A by A1,A9,FINSEQ_1:def 3;
    then j in dom A by A9,A13,A12,ZFMISC_1:87;
    then
A16: Col(A@,j)=Line(A,j) by MATRIX_2:14;
    reconsider i0=i,j0=j as Element of NAT by ORDINAL1:def 12;
A17: Seg width B = dom (B@) by A4,A5,FINSEQ_1:def 3;
A18: Indices ((B@)*(A@))=[:Seg n,Seg n :] by MATRIX_1:24;
    then [i,j] in [:dom (B@),Seg width (A@):] by A6,A10,A13,A12,FINSEQ_3:29;
    then i in Seg width B by A17,ZFMISC_1:87;
    then Line(B@,i)=Col(B,i) by MATRIX_2:15;
    hence ((B@)*(A@))*(i,j)= Col(B,i0) "*" Line(A,j0) by A7,A13,A12,A18,A16,
MATRPROB:39
      .=(A*B)*(j0,i0) by A2,A15,MATRPROB:39
      .=((A*B)@)*(i,j) by A15,MATRIX_1:def 6;
  end;
A19: len ((B@)*(A@))=n & width ((B@)*(A@))=n by MATRIX_1:24;
  len ((A*B)@)=n & width ((A*B)@)=n by MATRIX_1:24;
  hence thesis by A19,A11,MATRIX_1:21;
end;

theorem Th31:
  for A being Matrix of REAL st len A=n & width A=m holds -A+A= 0_Rmatrix(n,m)
proof
  let A be Matrix of REAL;
  assume
A1: len A=n & width A=m;
  len (-(MXR2MXF A)) =len A & width (-(MXR2MXF A)) = width A by MATRIX_3:def 2;
  hence -A+A = MXF2MXR ((MXR2MXF A)+(-(MXR2MXF A))) by MATRIX_3:2
    .=0_Rmatrix(n,m) by A1,MATRIX_4:2;
end;

begin :: Determinants

definition
  let n;
  let A be Matrix of n,REAL;
  redefine func MXR2MXF A -> Matrix of n,F_Real;
  coherence;
end;

definition
  let n;
  let A be Matrix of n,REAL;
  func Det A -> Real equals
  Det MXR2MXF A;
  coherence;
end;

theorem
  for A being Matrix of 2,REAL holds Det A = (A*(1,1))*(A*(2,2))-(A*(1,2
  ))*(A*(2,1))
proof
  let A be Matrix of 2,REAL;
  reconsider N=MXR2MXF A as Matrix of 2,F_Real;
  Det A = (N*(1,1))*(N*(2,2))-(N*(1,2))*(N*(2,1)) by MATRIX_7:12;
  hence thesis;
end;

theorem Th33:
  for s1,s2,s3 be FinSequence st len s1 = n & len s2 = n & len s3
  = n holds <*s1,s2,s3*> is tabular
proof
  let s1,s2,s3 be FinSequence;
  assume
A1: len s1 = n & len s2 = n & len s3 = n;
  now
    take n;
    let x;
    assume x in rng (<*s1,s2,s3*>);
    then
A2: x in { s1,s2,s3} by FINSEQ_2:128;
    then reconsider r=x as FinSequence by ENUMSET1:def 1;
    take r;
    thus x= r & len r=n by A1,A2,ENUMSET1:def 1;
  end;
  hence thesis by MATRIX_1:def 1;
end;

theorem Th34:
  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
  let p1,p2,p3 be FinSequence of D;
  reconsider q1 = p1,q2 = p2,q3=p3 as Element of D* by FINSEQ_1:def 11;
  reconsider M = <*q1,q2,q3*> as FinSequence of D*;
  assume
A1: len p1 =n & len p2 =n & len p3 =n;
  then reconsider M as Matrix of D by Th33;
  M is Matrix of 3,n,D
  proof
    thus len M = 3 by FINSEQ_1:45;
    let r be FinSequence of D;
    assume r in rng M;
    then r in { p1,p2,p3 } by FINSEQ_2:128;
    hence thesis by A1,ENUMSET1:def 1;
  end;
  hence thesis;
end;

theorem Th35:
  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
  let a1,a2,a3,b1,b2,b3,c1,c2,c3 be Element of D;
A1: len <*c1,c2,c3*>=3 by FINSEQ_1:45;
  len <*a1,a2,a3*>=3 & len <*b1,b2,b3*>=3 by FINSEQ_1:45;
  hence thesis by A1,Th34;
end;

theorem Th36:
  for A being Matrix of n,D for p being FinSequence of D, i being
  Nat st p=A.i & i in Seg n holds len p=n
proof
  let A be Matrix of n,D;
  let p be FinSequence of D, i be Nat;
  assume that
A1: p=A.i and
A2: i in Seg n;
  consider n2 being Nat such that
A3: for x being set st x in rng A ex s being FinSequence of D st s=x &
  len s = n2 by MATRIX_1:9;
  len A=n by MATRIX_1:24;
  then
A4: i in dom A by A2,FINSEQ_1:def 3;
  then A.i in rng A by FUNCT_1:def 3;
  then consider s being FinSequence of D such that
A5: s=A.i and
  len s = n2 by A3;
  s in rng A by A4,A5,FUNCT_1:def 3;
  hence thesis by A1,A5,MATRIX_1:def 2;
end;

theorem Th37:
  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
  let A be Matrix of 3,D;
  reconsider B=<* <* 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) *> *> as Matrix of 3,D by Th35;
A1: len A=3 & width A=3 by MATRIX_1:24;
A2: for i,j being Nat st [i,j] in Indices A holds A*(i,j) = B*(i,j)
  proof
    let i,j be Nat;
A3: Indices B=[: Seg 3,Seg 3 :] by MATRIX_1:24;
A4: Indices A=[: Seg 3,Seg 3 :] by MATRIX_1:24;
    assume
A5: [i,j] in Indices A;
    then
A6: i in Seg 3 by A4,ZFMISC_1:87;
    2 in Seg 3;
    then
A7: [i,2] in Indices A by A4,A6,ZFMISC_1:87;
    1 in Seg 3;
    then
A8: [i,1] in Indices A by A4,A6,ZFMISC_1:87;
    3 in Seg 3;
    then
A9: [i,3] in Indices A by A4,A6,ZFMISC_1:87;
A10: i in {1,2,3} by A5,A4,FINSEQ_3:1,ZFMISC_1:87;
    now
      per cases by A10,ENUMSET1:def 1;
      case
A11:    i=1;
        reconsider p0=<* A*(1,1),A*(1,2), A*(1,3) *> as FinSequence of D;
A12:    len p0=3 by FINSEQ_1:45;
A13:    ex p23 being FinSequence of D st p23 = A.i & A*(i,3) = p23.3 by A9,
MATRIX_1:def 5;
        consider p2 being FinSequence of D such that
A14:    p2 = A.i and
A15:    A*(i,1) = p2.1 by A8,MATRIX_1:def 5;
A16:    ex p22 being FinSequence of D st p22 = A.i & A*(i,2) = p22.2 by A7,
MATRIX_1:def 5;
A17:    for k be Nat st 1 <=k & k <= len p0 holds p0.k=p2.k
        proof
          let k be Nat;
          assume
A18:      1 <=k & k <= len p0;
          k in NAT by ORDINAL1:def 12;
          then
A19:      k in Seg 3 by A12,A18;
          per cases by A19,ENUMSET1:def 1,FINSEQ_3:1;
          suppose
            k=1;
            hence thesis by A11,A15,FINSEQ_1:45;
          end;
          suppose
            k=2;
            hence thesis by A11,A14,A16,FINSEQ_1:45;
          end;
          suppose
            k=3;
            hence thesis by A11,A14,A13,FINSEQ_1:45;
          end;
        end;
        ex p being FinSequence of D st p = B.i & B*(i,j) = p.j by A5,A3,A4,
MATRIX_1:def 5;
        then
A20:    B*(i,j)=p0.j by A11,FINSEQ_1:45;
        len p2=3 by A6,A14,Th36;
        hence
        ex p being FinSequence of D st p = A.i & B*(i,j) = p.j by A12,A14,A17
,A20,FINSEQ_1:14;
      end;
      case
A21:    i=2;
        reconsider p0=<* A*(2,1),A*(2,2), A*(2,3) *> as FinSequence of D;
A22:    len p0=3 by FINSEQ_1:45;
A23:    ex p23 being FinSequence of D st p23 = A.i & A*(i,3) = p23.3 by A9,
MATRIX_1:def 5;
        consider p2 being FinSequence of D such that
A24:    p2 = A.i and
A25:    A*(i,1) = p2.1 by A8,MATRIX_1:def 5;
A26:    ex p22 being FinSequence of D st p22 = A.i & A*(i,2) = p22.2 by A7,
MATRIX_1:def 5;
A27:    for k be Nat st 1 <=k & k <= len p0 holds p0.k=p2.k
        proof
          let k be Nat;
          assume
A28:      1 <=k & k <= len p0;
          k in NAT by ORDINAL1:def 12;
          then
A29:      k in {1,2,3} by A22,A28,FINSEQ_3:1;
          per cases by A29,ENUMSET1:def 1;
          suppose
            k=1;
            hence thesis by A21,A25,FINSEQ_1:45;
          end;
          suppose
            k=2;
            hence thesis by A21,A24,A26,FINSEQ_1:45;
          end;
          suppose
            k=3;
            hence thesis by A21,A24,A23,FINSEQ_1:45;
          end;
        end;
        ex p being FinSequence of D st p = B.i & B*(i,j) = p.j by A5,A3,A4,
MATRIX_1:def 5;
        then
A30:    B*(i,j)=p0.j by A21,FINSEQ_1:45;
        len p2=3 by A6,A24,Th36;
        hence
        ex p being FinSequence of D st p = A.i & B*(i,j) = p.j by A22,A24,A27
,A30,FINSEQ_1:14;
      end;
      case
A31:    i=3;
        reconsider p0=<* A*(3,1),A*(3,2), A*(3,3) *> as FinSequence of D;
A32:    len p0=3 by FINSEQ_1:45;
A33:    ex p23 being FinSequence of D st p23 = A.i & A*(i,3) = p23.3 by A9,
MATRIX_1:def 5;
        consider p2 being FinSequence of D such that
A34:    p2 = A.i and
A35:    A*(i,1) = p2.1 by A8,MATRIX_1:def 5;
A36:    ex p22 being FinSequence of D st p22 = A.i & A*(i,2) = p22.2 by A7,
MATRIX_1:def 5;
A37:    for k be Nat st 1 <=k & k <= len p0 holds p0.k=p2.k
        proof
          let k be Nat;
          assume
A38:      1 <=k & k <= len p0;
          k in NAT by ORDINAL1:def 12;
          then
A39:      k in {1,2,3} by A32,A38,FINSEQ_3:1;
          per cases by A39,ENUMSET1:def 1;
          suppose
            k=1;
            hence thesis by A31,A35,FINSEQ_1:45;
          end;
          suppose
            k=2;
            hence thesis by A31,A34,A36,FINSEQ_1:45;
          end;
          suppose
            k=3;
            hence thesis by A31,A34,A33,FINSEQ_1:45;
          end;
        end;
        ex p being FinSequence of D st p = B.i & B*(i,j) = p.j by A5,A3,A4,
MATRIX_1:def 5;
        then
A40:    B*(i,j)=p0.j by A31,FINSEQ_1:45;
        len p2=3 by A6,A34,Th36;
        hence
        ex p being FinSequence of D st p = A.i & B*(i,j) = p.j by A32,A34,A37
,A40,FINSEQ_1:14;
      end;
    end;
    hence thesis by A5,MATRIX_1:def 5;
  end;
  len B=3 & width B=3 by MATRIX_1:24;
  hence thesis by A1,A2,MATRIX_1:21;
end;

theorem
  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
  let A be Matrix of 3,REAL;
  reconsider N=MXR2MXF A as Matrix of 3,F_Real;
  reconsider N2=<* <* N*(1,1),N*(1,2), N*(1,3) *>, <* N*(2,1),N*(2,2), N*(2,3)
  *>, <* N*(3,1),N*(3,2), N*(3,3) *> *> as Matrix of 3,F_Real by Th35;
  Det A = Det N2 by Th37
    .= (N*(1,1))*(N*(2,2))*(N*(3,3))-(N*(1,3))*(N*(2,2))*(N*(3,1)) -(N*(1,1)
)*(N*(2,3))*(N*(3,2))+(N*(1,2))*(N*(2,3))*(N*(3,1)) -(N*(1,2))*(N*(2,1))*(N*(3,
  3))+(N*(1,3))*(N*(2,1))*(N*(3,2)) by MATRIX_9:46;
  hence thesis;
end;

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

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

theorem Th40:
  Permutations 0 = {<*>NAT}
proof
  now
    let p be set;
    assume p in Permutations(0);
    then reconsider q=p as Permutation of Seg 0 by MATRIX_2:def 9;
    q=<*>NAT;
    hence p in {<*>NAT} by TARSKI:def 1;
  end;
  then
A1: Permutations(0) c={<*>NAT} by TARSKI:def 3;
  {<*>NAT} c=Permutations(0)
  proof
    let x be set;
    assume x in {<*>NAT};
    then x is Permutation of Seg 0 by Lm4,TARSKI:def 1;
    hence thesis by MATRIX_2:def 9;
  end;
  hence thesis by A1,XBOOLE_0:def 10;
end;

theorem Th41:
  for A being Matrix of 0,K holds Det A = 1.K
proof
  reconsider kk=idseq 0 as Element of Permutations(0) by Th40,TARSKI:def 1;
  let A be Matrix of 0,K;
A1: (Path_product A).(idseq 0)=1.K
  proof
    reconsider p = idseq 0 as Element of Permutations(0) by Lm4,MATRIX_2:def 9
;
A2: -(1_K,p)=1_K
    proof
      reconsider q = id Seg 0 as Element of Permutations(0) by Lm4,
MATRIX_2:def 9;
      len Permutations 0 = 0 by MATRIX_2:18;
      then q is even by MATRIX_2:25;
      hence thesis by MATRIX_2:def 13;
    end;
    1_K is_a_unity_wrt (the multF of K) by GROUP_1:21;
    then len Path_matrix(p,A) = 0 & (the multF of K) is having_a_unity by
MATRIX_3:def 7,SETWISEO:def 2;
    then
    (the multF of K) $$ Path_matrix(p,A) = the_unity_wrt (the multF of K)
    by FINSOP_1:def 1
      .= 1_K by GROUP_1:22;
    hence thesis by A2,MATRIX_3:def 8;
  end;
A3: FinOmega (Permutations(0)) = Permutations(0) by Th40,MATRIX_2:def 14
    .= {. kk .} by Th40;
  Det A=(the addF of K) $$ (FinOmega(Permutations(0)),Path_product(A)) by
MATRIX_3:def 9
    .=1.K by A1,A3,SETWISEO:17;
  hence thesis;
end;

theorem
  for A being Matrix of 0,REAL holds Det A = 1
proof
  let A be Matrix of 0,REAL;
  thus Det A = 1.F_Real by Th41
    .=1;
end;

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

theorem Th43:
  for n being Nat, A being Matrix of n,K holds Det A = Det (A@)
proof
  let n be Nat, A be Matrix of n,K;
  n=0 or n>=1 & n is Element of NAT by NAT_1:14,ORDINAL1:def 12;
  then Det A=1_K & Det A@=1_K or Det A = Det A@ by Th41,MATRIX_7:37;
  hence thesis;
end;

theorem
  for A being Matrix of n,REAL holds Det A = Det (A@)
proof
  let A be Matrix of n,REAL;
  reconsider N1=MXR2MXF A, N2=MXR2MXF (A@) as Matrix of n,F_Real;
  reconsider N3=MXF2MXR (N1@) as Matrix of n,REAL;
  reconsider N4=MXR2MXF N3 as Matrix of n,F_Real;
  thus thesis by Th43;
end;

:: Removing condition n>0 from MATRIX11:62

theorem Th45:
  for A,B being Matrix of n,K holds Det(A*B) = (Det A)*(Det B)
proof
  let A,B be Matrix of n,K;
  per cases;
  suppose
    n>0;
    hence thesis by MATRIX11:62;
  end;
  suppose
    n<=0;
    then
A1: n=0;
    hence Det(A*B) = 1.K by Th41
      .=1.K * 1.K by VECTSP_1:def 6
      .=(Det A)*1.K by A1,Th41
      .=(Det A)*(Det B) by A1,Th41;
  end;
end;

theorem Th46:
  for A,B being Matrix of n,REAL holds Det (A*B) = (Det A)*(Det B)
proof
  set K=F_Real;
  let A,B be Matrix of n,REAL;
  reconsider Na=MXR2MXF A, Nb=MXR2MXF B as Matrix of n,K;
  Det (A*B) = (Det Na) * (Det Nb) by Th45
    .= (Det A)*(Det B);
  hence thesis;
end;

begin :: Matrix as Operator

theorem
  for x,y being FinSequence of REAL, 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
  let x,y be FinSequence of REAL,A be Matrix of REAL;
  assume that
A1: len x=len A and
A2: len y=len x and
A3: len x>0;
A4: width LineVec2Mx y=len y by MATRIXR1:def 10;
A5: width LineVec2Mx x=len x by MATRIXR1:def 10;
  then
A6: width ((LineVec2Mx x)*A)=width A by A1,MATRIX_3:def 4
    .=width ((LineVec2Mx y)*A) by A1,A2,A4,MATRIX_3:def 4;
A7: len LineVec2Mx y=1 by MATRIXR1:def 10;
A8: len LineVec2Mx x=1 by MATRIXR1:def 10;
  then
A9: 1<=len((LineVec2Mx x)*A) by A1,A5,MATRIX_3:def 4;
A10: len ((LineVec2Mx x)*A)=len LineVec2Mx x by A1,A5,MATRIX_3:def 4
    .=len LineVec2Mx y by A7,MATRIXR1:def 10
    .=len((LineVec2Mx y)*A) by A1,A2,A4,MATRIX_3:def 4;
  thus (x-y)*A=Line(((LineVec2Mx x)-(LineVec2Mx y))*A,1) by A2,Th23
    .=Line((LineVec2Mx x)*A-(LineVec2Mx y)*A,1) by A1,A2,A3,A5,A4,A8,A7,Th16
    .=x*A - y*A by A6,A10,A9,Th25;
end;

theorem
  for x,y being FinSequence of REAL,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
  let x,y be FinSequence of REAL, A be Matrix of REAL;
  assume that
A1: len x=width A and
A2: len y=len x and
A3: len x >0 and
A4: len A >0;
A5: len ColVec2Mx y=len y by A2,A3,MATRIXR1:def 9;
A6: width ColVec2Mx y=1 by A2,A3,MATRIXR1:def 9;
A7: len ColVec2Mx x=len x by A3,MATRIXR1:def 9;
  then
A8: len (A*(ColVec2Mx x))=len A by A1,MATRIX_3:def 4
    .=len (A*(ColVec2Mx y)) by A1,A2,A5,MATRIX_3:def 4;
A9: width ColVec2Mx x=1 by A3,MATRIXR1:def 9;
  then
A10: 1<=width(A*(ColVec2Mx x)) by A1,A7,MATRIX_3:def 4;
A11: width (A*(ColVec2Mx x))=width (ColVec2Mx (x)) by A1,A7,MATRIX_3:def 4
    .=width (ColVec2Mx y) by A3,A6,MATRIXR1:def 9
    .=width(A*(ColVec2Mx y)) by A1,A2,A5,MATRIX_3:def 4;
  thus A*(x-y)=Col(A*((ColVec2Mx x)-(ColVec2Mx y)),1) by A2,A3,Th24
    .=Col(A*(ColVec2Mx x)-A*(ColVec2Mx y),1) by A1,A2,A3,A4,A7,A5,A9,A6,Th20
    .=A*x - A*y by A8,A11,A10,Th26;
end;

theorem
  for x being FinSequence of REAL, A being Matrix of REAL st len A=len x
  & len x>0 & width A>0 holds (-x)*A=-(x*A)
proof
  let x be FinSequence of REAL,A be Matrix of REAL;
  assume that
A1: len A=len x and
A2: len x>0 and
A3: width A>0;
A4: (A@)*x=x*A by A1,A2,A3,MATRIXR1:52;
A5: width (A@)=len x by A1,A3,MATRIX_2:10;
  then
A6: (A@)*(-x)=(-1)*((A@)*x) by A2,MATRIXR1:59;
A7: len (-x)=len x by RVSUM_1:114;
  len (A@)>0 by A3,MATRIX_2:10;
  then (-x)*((A@)@)=(A@)*(-x) by A2,A5,A7,MATRIXR1:53;
  hence thesis by A1,A2,A3,A6,A4,MATRIX_2:13;
end;

theorem
  for x being FinSequence of REAL,A being Matrix of REAL st len x=width
  A & len x > 0 holds A*(-x)=-(A*x)
proof
  let x be FinSequence of REAL,A be Matrix of REAL;
  assume that
A1: len x=width A and
A2: len x > 0;
A3: len ColVec2Mx x=len x by A2,MATRIXR1:def 9;
  width ColVec2Mx x=1 by A2,MATRIXR1:def 9;
  then
A4: 1<=width(A*(ColVec2Mx x)) by A1,A3,MATRIX_3:def 4;
  thus A*(-x) =Col(A*((-1)*ColVec2Mx x),1) by A2,MATRIXR1:47
    .=Col((-1)*(A*(ColVec2Mx x)),1) by A1,A3,MATRIXR1:40
    .=-(A*x) by A4,MATRIXR1:56;
end;

theorem
  for x being FinSequence of REAL,A being Matrix of REAL st len x=len A
  & len x>0 holds x*(-A)=-(x*A)
proof
  let x be FinSequence of REAL,A be Matrix of REAL;
  assume that
A1: len x=len A and
A2: len x>0;
A3: width A=len (x*A) by A1,MATRIXR1:62;
A4: len A=len (-A) & width A=width (-A) by MATRIX_3:def 2;
  then
A5: len (x*(-A))=width A by A1,MATRIXR1:62;
  x*(-A)+(x*A)=x*(-A+A) by A1,A2,A4,MATRIXR1:64
    .=x*(0_Rmatrix(len A,width A)) by Th31
    .=0*(width A) by A1,A2,MATRIXR1:66;
  hence thesis by A5,A3,Th1;
end;

theorem
  for x being FinSequence of REAL,A being Matrix of REAL st len x=width
  A & len A>0 & len x> 0 holds (-A)*x=-(A*x)
proof
  let x be FinSequence of REAL,A be Matrix of REAL;
  assume that
A1: len x=width A and
A2: len A>0 and
A3: len x> 0;
A4: len ColVec2Mx x=len x & width ColVec2Mx x=1 by A3,MATRIXR1:def 9;
  then
A5: 1<=width(A*(ColVec2Mx x)) by A1,MATRIX_3:def 4;
  thus (-A)*x =Col(((-1)*A*(ColVec2Mx x)),1) by Th9
    .=Col((-1)*(A*(ColVec2Mx x)),1) by A1,A2,A3,A4,MATRIXR1:41
    .=-(A*x) by A5,MATRIXR1:56;
end;

theorem
  for a being Real,x being FinSequence of REAL,A being Matrix of REAL st
  width A=len x & len x>0 holds A*(a*x)=a*(A*x)
proof
  let a be Real,x be FinSequence of REAL,A be Matrix of REAL;
  assume that
A1: width A=len x and
A2: len x>0;
A3: len ColVec2Mx x=len x by A2,MATRIXR1:def 9;
  width ColVec2Mx x=1 by A2,MATRIXR1:def 9;
  then
A4: 1<=width(A*(ColVec2Mx x)) by A1,A3,MATRIX_3:def 4;
  thus A*(a*x)=Col(A*(a*ColVec2Mx x),1) by A2,MATRIXR1:47
    .=Col(a*(A*(ColVec2Mx x)),1) by A1,A3,MATRIXR1:40
    .=a*(A*x) by A4,MATRIXR1:56;
end;

theorem
  for x being FinSequence of REAL, 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
  let x be FinSequence of REAL,A,B be Matrix of REAL;
  assume that
A1: len x=len A and
A2: len A=len B and
A3: width A=width B and
A4: len A >0;
A5: width LineVec2Mx x=len x by MATRIXR1:def 10;
  then
A6: len ((LineVec2Mx x)*A)=len LineVec2Mx x by A1,MATRIX_3:def 4
    .=1 by MATRIXR1:def 10;
A7: len ((LineVec2Mx x)*A)= len LineVec2Mx x by A1,A5,MATRIX_3:def 4
    .= len ((LineVec2Mx x)*B) by A1,A2,A5,MATRIX_3:def 4;
A8: width ((LineVec2Mx x)*A)=width A by A1,A5,MATRIX_3:def 4
    .=width ((LineVec2Mx x)*B) by A1,A2,A3,A5,MATRIX_3:def 4;
  len LineVec2Mx x=1 by MATRIXR1:def 10;
  hence x*(A-B) =Line((LineVec2Mx x)*A-(LineVec2Mx x)*B,1) by A1,A2,A3,A4,A5
,Th20
    .=(x*A) - (x*B) by A8,A7,A6,Th25;
end;

theorem
  for x being FinSequence of REAL, 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
  let x be FinSequence of REAL,A,B be Matrix of REAL;
  assume that
A1: len x=width A and
A2: len A=len B and
A3: width A=width B and
A4: len x >0 and
A5: len A >0;
A6: len ColVec2Mx x=len x by A4,MATRIXR1:def 9;
  then
A7: len (A*(ColVec2Mx x))=len A by A1,MATRIX_3:def 4
    .=len (B*(ColVec2Mx x)) by A1,A2,A3,A6,MATRIX_3:def 4;
A8: width (A*(ColVec2Mx x))=width (ColVec2Mx x) by A1,A6,MATRIX_3:def 4
    .=1 by A4,MATRIXR1:45;
A9: width (A*(ColVec2Mx x))= width (ColVec2Mx x) by A1,A6,MATRIX_3:def 4
    .= width (B*(ColVec2Mx x)) by A1,A3,A6,MATRIX_3:def 4;
  thus (A-B)*x =Col(A*(ColVec2Mx x)-B*(ColVec2Mx x),1) by A1,A2,A3,A4,A5,A6
,Th16
    .=(A*x) - (B*x) by A7,A9,A8,Th26;
end;

theorem Th56:
  for x being FinSequence of REAL,A being Matrix of REAL st len A=
  len x holds (LineVec2Mx x)*A=LineVec2Mx (x*A)
proof
  let x be FinSequence of REAL,A be Matrix of REAL;
A1: len LineVec2Mx (x*A)=1 by MATRIXR1:def 10;
  assume
A2: len A=len x;
  then
A3: width (MXR2MXF(LineVec2Mx x))=len MXR2MXF A by MATRIXR1:def 10;
  width LineVec2Mx (x*A)=len (x*A) by MATRIXR1:def 10;
  then
A4: width (LineVec2Mx (x*A))=width A by A2,MATRIXR1:62;
A5: len (x*A)=width A by A2,MATRIXR1:62;
  then
A6: width (MXR2MXF (LineVec2Mx (x*A)))= width MXR2MXF A by MATRIXR1:def 10;
A7: width (LineVec2Mx x)=len x by MATRIXR1:def 10;
A8: for i,j being Nat st [i,j] in Indices (MXR2MXF (LineVec2Mx (x*A)))
holds MXR2MXF (LineVec2Mx (x*A))*(i,j) =Line(MXR2MXF(LineVec2Mx x),i) "*" Col((
  MXR2MXF A),j)
  proof
    len ((MXR2MXF (LineVec2Mx x))*(MXR2MXF A)) =len MXR2MXF LineVec2Mx x
    by A3,MATRIX_3:def 4;
    then len ((MXR2MXF (LineVec2Mx x))*(MXR2MXF A)) = 1 by MATRIXR1:def 10;
    then
A9: 1 in Seg len ((MXR2MXF (LineVec2Mx x))*(MXR2MXF A));
    let i,j be Nat;
A10: width ((LineVec2Mx x)*A)=width A by A2,A7,MATRIX_3:def 4;
    assume
A11: [i,j] in Indices (MXR2MXF (LineVec2Mx (x*A)));
    then
A12: j in Seg (width A) by A4,ZFMISC_1:87;
    then j in dom (x*A) by A5,FINSEQ_1:def 3;
    then
A13: (Line((LineVec2Mx x)*A,1)).j=(LineVec2Mx (x*A))*(1,j) by MATRIXR1:def 10;
    Indices (LineVec2Mx (x*A))=[:Seg 1,Seg (width A):] by A1,A4,FINSEQ_1:def 3;
    then i in Seg 1 by A11,ZFMISC_1:87;
    then 1<=i & i<=1 by FINSEQ_1:1;
    then
A14: i=1 by XXREAL_0:1;
    width ((MXR2MXF (LineVec2Mx x))*(MXR2MXF A))=width A by A3,MATRIX_3:def 4;
    then [1,j] in [:Seg len ((MXR2MXF (LineVec2Mx x))*(MXR2MXF A)), Seg width
    ((MXR2MXF (LineVec2Mx x))*(MXR2MXF A)):] by A12,A9,ZFMISC_1:87;
    then
A15: [1,j] in Indices ((MXR2MXF (LineVec2Mx x))*(MXR2MXF A)) by FINSEQ_1:def 3;
    width MXR2MXF LineVec2Mx x = len MXR2MXF A by A2,MATRIXR1:def 10;
    then ((LineVec2Mx x)*A)*(1,j) =Line((MXR2MXF (LineVec2Mx x)),i) "*" Col((
    MXR2MXF A),j) by A14,A15,MATRIX_3:def 4;
    hence thesis by A12,A14,A13,A10,MATRIX_1:def 7;
  end;
  len MXR2MXF (LineVec2Mx (x*A)) = len (MXR2MXF(LineVec2Mx x)) by A1,
MATRIXR1:def 10;
  hence thesis by A6,A3,A8,MATRIX_3:def 4;
end;

theorem Th57:
  for x being FinSequence of REAL, A,B being Matrix of REAL st len
  x=len A & width A=len B holds x*(A*B)=(x*A)*B
proof
  let x be FinSequence of REAL,A,B be Matrix of REAL;
  assume that
A1: len x=len A and
A2: width A=len B;
  width LineVec2Mx x=len x by MATRIXR1:def 10;
  hence x*(A*B) = Line((LineVec2Mx x)*A*B,1) by A1,A2,MATRIX_3:33
    .=(x*A)*B by A1,Th56;
end;

theorem Th58:
  for x being FinSequence of REAL,A being Matrix of REAL st width
  A=len x & len x>0 & len A>0 holds A*(ColVec2Mx x)=ColVec2Mx (A*x)
proof
  let x be FinSequence of REAL,A be Matrix of REAL;
  assume that
A1: width A=len x and
A2: len x>0 and
A3: len A>0;
A4: len ColVec2Mx x=len x by A2,MATRIXR1:def 9;
A5: len (MXR2MXF(ColVec2Mx x))=width MXR2MXF A by A1,A2,MATRIXR1:def 9;
  then
A6: width ((MXR2MXF A)*(MXR2MXF (ColVec2Mx x)))=width(ColVec2Mx x) by
MATRIX_3:def 4
    .=1 by A2,MATRIXR1:def 9;
A7: len ((MXR2MXF A)*(MXR2MXF (ColVec2Mx x)))=len A by A5,MATRIX_3:def 4;
A8: len (A*x)=len A by A1,A2,MATRIXR1:61;
  then
A9: width (ColVec2Mx (A*x))=1 by A3,MATRIXR1:def 9;
A10: len (ColVec2Mx (A*x))=len A by A3,A8,MATRIXR1:def 9;
A11: len (ColVec2Mx (A*x))=len (A*x) by A3,A8,MATRIXR1:def 9;
A12: for i,j being Nat st [i,j] in Indices (MXR2MXF (ColVec2Mx (A*x))) holds
MXR2MXF (ColVec2Mx (A*x))*(i,j) =Line((MXR2MXF A),i) "*" Col(MXR2MXF(ColVec2Mx
  x),j)
  proof
    let i,j be Nat;
A13: 1 in Seg 1 & Indices (ColVec2Mx (A*x))=[:Seg (len (ColVec2Mx (A*x))),
    Seg 1:] by A9,FINSEQ_1:def 3;
    assume
A14: [i,j] in Indices MXR2MXF (ColVec2Mx (A*x));
    then
A15: j in Seg width ((MXR2MXF A)*(MXR2MXF (ColVec2Mx x))) by A9,A6,ZFMISC_1:87
;
A16: Indices (ColVec2Mx (A*x))=[:Seg len A,Seg 1:] by A8,A11,A9,FINSEQ_1:def 3;
    then
A17: i in Seg (len A) by A14,ZFMISC_1:87;
    then
A18: i in dom (A*x) by A8,FINSEQ_1:def 3;
    i in Seg len ((MXR2MXF A)*(MXR2MXF (ColVec2Mx x))) by A7,A14,A16,
ZFMISC_1:87;
    then
    [i,j] in [:Seg len ((MXR2MXF A)*(MXR2MXF (ColVec2Mx x))), Seg width (
    (MXR2MXF A)*(MXR2MXF (ColVec2Mx x))):] by A15,ZFMISC_1:87;
    then
A19: [i,j] in Indices ((MXR2MXF A)*(MXR2MXF (ColVec2Mx x))) by FINSEQ_1:def 3;
    j in Seg 1 by A9,A14,ZFMISC_1:87;
    then 1<=j & j<=1 by FINSEQ_1:1;
    then
A20: j=1 by XXREAL_0:1;
    i in Seg (len (ColVec2Mx (A*x))) by A10,A14,A16,ZFMISC_1:87;
    then [i,1] in Indices (ColVec2Mx (A*x)) by A13,ZFMISC_1:87;
    then
A21: ex p2 being FinSequence of REAL st p2=(ColVec2Mx (A*x)).i & (ColVec2Mx
    (A*x))*(i,1)=p2.1 by MATRIX_1:def 5;
A22: (Col(A*(ColVec2Mx x),1)).i =(<*(A*x).i*>).1 by FINSEQ_1:40
      .=(ColVec2Mx (A*x))*(i,1) by A3,A8,A18,A21,MATRIXR1:def 9;
    len (A*(ColVec2Mx x))=len A by A1,A4,MATRIX_3:def 4;
    then i in dom (A*(ColVec2Mx x)) by A17,FINSEQ_1:def 3;
    then (Col(A*(ColVec2Mx x),1)).i=(A*(ColVec2Mx x))*(i,j) by A20,
MATRIX_1:def 8;
    hence thesis by A5,A20,A22,A19,MATRIX_3:def 4;
  end;
A23: len (MXR2MXF (ColVec2Mx (A*x))) = len (MXR2MXF A) by A3,A8,MATRIXR1:def 9;
  width (MXR2MXF (ColVec2Mx (A*x))) = 1 by A3,A8,MATRIXR1:def 9
    .= width (MXR2MXF(ColVec2Mx x)) by A2,MATRIXR1:def 9;
  hence thesis by A23,A5,A12,MATRIX_3:def 4;
end;

theorem Th59:
  for x being FinSequence of REAL, 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
  let x be FinSequence of REAL,A,B be Matrix of REAL;
  assume that
A1: len x=width B and
A2: width A=len B and
A3: len x >0 and
A4: len B>0;
  len ColVec2Mx x=len x by A3,MATRIXR1:def 9;
  hence (A*B)*x = Col(A*(B*(ColVec2Mx x)),1) by A1,A2,MATRIX_3:33
    .=A*(B*x) by A1,A3,A4,Th58;
end;

theorem
  for B being (Matrix of n,m,REAL),A being (Matrix of m,k,REAL) st n>0
  holds (for i,j st [i,j] in Indices (B*A) holds (B*A)*(i,j)=((Line(B,i))*A).j)
proof
  let B be (Matrix of n,m,REAL),A be (Matrix of m,k,REAL);
  assume
A1: n>0;
  then
A2: width B=m by MATRIX_1:23;
  let i,j;
A3: len A=m by MATRIX_1:def 2;
  then
A4: len A=len (Line(B,i)) by A2,MATRIX_1:def 7;
  assume
A5: [i,j] in Indices (B*A);
  then
A6: j in Seg width (B*A) by ZFMISC_1:87;
  width B=len A by A1,A3,MATRIX_1:23;
  then
A7: (B*A)*(i,j) =Line(B,i) "*" Col(A,j) by A5,MATRPROB:39;
  width A=width (B*A) by A3,A2,MATRPROB:39;
  then j in Seg len ((Line(B,i))*A) by A6,A4,MATRIXR1:62;
  hence thesis by A7,A4,MATRPROB:40;
end;

theorem Th61:
  for A, B being Matrix of n,REAL holds for i,j st [i,j] in
  Indices (B*A) holds (B*A)*(i,j)=((Line(B,i))*A).j
proof
  let A,B be Matrix of n,REAL;
  let i,j;
  assume
A1: [i,j] in Indices (B*A);
  then
A2: j in Seg width (B*A) by ZFMISC_1:87;
A3: len A=n by MATRIX_1:def 2;
  then width B=len A by MATRIX_1:24;
  then
A4: (B*A)*(i,j) =Line(B,i) "*" Col(A,j) by A1,MATRPROB:39;
A5: width B=n by MATRIX_1:24;
  then
A6: len A=len (Line(B,i)) by A3,MATRIX_1:def 7;
  width A=width (B*A) by A3,A5,MATRPROB:39;
  then j in Seg len ((Line(B,i))*A) by A2,A6,MATRIXR1:62;
  hence thesis by A4,A6,MATRPROB:40;
end;

theorem
  for A, B being Matrix of n,REAL st n>0 holds for i,j st [i,j] in
  Indices (A*B) holds (A*B)*(i,j)=(A*(Col(B,j))).i
proof
  let A, B be Matrix of n,REAL;
  assume
A1: n>0;
  let i,j;
A2: width A=n by MATRIX_1:24;
  assume
A3: [i,j] in Indices (A*B);
  then i in dom (A*B) by ZFMISC_1:87;
  then
A4: i in Seg len (A*B) by FINSEQ_1:def 3;
A5: len B=n by MATRIX_1:def 2;
  then
A6: width A=len (Col(B,j)) by A2,MATRIX_1:def 8;
  width A=len B by A5,MATRIX_1:24;
  then
A7: (A*B)*(i,j) = Line(A,i) "*" Col(B,j) by A3,MATRPROB:39;
  len (A*B)=n & len A=n by MATRIX_1:24;
  then i in Seg len (A*(Col(B,j))) by A1,A4,A2,A6,MATRIXR1:61;
  hence thesis by A1,A2,A7,A6,MATRPROB:41;
end;

begin :: Identity and Zero of Matrix of REAL

definition
  let n be Element of NAT;
  func 1_Rmatrix(n) -> Matrix of n,REAL equals
  MXF2MXR (1.(F_Real,n));
  correctness;
end;

theorem Th63:
  (for i st [i,i] in Indices 1_Rmatrix n holds (1_Rmatrix n)*(i,i)
= 1) & for i,j st [i,j] in Indices (1_Rmatrix n) & i <> j holds (1_Rmatrix n)*(
  i,j) = 0
proof
  set K=F_Real;
  thus for i st [i,i] in Indices 1_Rmatrix n holds (1_Rmatrix n)*(i,i) = 1
  proof
    let i;
    assume [i,i] in Indices 1_Rmatrix n;
    hence (1_Rmatrix n)*(i,i) = 1_ F_Real by MATRIX_1:def 11
      .=1;
  end;
  let i,j;
  assume [i,j] in Indices 1_Rmatrix n & i <> j;
  hence (1_Rmatrix n)*(i,j) = 0.K by MATRIX_1:def 11
    .=0;
end;

theorem Th64:
  (1_Rmatrix(n))@=1_Rmatrix(n)
proof
  per cases;
  suppose
A1: n>0;
A2: len (1_Rmatrix(n))=n by MATRIX_1:24;
A3: Indices (1_Rmatrix(n)) = [:Seg n, Seg n:] by MATRIX_1:24;
A4: for i,j being Nat st [i,j] in Indices (1_Rmatrix(n)) holds (1_Rmatrix(
    n))*(i,j)=((1_Rmatrix(n))@)*(i,j)
    proof
      let i,j be Nat;
      reconsider i0=i,j0=j as Element of NAT by ORDINAL1:def 12;
      assume
A5:   [i,j] in Indices (1_Rmatrix(n));
      then i in Seg n & j in Seg n by A3,ZFMISC_1:87;
      then
A6:   [j,i] in Indices (1_Rmatrix(n) ) by A3,ZFMISC_1:87;
      per cases;
      suppose
        i=j;
        hence thesis by A5,MATRIX_1:def 6;
      end;
      suppose
        i<>j;
        then (1_Rmatrix(n))*(i0,j0)=0 & (1_Rmatrix(n))*(j0,i0)=0 by A5,A6,Th63;
        hence thesis by A6,MATRIX_1:def 6;
      end;
    end;
A7: width (1_Rmatrix(n))=n by MATRIX_1:24;
    then
    len ((1_Rmatrix(n))@)=width (1_Rmatrix(n)) & width ((1_Rmatrix(n))@)=
    len ( 1_Rmatrix n) by A1,MATRIX_2:10;
    hence thesis by A7,A2,A4,MATRIX_1:21;
  end;
  suppose
    n=0;
    hence thesis by MATRIX_1:35;
  end;
end;

theorem Th65:
  for n,m being Element of NAT st n>0 holds 0_Rmatrix(n,m)+
  0_Rmatrix(n,m)=0_Rmatrix(n,m)
proof
  let n,m be Element of NAT;
  assume
A1: n>0;
  then width (0_Rmatrix(n,m))=m & len (0_Rmatrix(n,m))=n by MATRIX_1:23;
  then (0+0) *(0_Rmatrix(n,m))=0_Rmatrix(n,m) by A1,MATRIXR1:44;
  hence thesis by Th12;
end;

theorem
  for a being Real st n>0 holds a*(0_Rmatrix(n,m)) = 0_Rmatrix(n,m)
proof
  let a be Real;
A1: len (a*(0_Rmatrix(n,m)))=len (0_Rmatrix(n,m)) & width (a*(0_Rmatrix(n,m)
  ))= width (0_Rmatrix(n,m)) by MATRIXR1:27;
  assume
A2: n>0;
  then
A3: width (0_Rmatrix(n,m))=m & len (0_Rmatrix(n,m))=n by MATRIX_1:23;
  a*(0_Rmatrix(n,m))=a*(0_Rmatrix(n,m)+0_Rmatrix(n,m)) by A2,Th65
    .=a*(0_Rmatrix(n,m)) +a*(0_Rmatrix(n,m)) by A3,MATRIXR1:43;
  hence thesis by A3,A1,MATRIXR1:37;
end;

theorem Th67:
  for K being Field, A being Matrix of K holds A*(1.(K,width A))=A
proof
  let K be Field, A be Matrix of K;
  set n=width A;
  set B=1.(K,n);
A1: width B=n by MATRIX_1:24;
A2: len B=n by MATRIX_1:24;
  then
A3: width (A*B)=width B by MATRIX_3:def 4;
A4: now
    let i,j be Nat;
    assume
A5: [i,j] in Indices (A*B);
    then
A6: j in Seg width B by A3,ZFMISC_1:87;
    then j in Seg len (Line(A,i)) by A1,MATRIX_1:def 7;
    then
A7: j in dom (Line(A,i)) by FINSEQ_1:def 3;
A8: now
      let k be Nat;
      assume that
A9:   k in dom (Col(B,j)) and
A10:  k<>j;
      k in Seg len (Col(B,j)) by A9,FINSEQ_1:def 3;
      then k in Seg len B by MATRIX_1:def 8;
      then k in dom B by FINSEQ_1:def 3;
      then [k,j] in Indices B by A6,ZFMISC_1:87;
      hence (Col(B,j)).k=0.K by A10,MATRIX_3:16;
    end;
A11: j in Seg width A by A1,A3,A5,ZFMISC_1:87;
    then j in dom B by A2,FINSEQ_1:def 3;
    then [j,j] in Indices B by A1,A11,ZFMISC_1:87;
    then
A12: (Col(B,j)).j=1_K by MATRIX_3:16;
    j in Seg len (Col(B,j)) by A2,A1,A6,MATRIX_1:def 8;
    then
A13: j in dom (Col(B,j)) by FINSEQ_1:def 3;
    thus (A*B)*(i,j)= Line(A,i) "*" Col(B,j) by A2,A5,MATRIX_3:def 4
      .=Col(B,j) "*" Line(A,i) by FVSUM_1:90
      .=Sum(mlt(Col(B,j),Line(A,i))) by FVSUM_1:def 9
      .=Line(A,i).j by A13,A7,A8,A12,MATRIX_3:17
      .=A*(i,j) by A11,MATRIX_1:def 7;
  end;
  len (A*B)=len A by A2,MATRIX_3:def 4;
  hence thesis by A1,A3,A4,MATRIX_1:21;
end;

theorem Th68:
  for A being Matrix of K holds (1.(K,len A))*A=A
proof
  let A be Matrix of K;
  set n=len A;
  set B=1.(K,n);
A1: len B=n by MATRIX_1:24;
A2: width B=n by MATRIX_1:24;
  then
A3: len (B*A)=len B by MATRIX_3:def 4;
A4: now
A5: dom A = Seg len A by FINSEQ_1:def 3;
    let i,j be Nat;
    assume
A6: [i,j] in Indices (B*A);
A7: dom (B*A) = Seg len (B*A) by FINSEQ_1:def 3;
    then
A8: i in Seg width B by A1,A2,A3,A6,ZFMISC_1:87;
    then i in Seg len(Line(B,i)) by MATRIX_1:def 7;
    then
A9: i in dom (Line(B,i)) by FINSEQ_1:def 3;
A10: dom B = Seg len B by FINSEQ_1:def 3;
    then
A11: i in dom B by A3,A6,A7,ZFMISC_1:87;
    then [i,i] in Indices B by A8,ZFMISC_1:87;
    then
A12: (Line(B,i)).i=1_K by MATRIX_3:15;
    i in Seg len (Col(A,j)) by A2,A8,MATRIX_1:def 8;
    then
A13: i in dom Col(A,j) by FINSEQ_1:def 3;
A14: now
      let k be Nat;
      assume that
A15:  k in dom (Line (B,i)) and
A16:  k<>i;
      k in Seg len (Line (B,i)) by A15,FINSEQ_1:def 3;
      then k in Seg width B by MATRIX_1:def 7;
      then [i,k] in Indices B by A11,ZFMISC_1:87;
      hence (Line(B,i)).k=0.K by A16,MATRIX_3:15;
    end;
    thus (B*A)*(i,j)= Line(B,i) "*" Col(A,j) by A2,A6,MATRIX_3:def 4
      .=Sum(mlt(Line(B,i),Col(A,j))) by FVSUM_1:def 9
      .=Col(A,j).i by A9,A13,A14,A12,MATRIX_3:17
      .=A*(i,j) by A1,A5,A10,A11,MATRIX_1:def 8;
  end;
  width (B*A)=width A by A2,MATRIX_3:def 4;
  hence thesis by A1,A3,A4,MATRIX_1:21;
end;

theorem
  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:
  for A being Matrix of n,REAL holds (1_Rmatrix n)*A=A
proof
  let A be Matrix of n,REAL;
  n=len A by MATRIX_1:def 2;
  hence thesis by Th68;
end;

theorem Th71:
  for A be Matrix of n,REAL holds A*(1_Rmatrix(n))=A
proof
  let A be Matrix of n,REAL;
A1: n=len A by MATRIX_1:def 2;
  now
    per cases;
    case
      n<>0;
      hence n=width A by A1,MATRIX_1:20;
    end;
    case
      n=0;
      hence n=width A by A1,MATRIX_1:def 3;
    end;
  end;
  hence thesis by Th67;
end;

theorem Th72:
  Det 1_Rmatrix n=1
proof
  per cases;
  suppose
    n>=1;
    hence Det 1_Rmatrix n=1_(F_Real) by MATRIX_7:16
      .= 1;
  end;
  suppose
    n<1;
    then n=0 by NAT_1:25;
    hence Det (1_Rmatrix n)=1.F_Real by Th41
      .=1;
  end;
end;

definition
  let n be Element of NAT;
  func 0_Rmatrix(n) -> Matrix of n,REAL equals
  0_Rmatrix(n,n);
  correctness;
end;

theorem
  n>0 implies Det 0_Rmatrix n = 0
proof
  set K=F_Real;
  assume n>0;
  then n>=0+1 by NAT_1:13;
  then Det (0_Rmatrix n)=0.K by MATRIX_7:15
    .=0;
  hence thesis;
end;

definition
  let n,i be Nat;
  func Base_FinSeq(n,i) -> FinSequence of REAL equals
  (n |-> 0)+*(i,1);
  coherence
  proof
    reconsider n as Element of NAT by ORDINAL1:def 12;
    (n |-> 0)+*(i,1) = Replace(n |-> 0, i,1);
    hence thesis;
  end;
end;

reserve n,i,j for Nat;

theorem Th74:
  len Base_FinSeq(n,i) = n
proof
  len((n |-> 0)+*(i,1)) = len (n |-> 0) by FUNCT_7:97
    .= n by CARD_1:def 7;
  hence thesis;
end;

theorem Th75:
  1<=i & i<=n implies (Base_FinSeq(n,i)).i=1
proof
A1: len (n |-> 0)=n by CARD_1:def 7;
  assume 1<=i & i<=n;
  then i in dom(n |-> 0) by A1,FINSEQ_3:25;
  hence thesis by FUNCT_7:31;
end;

theorem Th76:
  1<=j & j<=n & i<>j implies (Base_FinSeq(n,i)).j=0
proof
  assume that
A1: 1<=j & j<=n and
A2: i<>j;
A3: j in Seg n by A1,FINSEQ_1:1;
  thus (Base_FinSeq(n,i)).j = (n |-> 0).j by A2,FUNCT_7:32
    .= 0 by A3,FINSEQ_2:57;
end;

reserve n for Element of NAT;

theorem
  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
  thus Base_FinSeq(1,1) = Replace (<* 0 *>,1,1) by FINSEQ_2:59
    .= <* 1 *> by FINSEQ_7:12;
  thus Base_FinSeq(2,1) = Replace (<* 0 qua Element of REAL,0 qua Element of
  REAL *>,1,1) by FINSEQ_2:61
    .= <* 1,0 *> by FINSEQ_7:13;
  thus Base_FinSeq(2,2) = Replace (<* 0 qua Element of REAL,0 qua Element of
  REAL *>,2,1) by FINSEQ_2:61
    .= <* 0,1 *> by FINSEQ_7:14;
  thus Base_FinSeq(3,1) = Replace (<* 0 qua Element of REAL,0 qua Element of
  REAL,0 *>,1,1) by FINSEQ_2:62
    .= <* 1,0,0 *> by FINSEQ_7:15;
  thus Base_FinSeq(3,2) = Replace (<* 0 qua Element of REAL,0 qua Element of
  REAL, 0 qua Element of REAL *>,2,1) by FINSEQ_2:62
    .= <* 0,1,0 *> by FINSEQ_7:16;
  thus Base_FinSeq(3,3) = Replace (<* 0 qua Element of REAL,0 qua Element of
  REAL, 0 qua Element of REAL *>,3,1) by FINSEQ_2:62
    .= <* 0,0,1 *> by FINSEQ_7:17;
end;

theorem Th78:
  1<=i & i<=n implies (1_Rmatrix(n)).i=Base_FinSeq(n,i)
proof
  assume
A1: 1<=i & i<=n;
  then 1<=n by XXREAL_0:2;
  then
A2: 1 in Seg n;
  i in NAT by ORDINAL1:def 12;
  then i in Seg n by A1;
  then [i,1] in [:Seg n, Seg n:] by A2,ZFMISC_1:87;
  then [i,1] in Indices (1.(F_Real,n)) by MATRIX_1:24;
  then consider q being FinSequence of REAL such that
A3: q = (1_Rmatrix n).i and
  (1_Rmatrix n)*(i,1) = q.1 by MATRIX_1:def 5;
  len (1_Rmatrix(n))=n by MATRIX_1:24;
  then i in dom 1_Rmatrix n by A1,FINSEQ_3:25;
  then q in rng 1_Rmatrix n by A3,FUNCT_1:def 3;
  then
A4: len q=n by MATRIX_1:def 2;
A5: for j be Nat st 1<=j & j<=n holds q.j=(Base_FinSeq(n,i)).j
  proof
    i in NAT by ORDINAL1:def 12;
    then
A6: i in Seg n by A1;
    let j be Nat;
    assume
A7: 1<=j & j<=n;
    j in NAT by ORDINAL1:def 12;
    then j in Seg n by A7;
    then [i,j] in [:Seg n, Seg n:] by A6,ZFMISC_1:87;
    then
A8: [i,j] in Indices (1.(F_Real,n)) by MATRIX_1:24;
    then
A9: ex q0 being FinSequence of REAL st q0 = (1_Rmatrix(n)).i & (1_Rmatrix(
    n))*(i,j) = q0.j by MATRIX_1:def 5;
    per cases;
    suppose
A10:  i=j;
      then (1.(F_Real,n))*(i,i) = 1_(F_Real) by A8,MATRIX_1:def 11;
      hence thesis by A1,A3,A9,A10,Th75;
    end;
    suppose
A11:  i<>j;
      then (1.(F_Real,n))*(i,j) = 0.(F_Real) by A8,MATRIX_1:def 11;
      hence thesis by A3,A7,A9,A11,Th76;
    end;
  end;
  len Base_FinSeq(n,i)=n by Th74;
  hence thesis by A3,A4,A5,FINSEQ_1:14;
end;

begin :: Inverse of Matrix

definition
  let n be Element of NAT,A be Matrix of n,REAL;
  attr A is invertible means
  :Def5:
  ex B being Matrix of n,REAL st B*A= 1_Rmatrix(n) & A*B=1_Rmatrix(n);
end;

definition
  let n be Element of NAT,A be Matrix of n,REAL;
  assume
A1: A is invertible;
  func Inv(A) -> Matrix of n,REAL means
  :Def6:
  it*A=1_Rmatrix(n) & A*it= 1_Rmatrix(n);
  existence by A1,Def5;
  uniqueness
  proof
    let B1,B2 be Matrix of n,REAL;
    assume that
    B1*A=1_Rmatrix(n) and
A2: A*B1=1_Rmatrix(n) and
A3: B2*A=1_Rmatrix(n) and
    A*B2=1_Rmatrix(n);
A4: len A=n & width A=n by MATRIX_1:24;
    len B1=n & width B2=n by MATRIX_1:24;
    then B2*A*B1=B2*1_Rmatrix(n) by A2,A4,MATRIX_3:33;
    then B1=B2*1_Rmatrix(n) by A3,Th70;
    hence thesis by Th71;
  end;
end;

registration
  let n;
  cluster 1_Rmatrix n -> invertible;
  coherence
  proof
    (1_Rmatrix(n))*(1_Rmatrix(n))=1_Rmatrix(n) by Th70;
    hence thesis by Def5;
  end;
end;

theorem
  Inv(1_Rmatrix(n))=1_Rmatrix(n)
proof
  (1_Rmatrix(n))*(1_Rmatrix n)=1_Rmatrix(n) by Th70;
  hence thesis by Def6;
end;

theorem Th80:
  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
  let A,B1,B2 be Matrix of n,REAL;
  assume that
A1: B1*A=1_Rmatrix(n) and
A2: A*B2=1_Rmatrix(n);
A3: B1*A*B2=B1*(A*B2) by Th28
    .= B1 by A2,Th71;
  hence B1=B2 by A1,Th70;
  B1*A*B2=B2 by A1,Th70;
  hence thesis by A1,A2,A3,Def5;
end;

theorem
  for A being Matrix of n,REAL st A is invertible holds Det Inv A = (Det A)"
proof
  let A be Matrix of n,REAL;
  assume A is invertible;
  then A*(Inv A)=1_Rmatrix(n) by Def6;
  then Det (A*(Inv A))=1 by Th72;
  then
A1: Det(A)*Det (Inv A)=1 by Th46;
  per cases;
  suppose
    Det A <> 0;
    hence thesis by A1,XCMPLX_0:def 7;
  end;
  suppose
    Det A=0;
    hence thesis by A1;
  end;
end;

theorem
  for A being Matrix of n,REAL st A is invertible holds Det A <> 0
proof
  let A be Matrix of n,REAL;
  assume A is invertible;
  then A*(Inv A)=1_Rmatrix(n) by Def6;
  then Det (A*(Inv A))=1 by Th72;
  then Det(A)*Det Inv A=1 by Th46;
  hence thesis;
end;

theorem
  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
  let A,B be Matrix of n,REAL;
  assume that
A1: A is invertible and
A2: B is invertible;
A3: (Inv(B)*(Inv(A)))*(A*B)=(Inv(B)*(Inv(A)))*A*B by Th28
    .=(Inv(B))*((Inv(A))*A)*B by Th28
    .=(Inv(B))*(1_Rmatrix(n))*B by A1,Def6
    .=(Inv(B))*B by Th71
    .=1_Rmatrix(n) by A2,Def6;
A4: (A*B)*(Inv(B)*(Inv(A)))=A*(B*(Inv(B)*(Inv(A)))) by Th28
    .=A*((B*(Inv(B)))*(Inv(A))) by Th28
    .=A*((1_Rmatrix(n))*(Inv(A))) by A2,Def6
    .=A*(1_Rmatrix(n))*(Inv(A)) by Th28
    .=A*(Inv(A)) by Th71
    .=1_Rmatrix(n) by A1,Def6;
  hence A*B is invertible by A3,Def5;
  hence thesis by A3,A4,Def6;
end;

theorem
  for A be Matrix of n,REAL st A is invertible holds Inv Inv A = A
proof
  let A be Matrix of n,REAL;
  assume A is invertible;
  then
A1: Inv(A)*A=1_Rmatrix(n) & A*(Inv(A))=1_Rmatrix(n) by Def6;
  then Inv(A) is invertible by Def5;
  hence thesis by A1,Def6;
end;

theorem
  1_Rmatrix(0)=0_Rmatrix(0) & 1_Rmatrix(0)={}
proof
A1: len 1_Rmatrix(0) = 0 by MATRIX_1:24;
  len 0_Rmatrix(0) = 0 by MATRIX_1:24;
  then 0_Rmatrix(0)={};
  hence 1_Rmatrix(0)=0_Rmatrix(0) by A1;
  thus thesis by A1;
end;

theorem Th86:
  for x being FinSequence of REAL st len x=n & n>0 holds ( 1_Rmatrix n)*x=x
proof
  let x be FinSequence of REAL;
  assume that
A1: len x=n and
A2: n>0;
A3: len (ColVec2Mx x)=len x by A1,A2,MATRIXR1:def 9;
A4: len Col((ColVec2Mx x),1) = len (ColVec2Mx x) by MATRIX_1:def 8;
A5: for k being Nat st 1 <=k & k <= len (Col((ColVec2Mx x),1)) holds (Col((
  ColVec2Mx x),1)).k=x.k
  proof
    let k be Nat;
    assume
A6: 1 <=k & k <= len (Col((ColVec2Mx x),1));
    k in NAT by ORDINAL1:def 12;
    then
A7: k in Seg len ColVec2Mx x by A4,A6;
    then
A8: k in dom (ColVec2Mx x) by FINSEQ_1:def 3;
    then
A9: Col((ColVec2Mx x),1).k = (ColVec2Mx x)*(k,1) by MATRIX_1:def 8;
    1 in Seg 1 & Indices (ColVec2Mx x)=[:dom (ColVec2Mx x),Seg 1:] by A1,A2,
MATRIXR1:def 9;
    then [k,1] in Indices (ColVec2Mx x) by A8,ZFMISC_1:87;
    then consider p being FinSequence of REAL such that
A10: p=(ColVec2Mx x).k and
A11: (ColVec2Mx x)*(k,1)=p.1 by MATRIX_1:def 5;
    k in dom x by A3,A7,FINSEQ_1:def 3;
    then p=<* x.k *> by A1,A2,A10,MATRIXR1:def 9;
    hence thesis by A9,A11,FINSEQ_1:40;
  end;
  (1_Rmatrix n)*x =Col(MXF2MXR (MXR2MXF (ColVec2Mx x)),1) by A1,A3,Th68
    .=x by A3,A4,A5,FINSEQ_1:14;
  hence thesis;
end;

theorem Th87:
  for n being Element of NAT,x,y being FinSequence of REAL, A be
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
  let n be Element of NAT,x,y be FinSequence of REAL, A be Matrix of n,REAL;
  assume that
A1: A is invertible and
A2: len x=n and
A3: len y=n and
A4: n>0;
A5: width A=n & width (Inv(A))=n by MATRIX_1:24;
A6: len A=n by MATRIX_1:24;
  thus A*x=y implies x=Inv(A)*y
  proof
    assume
A7: A*x=y;
    thus x=(1_Rmatrix(n))*x by A2,A4,Th86
      .=((Inv A)*A) *x by A1,Def6
      .=Inv(A)*y by A2,A4,A6,A5,A7,Th59;
  end;
A8: len (Inv(A))=n by MATRIX_1:24;
  x=Inv(A)*y implies A*x=y
  proof
    assume
A9: x=Inv(A)*y;
    thus y=(1_Rmatrix(n))*y by A3,A4,Th86
      .=(A*(Inv A))*y by A1,Def6
      .=A*x by A3,A4,A8,A5,A9,Th59;
  end;
  hence thesis;
end;

theorem Th88:
  for x being FinSequence of REAL st len x=n holds x*(1_Rmatrix n) =x
proof
  let x be FinSequence of REAL;
A1: width (LineVec2Mx x)=len x by MATRIXR1:def 10;
  assume len x=n;
  then x*(1_Rmatrix n) =Line(MXF2MXR (MXR2MXF (LineVec2Mx x)),1) by A1,Th67
    .=x by MATRIXR1:48;
  hence thesis;
end;

theorem Th89:
  for x,y being FinSequence of REAL,A be Matrix of n,REAL st A is
  invertible & len x=n & len y=n holds x*A=y iff x=y*Inv(A)
proof
  let x,y be FinSequence of REAL, A be Matrix of n,REAL;
  assume that
A1: A is invertible and
A2: len x=n and
A3: len y=n;
A4: len A=n & len Inv A=n by MATRIX_1:24;
A5: width A=n by MATRIX_1:24;
  thus x*A=y implies x=y*Inv(A)
  proof
    assume
A6: x*A=y;
    thus x=x*(1_Rmatrix n) by A2,Th88
      .=x*(A*(Inv A)) by A1,Def6
      .=y*(Inv A) by A2,A5,A4,A6,Th57;
  end;
  assume
A7: x=y*(Inv A);
A8: width Inv A=n by MATRIX_1:24;
  thus y=y*(1_Rmatrix(n)) by A3,Th88
    .= y*((Inv A)*A) by A1,Def6
    .= x*A by A3,A4,A8,A7,Th57;
end;

theorem
  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
  let A be Matrix of n,REAL;
  assume that
A1: n>0 and
A2: A is invertible;
  let y be FinSequence of REAL;
  assume
A3: len y=n;
  reconsider x0=(Inv A)*y as FinSequence of REAL;
  len Inv(A)=n & width Inv(A) =n by MATRIX_1:24;
  then
A4: len x0=n by A1,A3,MATRIXR1:61;
  then A*x0=y by A1,A2,A3,Th87;
  hence thesis by A4;
end;

theorem
  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
  let A be Matrix of n,REAL;
  assume
A1: A is invertible;
  let y be FinSequence of REAL;
  assume
A2: len y=n;
  reconsider x0=y*(Inv A) as FinSequence of REAL;
  len Inv(A)=n by MATRIX_1:24;
  then
A3: len x0=width Inv A by A2,MATRIXR1:62
    .=n by MATRIX_1:24;
  then x0*A=y by A1,A2,Th89;
  hence thesis by A3;
end;

theorem
  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 Element of NAT st 1<=j & j<=n holds y.j
  =|(x,Col(A,j))|
proof
  let A be Matrix of n,REAL;
  let x,y be FinSequence of REAL;
  assume that
A1: len x=n and
A2: len y=n and
A3: x*A=y;
  let j be Element of NAT;
  assume 1<=j & j<=n;
  then j in Seg len (x*A) by A2,A3;
  hence thesis by A1,A3,MATRIX_1:24,MATRPROB:40;
end;

theorem Th93:
  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
  let A be Matrix of n,REAL;
  defpred P[set,set] means for s being Element of NAT,q being FinSequence of
  REAL st s=$1 & q=$2 holds len q=n & q*A=Base_FinSeq(n,s);
  assume
A1: for y being FinSequence of REAL st len y=n holds ex x being
  FinSequence of REAL st len x=n & x*A=y;
A2: for i holds ex x being FinSequence of REAL st len x=n & x*A=Base_FinSeq(
  n,i)
  proof
    let i;
    len Base_FinSeq(n,i)=n by Th74;
    hence thesis by A1;
  end;
A3: for j being Nat st j in Seg n ex d being Element of REAL* st P[j,d]
  proof
    let j be Nat;
    assume j in Seg n;
    consider x being FinSequence of REAL such that
A4: len x=n & x*A=Base_FinSeq(n,j) by A2;
    reconsider d0=x as Element of REAL* by FINSEQ_1:def 11;
    for s being Element of NAT,q being FinSequence of REAL st s=j & q=d0
    holds len q=n & q*A=Base_FinSeq(n,s) by A4;
    hence thesis;
  end;
  consider f being FinSequence of REAL* such that
A5: len f = n & for j being Nat st j in Seg n holds P[j,(f/.j)] from
  FINSEQ_4:sch 1(A3);
  for x being set st x in rng f ex p being FinSequence of REAL st x = p &
  len p = n
  proof
    let x be set;
    assume x in rng f;
    then consider z being set such that
A6: z in dom f and
A7: f.z=x by FUNCT_1:def 3;
    reconsider j0=z as Element of NAT by A6;
    reconsider q0=f/.j0 as FinSequence of REAL by FINSEQ_1:def 11;
    z in Seg len f by A6,FINSEQ_1:def 3;
    then
A8: len q0=n by A5;
    q0=x by A6,A7,PARTFUN1:def 6;
    hence thesis by A8;
  end;
  then reconsider M=f as Matrix of REAL by MATRIX_1:9;
  for p being FinSequence of REAL st p in rng M holds len p = n
  proof
    let p be FinSequence of REAL;
    assume p in rng M;
    then consider z being set such that
A9: z in dom f and
A10: M.z=p by FUNCT_1:def 3;
    reconsider j0=z as Element of NAT by A9;
    reconsider q0=f/.j0 as FinSequence of REAL by FINSEQ_1:def 11;
    z in Seg len f & q0=p by A9,A10,FINSEQ_1:def 3,PARTFUN1:def 6;
    hence thesis by A5;
  end;
  then reconsider B=M as Matrix of n,REAL by A5,MATRIX_1:def 2;
  for i4,j4 being Nat st [i4,j4] in Indices (B*A) holds (B*A)*(i4,j4)=
  1_Rmatrix(n)*(i4,j4)
  proof
    let i4,j4 be Nat;
    reconsider i=i4,j=j4 as Element of NAT by ORDINAL1:def 12;
    consider n2 being Nat such that
A11: for x being set st x in rng (M*A) ex p being FinSequence of REAL
    st x = p & len p = n2 by MATRIX_1:9;
    assume
A12: [i4,j4] in Indices (B*A);
    then j in Seg width (M*A) by ZFMISC_1:87;
    then
A13: 1<=j & j<=width (M*A) by FINSEQ_1:1;
    i in dom (M*A) by A12,ZFMISC_1:87;
    then
A14: (M*A).i in rng (M*A) by FUNCT_1:def 3;
    then consider p2 being FinSequence of REAL such that
A15: (M*A).i = p2 and
A16: len p2 = n2 by A11;
A17: len B=n by MATRIX_1:24;
A18: [i,j] in [:Seg n,Seg n:] by A12,MATRIX_1:24;
    then [i,j] in Indices (1_Rmatrix(n)) by MATRIX_1:24;
    then
A19: ex p3 being FinSequence of REAL st p3 = (1_Rmatrix(n)).i & 1_Rmatrix(n
    )*(i,j) = p3.j by MATRIX_1:def 5;
A20: width (B*A)=n by MATRIX_1:24;
    j in Seg n by A18,ZFMISC_1:87;
    then
A21: 1<=j & j<=n by FINSEQ_1:1;
A22: i in Seg n by A18,ZFMISC_1:87;
    then
A23: 1<=i & i<=n by FINSEQ_1:1;
A24: len (B*A) = n & for p being FinSequence of REAL st p in rng (B*A)
    holds len p = n by MATRIX_1:def 2;
    now
      per cases;
      case
A25:    i=j;
        reconsider g=f/.i as FinSequence of REAL by FINSEQ_1:def 11;
A26:    g*A=Base_FinSeq(n,i) by A5,A22;
        len B=n by MATRIX_1:24;
        then f/.i=M.i by A23,FINSEQ_4:15;
        then
A27:    g=Line(B,i) by A23,A17,Lm2;
A28:    1_Rmatrix(n)*(i,j)=(Base_FinSeq(n,i)).i by A19,A23,A25,Th78
          .=1 by A23,Th75;
        p2.j=(B*A)*(i,j) by A24,A14,A15,A16,A13,A23,A20,Th2
          .=(Base_FinSeq(n,i)).j by A12,A26,A27,Th61
          .=1 by A23,A25,Th75;
        hence 1_Rmatrix(n)*(i,j) = p2.j by A28;
      end;
      case
A29:    i<>j;
        reconsider g=f/.i as FinSequence of REAL by FINSEQ_1:def 11;
        len B=n by MATRIX_1:24;
        then f/.i=M.i by A23,FINSEQ_4:15;
        then g=Line(B,i) by A23,A17,Lm2;
        then
A30:    (Line(B,i))*A=Base_FinSeq(n,i) by A5,A22;
A31:    1_Rmatrix(n)*(i,j)=(Base_FinSeq(n,i)).j by A19,A23,Th78
          .=0 by A21,A29,Th76;
        p2.j=(B*A)*(i,j) by A24,A14,A15,A16,A13,A23,A20,Th2
          .=(Base_FinSeq(n,i)).j by A12,A30,Th61
          .=0 by A21,A29,Th76;
        hence 1_Rmatrix(n)*(i,j) = p2.j by A31;
      end;
    end;
    hence thesis by A12,A15,MATRIX_1:def 5;
  end;
  hence thesis by MATRIX_1:27;
end;

theorem
  for x being FinSequence of REAL, A being Matrix of n,REAL st n>0 & len
  x=n holds (A@)*x = x*A
proof
  let x be FinSequence of REAL,A be Matrix of n,REAL;
A1: len A=n & width A=n by MATRIX_1:24;
  assume n>0 & len x=n;
  hence thesis by A1,MATRIXR1:52;
end;

theorem Th95:
  for x being FinSequence of REAL, A being Matrix of n,REAL st n>0
  & len x=n holds x*(A@) = A*x
proof
  let x be FinSequence of REAL,A be Matrix of n,REAL;
A1: len A=n & width A=n by MATRIX_1:24;
  assume n>0 & len x=n;
  hence thesis by A1,MATRIXR1:53;
end;

theorem Th96:
  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
  let A be Matrix of n,REAL;
  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;
  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;
    assume len y=n;
    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 thesis by A3,A4;
  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 thesis;
end;

theorem
  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
  let A be Matrix of n,REAL;
  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;
  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;
    assume len y=n;
    then ex x1,x2 being FinSequence of REAL st len x1=n & len x2= n & A*x1=y &
    x2*A=y by A2;
    hence thesis;
  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;
    assume len y=n;
    then ex x1,x2 being FinSequence of REAL st len x1=n & len x2= n & A*x1=y &
    x2*A=y by A2;
    hence thesis;
  end;
  then ex B2 being Matrix of n,REAL st A*B2=1_Rmatrix(n) by A1,Th96;
  hence thesis by A3,Th80;
end;