MATGRP_0

:: General Linear Group over Arbitrary Rings
::  by Alexander M. Nelson
:: 
:: Received June 18, 2026
:: Copyright (c) 2026 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 4.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/4.0/.

environ

 vocabularies SETWISEO, RVSUM_1, FVSUM_1, INCSP_1, QC_LANG1, MSSUBFAM, ARYTM_3,
      FUNCT_1, FUNCT_2, RELAT_1, RLVECT_1, VECTSP_1, VECTSP_2, ALGSTR_0,
      XBOOLE_0, TARSKI, STRUCT_0, SUBSET_1, SUPINF_2, NAT_1, MESFUNC1, FDIFF_1,
      QUOFIELD, C0SP1, ORDINAL4, RING_3, MOD_4, GROUP_1, GROUP_2, GROUP_5,
      ARYTM_1, FINSEQ_1, FINSEQ_2, FINSEQOP, BINOP_1, LATTICES, CARD_1, CARD_3,
      NUMBERS, REALSET1, ZFMISC_1, FUNCSDOM, XXREAL_0, TREES_1, WELLORD1,
      MATRIX_1, MATRIX_6, GROUP_6, UNIROOTS, MATGRP_0;
 notations NUMBERS, TARSKI, SETWISEO, XBOOLE_0, ZFMISC_1, SUBSET_1, DOMAIN_1,
      FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, REALSET1, FINSEQ_1,
      FINSEQ_2, FINSEQOP, ORDINAL1, XCMPLX_0, XXREAL_0, VECTSP_1, STRUCT_0,
      ALGSTR_0, RINGCAT1, MOD_4, QUOFIELD, C0SP1, GROUP_1, RLVECT_1, GCD_1,
      GROUP_5, WEDDWITT, GROUP_6, GROUP_2, RING_3, MATRIX_0, FVSUM_1, MATRIX_3,
      MATRIX_1, MATRIX_6, UNIROOTS;
 constructors SETWISEO, RELSET_1, GCD_1, MATRLIN2, RING_3, RINGCAT1, GROUP_5,
      WEDDWITT, REALSET1, FVSUM_1, MATRIX_6, UNIROOTS, FINSEQOP, MATRIX_1,
      MATRIX_3;
 registrations XBOOLE_0, ORDINAL1, RELSET_1, XREAL_0, NAT_1, FINSEQ_1,
      FINSEQ_2, STRUCT_0, VECTSP_1, ALGSTR_1, SUBSET_1, RELAT_1, ALGSTR_0,
      RLVECT_1, REALSET1, XXREAL_0, FUNCT_1, CARD_1, GR_CY_1, GROUP_2,
      WEDDWITT, RING_2, MATRIX_0, MATRIX_1, MATRIX_6, MOD_4, FUNCT_2, RINGCAT1,
      MATRIX_3;
 requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM;
 equalities BINOP_1, REALSET1, STRUCT_0, ALGSTR_0, MATRIX_1, MATRIX_3;
 definitions MATRIX_1;
 expansions MATRIX_1;
 theorems XXREAL_0, FVSUM_1, XBOOLE_1, XTUPLE_0, CARD_1, STRUCT_0, FIELD_6,
      LIOUVIL2, SETWISEO, ALGSTR_0, GROUP_1, VECTSP_1, VECTSP_2, RLVECT_1,
      GCD_1, TARSKI, RELAT_1, FUNCT_1, FUNCT_2, REALSET1, ZFMISC_1, XBOOLE_0,
      FINSEQ_1, FINSEQ_2, FINSEQOP, MATRIX_0, MATRIX_1, MATRIX_3, MATRIX_4,
      MATRIX_6, RING_3, QUOFIELD, C0SP1, WEDDWITT, BINOP_1, GROUP_2, GROUP_5,
      GROUP_6, NAT_1, MATRIXR2, UNIROOTS;
 schemes BINOP_1, MATRIX_0, FUNCT_2, NAT_1;

begin :: Results about Ring Morphisms

:: Dedicated in loving memory of Kent Woodward

 reserve R for Ring;
 reserve L for associative right_unital non empty multLoopStr;
 reserve n for Nat;
 reserve S for Subring of R;

theorem Th1:
  for R1,R2 being Ring
  for phi being Function of R1,R2 st phi is linear
  holds phi.(1.R1) = 1.R2
proof
  let R1,R2 be Ring;
  let phi be Function of R1,R2;
  assume A1: phi is linear;
  thus phi.(1.R1) = phi.(1_R1)
                 .= 1_R2 by A1,GROUP_1:def 13
                 .= 1.R2;
end;

theorem
  for R1,R2 being Ring
  st R1,R2 are_isomorphic
  holds R2 is R1-isomorphic & R1 is R2-isomorphic
proof
  let R1,R2 be Ring;
  assume R1,R2 are_isomorphic;
  then consider f being Function of R1,R2 such that
  A1: f is RingIsomorphism by QUOFIELD:def 23;
  thus R2 is R1-isomorphic by A1,RING_3:def 4;
  hence R1 is R2-isomorphic by RING_3:74;
end;

theorem
  for R1,R2 being Ring
  for phi being Function of R1,R2 st phi is isomorphism
  for psi being Function of R2,R1 st psi = phi"
  holds psi is bijective
proof
  let R1,R2 be Ring;
  let phi be Function of R1,R2;
  assume A1: phi is isomorphism;
  let psi be Function of R2,R1;
  assume A2: psi = phi";
  then psi * phi = id (dom phi) by A1,FUNCT_1:39
                .= id (the carrier of R1) by FUNCT_2:def 1;
  then phi is one-to-one & psi is onto by FUNCT_2:23;
  hence psi is bijective by A2;
end;

theorem Th11:
  for R1,R2 being Ring
  for phi being Function of R1,R2 st phi is isomorphism
  for x being Element of R1 st phi.x = 1.R2
  holds x = 1.R1
proof
  let R1,R2 be Ring;
  let phi be Function of R1,R2;
  assume A1: phi is isomorphism;
  let x be Element of R1;
  assume A2: phi.x = 1.R2;
  x in the carrier of R1 & dom phi = the carrier of R1 by FUNCT_2:def 1;
  then A4: for x2 being object st x2 in dom phi & phi.x = phi.x2
  holds x2 = x by A1,FUNCT_1:def 4;
  1.R1 in the carrier of R1 & dom phi = the carrier of R1 by FUNCT_2:def 1;
  then A5: 1.R1 in dom phi;
  phi.(1.R1) = phi.x by A1,A2,Th1;
  hence x = 1.R1 by A4,A5;
end;

begin :: Centers of Groups and Rings

theorem Th12:
  for G1,G2 being Group
  st G1,G2 are_isomorphic
  holds center G1, center G2 are_isomorphic
proof
  let G1,G2 be Group;
  assume G1,G2 are_isomorphic;
  then consider phi being Homomorphism of G1,G2 such that
  A1: phi is bijective by GROUP_6:def 11;
  ex psi being Homomorphism of center G1,center G2 st psi is
  bijective
  proof
    set U1 = the carrier of center G1;
    set U2 = the carrier of center G2;
    A2: phi | U1 is one-to-one by A1,FUNCT_1:52;
    U1 c= the carrier of G1 by GROUP_2:def 5;
    then phi | U1 is Function of U1, G2 by FUNCT_2:32;
    then A3: dom (phi | U1) = U1 by FUNCT_2:def 1;
    A4: rng(phi | U1) = U2
    proof
      now
        let y be object;
        assume A5: y in rng(phi | U1);
        then reconsider y9 = y as Element of G2;
        consider x being object such that
        A6: x in dom (phi | U1) & y = (phi | U1).x
        by A5,FUNCT_1:def 3;
        reconsider x9 = x as Element of G1 by A6;
        for z9 being Element of G2 holds z9 * y9 = y9 * z9
        proof
          let z9 be Element of G2;
          rng phi = the carrier of G2 by A1,FUNCT_2:def 3;
          then consider w being object such that
          A7: w in dom phi & z9 = phi.w by FUNCT_1:def 3;
          reconsider w9 = w as Element of G1 by A7;
          A8: y9 = phi.x9 & z9 = phi.w9 by A3,A6,A7,FUNCT_1:49;
          hence z9 * y9 = phi.(w9 * x9) by GROUP_6:def 6
                      .= phi.(x9 * w9) by A3,A6,GROUP_5:77,STRUCT_0:def 5
                      .= y9 * z9 by A8,GROUP_6:def 6;
        end;
        hence y in U2 by GROUP_5:77,STRUCT_0:def 5;
      end;
      then A9: rng(phi | U1) c= U2 by TARSKI:def 3;
      now
        let y be object;
        assume A10: y in U2;
        A11: rng phi = the carrier of G2 by A1,FUNCT_2:def 3;
        y in center G2 by A10,STRUCT_0:def 5;
        then reconsider y9 = y as Element of G2 by GROUP_2:40,STRUCT_0:def 5;
        y = y9 & y9 in the carrier of G2;
        then consider x being object such that
        A12: x in dom phi & y = phi.x
        by A11,FUNCT_1:def 3;
        reconsider x9 = x as Element of G1 by A12;
        A13: phi is one-to-one by A1;
        A14: phi.x9 in center G2 by A10,A12,STRUCT_0:def 5;
        for w9 being Element of G1 holds x9 * w9 = w9 * x9
        proof
          let w9 be Element of G1;
          A15: dom phi = the carrier of G1 by FUNCT_2:def 1;
          hence x9 * w9 = (phi").(phi.(x9 * w9)) by A13,FUNCT_1:34
                      .= (phi").((phi.x9) * (phi.w9)) by GROUP_6:def 6
                      .= (phi").((phi.w9) * (phi.x9)) by A14,GROUP_5:77
                      .= (phi").(phi.(w9 * x9)) by GROUP_6:def 6
                      .= w9 * x9 by A13,A15,FUNCT_1:34;
        end;
        then x9 in U1 by GROUP_5:77,STRUCT_0:def 5;
        hence y in rng(phi | U1) by A12,FUNCT_1:50;
      end;
      then U2 c= rng(phi | U1) by TARSKI:def 3;
      hence rng(phi | U1) = U2 by A9,XBOOLE_0:def 10;
    end;
    then reconsider psi = phi | U1 as Function of (center G1),(center G2)
    by A3,FUNCT_2:2;

    for a,b being Element of center G1
    holds psi.(a * b) = (psi.a) * (psi.b)
    proof
      let a,b be Element of center G1;
      reconsider x = a, y = b as Element of G1 by GROUP_2:42;
      A16: psi.a = phi.x by FUNCT_1:49;
      A17: psi.b = phi.y by FUNCT_1:49;
      thus psi.(a * b) = phi.(a * b) by FUNCT_1:49
                      .= phi.(x * y) by GROUP_2:43
                      .= (phi.x) * (phi.y) by GROUP_6:def 6
                      .= (psi.a) * (psi.b) by A16,A17,GROUP_2:43;
    end;
    then reconsider psi as Homomorphism of (center G1),(center G2)
    by GROUP_6:def 6;
    take psi;
    psi is onto by A4,FUNCT_2:def 3;
    hence psi is bijective by A2;
  end;
  hence center G1, center G2 are_isomorphic by GROUP_6:def 11;
end;

Lm1:
  for R being Ring
  holds center R is commutative
  & center R is Subring of R
proof
  let R be Ring;
  thus center R is commutative;
  A1: for x being object st x in the carrier of center R
  holds x in the carrier of R
  proof
    let x be object;
    assume x in the carrier of center R;
    then reconsider r=x as Element of center R;
    r is Element of R by WEDDWITT:41;
    hence x in the carrier of R;
  end;
  the addF of center R = (the addF of R) || (the carrier of center R) &
  the multF of center R = (the multF of R) || (the carrier of center R) &
  0.(center R) = 0.R &
  1.(center R) = 1.R by WEDDWITT:def 4;
  hence center R is Subring of R by A1,C0SP1:def 3,TARSKI:def 3;
end;

registration
  let R;
  cluster strict commutative non empty for Subring of R;
  existence
  proof
    reconsider S = center R as Subring of R by Lm1;
    take S;
    thus thesis;
  end;
end;

definition
  let R;
  redefine func center R -> strict commutative non empty Subring of R;  :: redefines center (WEDDWITT, definition)
  coherence by Lm1;
end;

theorem Th13:
  for R being commutative Ring
  for x being object st x in R
  holds x in center R
proof
  let R be commutative Ring;
  let x be object;
  assume x in R;
  then reconsider x9 = x as Element of R by STRUCT_0:def 5;
  for y9 being Element of R
  holds x9 * y9 = y9 * x9;
  hence x in center R by WEDDWITT:17;
end;

theorem Th14:
  for R being commutative Ring
  for x being Element of R
  holds x in center R
proof
  let R be commutative Ring;
  let x be Element of R;
  for y being Element of R
  holds x * y = y * x;
  hence x in center R by WEDDWITT:17;
end;

theorem Th15:
  for R being commutative Ring
  holds the carrier of center R = the carrier of R
proof
  let R be commutative Ring;
  for x being object
  holds x in the carrier of center R iff x in the carrier of R
  proof
    let x be object;
    hereby
      assume A1: x in the carrier of center R;
      the carrier of center R c= the carrier of R by C0SP1:def 3;
      hence x in the carrier of R by A1;
    end;
    assume x in the carrier of R;
    then reconsider x9 = x as Element of R;
    x9 in center R by Th14;
    hence x in the carrier of center R by STRUCT_0:def 5;
  end;
  hence the carrier of center R = the carrier of R by TARSKI:2;
end;

theorem
  for R being strict commutative Ring
  holds center R = R
proof
  let R be strict commutative Ring;
  R is strict Subring of R by LIOUVIL2:18;
  hence center R = R by Th15,FIELD_6:14;
end;

begin :: Some results about matrix operations

theorem Th17:
  for m being Nat
  for A being Matrix of R
  st width (0.(R, m, len A)) = len A
  holds (0.(R, m, len A)) * A = 0.(R, m, width A)
proof
  let m be Nat;
  let A be Matrix of R;
  assume A1: width (0.(R, m, len A)) = len A;
  per cases;
  suppose A2: m > 0;
    set B = (0.(R, m,len A))*A;
    A4: len (0.(R, m,len A)) = m by MATRIX_0:def 2;
    then A5: width (0.(R, m,len A)) = len A by A2,MATRIX_0:20;
    then A6: len ((0.(R, m,len A))*A) = m by A4,MATRIX_3:def 4;
    A7: width ((0.(R, m,len A))*A) = width A by A5,MATRIX_3:def 4;
    (0.(R, m,len A))*A = (0.(R, m,len A) + 0.(R, m,len A))*A by MATRIX_3:4
      .= (0.(R, m,len A))*A + (0.(R, m,len A))*A by A5,MATRIX_4:63;
    then len -((0.(R, m,len A))*A) = len ((0.(R, m,len A))*A)
    & 0.(R, m, width A) = B + B + (-B) by A6,A7,MATRIX_1:def 4,MATRIX_4:2;
    then 0.(R, m,width A) = B + (B - B) by MATRIX_3:3
                         .= (0.(R, m,len A))*A by MATRIX_4:20;
    hence thesis;
  end;
  suppose A8: m = 0;
    set LHS = (0.(R, m, len A)) * A;
    set RHS = 0.(R, m, width A);
    A9: len LHS = len (0.(R, m, len A)) by A1,MATRIX_3:def 4
               .= 0 by A8;
    then {} = Seg len LHS
           .= dom LHS by FINSEQ_1:def 3;
    then {} = [:dom LHS, Seg (width LHS):] by ZFMISC_1:90
           .= Indices LHS by MATRIX_0:def 4;
    then A10: for i,j being Nat st [i,j] in Indices LHS
    holds LHS * (i,j) = 0.(R, m, width A) * (i,j);
    width LHS = 0 & len LHS = 0 &
    len RHS = 0 & width RHS = 0 by A8,A9,MATRIX_0:22,def 3;
    hence (0.(R, m, len A)) * A = 0.(R, m, width A)
    by A10,MATRIX_0:21;
  end;
end;

theorem Th18:
  for n being Nat, R being Ring,A being Matrix of R
  st n = width 0.(R,width A,n)
  holds A*(0.(R,width A,n)) = 0.(R,len A,n)
proof
  let n be Nat, R be Ring,A be Matrix of R;
  assume A1: n = width 0.(R,width A,n);
  set B = A*(0.(R,width A,n));
  per cases;
  suppose A3: width A > 0;
    A4: len (0.(R,width A,n))=width A by MATRIX_0:def 2;
    then A5: len (A*(0.(R,width A,n)))=len A by MATRIX_3:def 4;
    width (0.(R,width A,n))=n by A3,A4,MATRIX_0:20;
    then A7: width (A*(0.(R,width A,n)))=n by A4,MATRIX_3:def 4;
    per cases;
    suppose len A = 0;
      hence thesis by A3,MATRIX_0:def 3;
    end;
    suppose len A > 0;
      then reconsider LHS = A*(0.(R,width A,n)) as Matrix of (len A),n,R
      by A5,A7,MATRIX_0:20;
      A*(0.(R,width A,n))
       = A*(0.(R,width A,n) + 0.(R,width A,n)) by MATRIX_3:4
      .= A*(0.(R,width A,n))+A*(0.(R,width A,n)) by A4,MATRIX_4:62;
      then len -(A*(0.(R,width A,n)))=len (A*(0.(R,width A,n)))
      & 0.(R, len A,n) = B + B + (-B) by A5,A7,MATRIX_1:def 4,MATRIX_4:2;
      then 0.(R,len A,n) = B + (B - B) by MATRIX_3:3
                        .= A * (0.(R,width A,n)) by MATRIX_4:20;
      hence thesis;
    end;
  end;
  suppose A8: width A = 0; then :: degenerate case
    A10: len (0.(R,width A,n)) = 0
    & width (0.(R,width A,n)) = 0 by MATRIX_0:22;
    set LHS = A*(0.(R,width A,n));
    set RHS = (0.(R,len A,n));
    A11: len LHS = len A & width LHS = width (0.(R,width A,n))
      by A8,A10,MATRIX_3:def 4;
    then Seg width LHS = {} by A10;
    then {} = [:dom LHS, Seg width LHS:] by ZFMISC_1:90
           .= Indices LHS by MATRIX_0:def 4;
    then A12: for i,j being Nat st [i,j] in Indices LHS
      holds LHS * (i,j) = RHS * (i,j);
    len (0.(R, width A, n)) = width A by A8;
    then A15: len LHS = len A & width LHS = width (0.(R,width A,n))
      by MATRIX_3:def 4;
    per cases;
    suppose len A = 0; then
      len LHS = len RHS & width LHS = width RHS
        by A10,A11,MATRIX_0:22;
      hence thesis by A12,MATRIX_0:21;
    end;
    suppose len A > 0; then
      len LHS = len RHS & width LHS = width RHS
        by A1,A15,MATRIX_0:23;
      hence thesis by A12,MATRIX_0:21;
    end;
  end;
end;

theorem Th19:
  for i,k,m,n being Nat
  for A being Matrix of m,n,R
  st i in dom 0.(R,m)
  holds Line(0.(R,m), i) "*" Col(A, k) = 0.R
proof
  let i,k,m,n be Nat;
  let A be Matrix of m,n,R;
  assume A1: i in dom 0.(R,m);
  set p = mlt(Line(0.(R,m), i), Col(A, k));
  A2: for i9 being Element of NAT st i9 in dom p holds p.i9 = 0.R
  proof
    let i9 be Element of NAT;
    assume A3: i9 in dom p;
    A4: len Line(0.(R,m), i) = width 0.(R,m) by MATRIX_0:def 7
                            .= m by MATRIX_0:24
                            .= len A by MATRIX_0:25
                            .= len Col(A, k) by MATRIX_0:def 8;
    A5: Line(0.(R,m), i).i9 = 0.R
    proof
      i9 in Seg len p by A3,FINSEQ_1:def 3;
      then i9 in Seg(min(len Line(0.(R,m), i), len Col(A, k)))
      by MATRIX_3:13;
      then A6: i9 in Seg(width 0.(R,m)) by A4,MATRIX_0:def 7;
      then [i,i9] in [:dom 0.(R,m),Seg(width 0.(R,m)):] by A1,ZFMISC_1:87;
      then A7: [i,i9] in Indices 0.(R,m) by MATRIX_0:def 4;
      thus Line(0.(R,m), i).i9 = 0.(R,m) * (i, i9) by A6,MATRIX_0:def 7
                              .= 0.R by A7,MATRIX_1:1;
    end;
    i9 in dom A
    proof
      i9 in Seg len p by A3,FINSEQ_1:def 3;
      then i9 in Seg(min(len Line(0.(R,m), i), len Col(A, k)))
      by MATRIX_3:13;
      hence thesis by A4,FINSEQ_1:def 3,MATRIX_0:def 8;
    end;
    then A8: Col(A,k).i9 = A * (i9,k) by MATRIX_0:def 8;
    reconsider a1 = Line(0.(R,m), i).i9, a2 = Col(A,k).i9
    as Element of R by A5,A8;
    thus p.i9 = a1 * a2 by A3,FVSUM_1:60
             .= 0.R by A5;
  end;

  thus Line(0.(R,m), i) "*" Col(A, k) = Sum(p) by FVSUM_1:def 9
                                     .= 0.R by A2,MATRIX_3:35;
end;

theorem Th20:
  for i,k,m,n being Nat
  for A being Matrix of m,n,R
  st k in dom 0.(R,n)
  holds Line(A, i) "*" Col(0.(R,n), k) = 0.R
proof
  let i,k,m,n be Nat;
  let A be Matrix of m,n,R;
  assume A1: k in dom 0.(R,n);
  set p = mlt(Line(A,i), Col(0.(R,n), k));
  A2: for i9 being Element of NAT st i9 in dom p holds p.i9 = 0.R
  proof
    let i9 be Element of NAT;
    assume A3: i9 in dom p;
    per cases;
    suppose A4: m > 0;
      A5: len Line(A, i) = width A by MATRIX_0:def 7
                        .= n by A4,MATRIX_0:23
                        .= len 0.(R,n) by MATRIX_0:25
                        .= len Col(0.(R,n), k) by MATRIX_0:def 8;
      A6: i9 in Seg width A
      proof
        i9 in Seg len p by A3,FINSEQ_1:def 3;
        then i9 in Seg(min(len Line(A,i), len Col(0.(R,n), k)))
        by MATRIX_3:13;
        hence i9 in Seg(width A) by A5,MATRIX_0:def 7;
      end;
      then A7: Line(A,i).i9 = A * (i,i9) by MATRIX_0:def 7;
      A8: Col(0.(R,n), k).i9 = 0.R
      proof
        width A = n by A4,MATRIX_0:23;
        then i9 in Seg (len 0.(R,n)) by A6,MATRIX_0:24;
        then A9: i9 in dom 0.(R,n) by FINSEQ_1:def 3;
        A10: width 0.(R,n) = n & len 0.(R,n) = n by MATRIX_0:24;
        k in Seg (len 0.(R,n)) by A1,FINSEQ_1:def 3;
        then [i9,k] in [:dom 0.(R,n),Seg(width 0.(R,n)):]
        by A9,A10,ZFMISC_1:87;
        then A11: [i9,k] in Indices 0.(R,n) by MATRIX_0:def 4;
        Col(0.(R,n), k).i9 = (0.(R,n)) * (i9,k) by A9,MATRIX_0:def 8;
        hence thesis by A11,MATRIX_1:1;
      end;

      reconsider a2 = Col(0.(R,n), k).i9, a1 = Line(A,i).i9
      as Element of R by A8,A7;
      thus p.i9 = a1 * a2 by A3,FVSUM_1:60
               .= 0.R by A8;
    end;
    suppose m = 0;
      then width A = 0 by MATRIX_0:22;
      then A12: len Line(A,i) = 0;
      i9 in Seg len p by A3,FINSEQ_1:def 3;
      then i9 in Seg(min(len Line(A,i), len Col(0.(R,n), k))) by MATRIX_3:13;
      then i9 in Seg 0 by A12,XXREAL_0:def 9;
      hence thesis;
    end;
  end;
  thus Line(A, i) "*" Col(0.(R,n), k) = Sum(p) by FVSUM_1:def 9
                                     .= 0.R by A2,MATRIX_3:35;
end;

theorem Th21:
  for i,k,m,n being Nat
  for A being Matrix of m,n,R
  st i in dom 1.(R,m) & i in dom A
  holds Line(1.(R,m),i) "*" Col(A,k) = A * (i,k)
proof
  let i,k,m,n be Nat;
  let A be Matrix of m,n,R;
  assume A1: i in dom 1.(R,m);
  assume A2: i in dom A;
  set p = Line(1.(R,m),i);
  set q = Col(A,k);
  A3: i in dom p & i in dom q & p . i = 1.R &
  (for k being Nat st k in dom p & k <> i holds p.k = 0. R)
  proof
    A4: dom p = Seg len p by FINSEQ_1:def 3
             .= Seg (width 1.(R,m)) by MATRIX_0:def 7
             .= Seg m by MATRIX_0:24;
    i in Seg (len 1.(R,m)) by A1,FINSEQ_1:def 3;
    then A5: i in Seg m by MATRIX_0:24;
    hence i in dom p by A4;
    dom q = Seg len q by FINSEQ_1:def 3
         .= dom A by FINSEQ_1:def 3,MATRIX_0:def 8;
    hence i in dom q by A2;
    A6: i in Seg (width 1.(R,m)) by A5,MATRIX_0:24;
    A7: [i,i] in Indices 1.(R,m)
    proof
      [i,i] in [:dom 1.(R,m),Seg(width 1.(R,m)):] by A1,A6,ZFMISC_1:87;
      hence thesis by MATRIX_0:def 4;
    end;
    thus p.i = 1.(R,m) * (i,i) by A6,MATRIX_0:def 7
            .= 1.R by A7,MATRIX_1:def 3;
    let k be Nat;
    assume A8: k in dom p;
    assume A9: k <> i;
    A10: k in Seg (width 1.(R,m)) by A4,A8,MATRIX_0:24;
    then [i,k] in [:dom 1.(R,m), Seg(width 1.(R,m)):] by A1,ZFMISC_1:87;
    then A11: [i,k] in Indices 1.(R,m) by MATRIX_0:def 4;
    thus p.k = 1.(R,m) * (i,k) by A10,MATRIX_0:def 7
            .= 0. R by A9,A11,MATRIX_1:def 3;
  end;
  thus Line(1.(R,m),i) "*" Col(A,k)
   = Sum(mlt(Line(1.(R,m),i), Col(A,k))) by FVSUM_1:def 9
  .= Col(A,k).i by A3,MATRIX_3:17
  .= A * (i,k) by A2,MATRIX_0:def 8;
end;

theorem Th23:
  for i,k,m,n being Nat
  for A being Matrix of m,n,R
  st k in dom A & k in dom 1.(R,n)
  holds Line(A,i) "*" Col(1.(R,n),k) = A * (i,k)
proof
  let i,k,m,n be Nat;
  let A be Matrix of m,n,R;
  assume A1: k in dom A;
  assume A2: k in dom 1.(R,n);
  per cases;
  suppose A3: m > 0;
    set p = Line(A,i), q = Col(1.(R,n), k);
    dom p = Seg len p by FINSEQ_1:def 3
             .= Seg width A by MATRIX_0:def 7;
    then A4: dom p = Seg n by A3,MATRIX_0:23;
    dom 1.(R,n) = Seg (len 1.(R,n)) by FINSEQ_1:def 3
               .= Seg n by MATRIX_0:24;
    then A5: k in dom p by A2,A4;
    dom 1.(R,n) = Seg (len Col(1.(R,n), k)) by FINSEQ_1:def 3,MATRIX_0:def 8
               .= dom Col(1.(R,n), k) by FINSEQ_1:def 3;
    then A6: k in dom q by A2;
    A7: q.k = 1.R
    proof
      dom 1.(R,n) = Seg (len 1.(R,n)) by FINSEQ_1:def 3
                 .= Seg n by MATRIX_0:24;
      then [k,k] in [:Seg n,Seg n:] by A2,ZFMISC_1:87;
      then A8: [k,k] in Indices 1.(R,n) by MATRIX_0:24;
      thus q.k = (1.(R,n)) * (k,k) by A2,MATRIX_0:def 8
              .= 1.R by A8,MATRIX_1:def 3;
    end;
    A9: for k9 being Nat st k9 in dom q & k9 <> k holds q.k9 = 0.R
    proof
      let k9 be Nat;
      assume A10: k9 in dom q;
      assume A11: k9 <> k;
      A12: dom 1.(R,n) = Seg (len 1.(R,n)) by FINSEQ_1:def 3
                      .= Seg n by MATRIX_0:24;
      A13: dom q = Seg len q by FINSEQ_1:def 3
                .= Seg len 1.(R,n) by MATRIX_0:def 8
                .= Seg n by MATRIX_0:24;
      [k9,k] in [:Seg n,Seg n:] by A2,A10,A12,A13,ZFMISC_1:87;
      then [k9,k] in Indices 1.(R,n) by MATRIX_0:24;
      hence 0.R = (1.(R,n)) * (k9,k) by A11,MATRIX_1:def 3
               .= q.k9 by A10,A12,A13,MATRIX_0:def 8;
    end;
    k in Seg width A by A3,A4,A5,MATRIX_0:23;
    then A14: p.k = A * (i,k) by MATRIX_0:def 7;
    thus Line(A,i) "*" Col(1.(R,n),k)
     = Sum(mlt(Line(A,i), Col(1.(R,n),k))) by FVSUM_1:def 9
    .= A * (i,k) by A5,A6,A7,A9,A14,MATRIX_3:17;
  end;
  suppose m = 0; :: degenerate case
    then Seg 0 = Seg len A by MATRIX_0:25
              .= dom A by FINSEQ_1:def 3;
    hence thesis by A1;
  end;
end;

theorem Th24:
  for k,m being Nat st k = 0 implies m = 0
  for r being Element of R
  for A being Matrix of k,m,R
  for B being Matrix of m,n,R
  holds A*(r*B) = (A*r)*B
proof
  let k,m be Nat;
  assume A1: k = 0 implies m = 0;
  let r be Element of R;
  let A be Matrix of k,m,R;
  let B be Matrix of m,n,R;
  set LHS = A*(r*B), RHS = (A*r)*B;
  per cases;
  suppose A2: k = 0; :: degenerate case
    then A3: len A = 0 by MATRIX_0:25;
    width (A*r) = width A by MATRIX_3:def 6
               .= 0 by A3,MATRIX_0:def 3
               .= len B by A1,A2,MATRIX_0:25;
    then A4: len RHS = len (A * r) by MATRIX_3:def 4
                    .= 0 by A2,MATRIX_0:25;
    width A = 0 by A3,MATRIX_0:def 3
           .= len (r * B) by A1,A2,MATRIX_0:25;
    then len LHS = len A by MATRIX_3:def 4
                .= 0 by A2,MATRIX_0:25;
    hence LHS = {}
             .= RHS by A4;
  end;
  suppose A5: k > 0; :: textbook case
    A6: width A = len (r*B) & width(A*r) = len B
    proof
      thus width A = m by A5,MATRIX_0:23
                  .= len (r*B) by MATRIX_0:25;
      thus width(A*r) = m by A5,MATRIX_0:23
                     .= len B by MATRIX_0:25;
    end;
    A7: len LHS = len RHS & width LHS = width RHS
    proof
      thus len LHS = len A by A6,MATRIX_3:def 4
                  .= len (A*r) by MATRIX_3:def 6
                  .= len RHS by A6,MATRIX_3:def 4;
      thus width LHS = width(r*B) by A6,MATRIX_3:def 4
                    .= width B by MATRIX_3:def 5
                    .= width RHS by A6,MATRIX_3:def 4;
    end;
    for i,j being Nat st [i,j] in Indices LHS
    holds LHS * (i,j) = RHS * (i,j)
    proof
      let i,j be Nat;
      assume A8: [i,j] in Indices LHS;
      A9: [i,j] in Indices RHS
      proof
        Indices LHS = [:dom LHS,Seg width LHS:] by MATRIX_0:def 4
                   .= [:Seg len LHS,Seg width LHS:] by FINSEQ_1:def 3
                   .= [:dom RHS,Seg width RHS:] by A7,FINSEQ_1:def 3
                   .= Indices RHS by MATRIX_0:def 4;
        hence thesis by A8;
      end;
      A10: mlt(Line(A,i),Col(r*B,j)) = mlt(Line(A*r,i),Col(B,j))
      proof
        set a1 = Line(A,i), b1 = Col(r*B,j);
        set a2 = Line(A*r,i), b2 = Col(B,j);
        mlt(a1,b1) = (the multF of R) .: (a1,b1) by FVSUM_1:def 7;
        then len mlt(a1,b1) = min(len a1, len b1) by FINSEQ_2:71
                           .= min(width A, len b1) by MATRIX_0:def 7
                           .= min(len(r*B),len(r*B)) by A6,MATRIX_0:def 8
                           .= len B by MATRIX_3:def 5;
        then A11: Seg len B = dom(mlt(a1,b1)) by FINSEQ_1:def 3;
        mlt(a2,b2) = (the multF of R) .: (a2,b2) by FVSUM_1:def 7;
        then len mlt(a2,b2) = min(len a2, len b2) by FINSEQ_2:71
                           .= min(width(A*r), len b2) by MATRIX_0:def 7
                           .= min(width(A*r), len B) by MATRIX_0:def 8
                           .= len B by A6;
        then A12: dom(mlt(Line(A,i),Col(r*B,j)))
        = dom(mlt(Line(A*r,i),Col(B,j))) by A11,FINSEQ_1:def 3;
        for i9 being Nat st i9 in dom(mlt(Line(A,i),Col(r*B,j)))
        holds mlt(Line(A,i),Col(r*B,j)).i9 = mlt(Line(A*r,i),Col(B,j)).i9
        proof
          let i9 be Nat;
          assume A13: i9 in dom(mlt(Line(A,i),Col(r*B,j)));
          then A14: i9 in Seg width (A*r) & i9 in Seg width A
          by A6,A11,MATRIX_3:def 6;
          then A15: Line(A,i).i9 = A*(i,i9) & Line(A*r,i).i9 = (A*r)*(i,i9)
          by MATRIX_0:def 7;
          A16: [i,i9] in Indices A & [i,i9] in Indices(A*r)
          proof
            [i,j] in [:dom LHS,Seg(width LHS):] by A8,MATRIX_0:def 4;
            then i in dom LHS & j in Seg width LHS by ZFMISC_1:87;
            then i in Seg len LHS by FINSEQ_1:def 3;
            then A17: i in Seg len A by A6,MATRIX_3:def 4;
            then i in dom A by FINSEQ_1:def 3;
            then [i,i9] in [:dom A, Seg width A:] by A14,ZFMISC_1:87;
            hence [i,i9] in Indices A by MATRIX_0:def 4;
            dom(A*r) = Seg len(A*r) by FINSEQ_1:def 3
                    .= Seg len A by MATRIX_3:def 6;
            then [i,i9] in [:dom(A*r),Seg(width(A*r)):] by A14,A17,ZFMISC_1:87;
            hence [i,i9] in Indices(A*r) by MATRIX_0:def 4;
          end;
          consider aa1,aa2 being Element of R such that
          A18: aa1 = A*(i,i9) & aa2 = (A*r)*(i,i9);
          A19: i9 in dom B & i9 in dom (r*B)
          proof
            thus i9 in dom B by A11,A13,FINSEQ_1:def 3;
            i9 in Seg len(r*B) by A11,A13,MATRIX_3:def 5;
            hence i9 in dom (r*B) by FINSEQ_1:def 3;
          end;
          then A20: Col(r*B,j).i9 = (r*B)*(i9,j) & Col(B,j).i9 = (B)*(i9,j)
          by MATRIX_0:def 8;
          A21: [i9,j] in Indices (r*B) & [i9,j] in Indices B
          proof
            [i,j] in [:dom LHS,Seg(width LHS):] by A8,MATRIX_0:def 4;
            then i in dom LHS & j in Seg(width LHS) by ZFMISC_1:87;
            then A22: j in Seg(width (r*B)) by A6,MATRIX_3:def 4;
            then [i9,j] in [:dom(r*B),Seg(width(r*B)):] by A19,ZFMISC_1:87;
            hence [i9,j] in Indices (r*B) by MATRIX_0:def 4;
            j in Seg(width B) by A22,MATRIX_3:def 5;
            then [i9,j] in [:dom B,Seg(width B):] by A19,ZFMISC_1:87;
            hence [i9,j] in Indices B by MATRIX_0:def 4;
          end;
          consider bb1,bb2 being Element of R such that
          A23: bb1 = (r*B)*(i9,j) & bb2 = B*(i9,j);
          aa1*r = aa2 by A16,A18,MATRIX_3:def 6;
          then A24: aa1*r = aa2 & bb1 = r*bb2 by A21,A23,MATRIX_3:def 5;
          A25: Line(A*r,i).i9 = aa2 & Col(B,j).i9 = bb2 by A15,A18,A20,A23;
          thus mlt(Line(A,i),Col(r*B,j)).i9
           = aa1 * bb1 by A13,A15,A18,A20,A23,FVSUM_1:60
          .= (aa1 * r) * bb2 by A24,GROUP_1:def 3
          .= mlt(Line(A*r,i),Col(B,j)).i9 by A12,A13,A24,A25,FVSUM_1:60;
        end;
        hence mlt(Line(A,i),Col(r*B,j)) = mlt(Line(A*r,i),Col(B,j))
        by A12,FINSEQ_1:13;
      end;
      A26: Line(A,i) "*" Col(r*B,j)
        = Sum(mlt(Line(A,i),Col(r*B,j))) by FVSUM_1:def 9
       .= Line(A*r,i) "*" Col(B,j) by A10,FVSUM_1:def 9;
      thus LHS * (i,j) = Line(A,i) "*" Col(r*B,j) by A6,A8,MATRIX_3:def 4
                      .= RHS * (i,j) by A6,A9,A26,MATRIX_3:def 4;
    end;
    hence A*(r*B) = (A*r)*B by A7,MATRIX_0:21;
  end;
end;

theorem Th26:
  for r1,r2 being Element of R
  for A being Matrix of R
  holds (r1*A)*r2 = r1*(A*r2)
proof
  let r1,r2 be Element of R;
  let A be Matrix of R;
  A1: len ((r1*A)*r2) = len (r1*A) by MATRIX_3:def 6
                     .= len A by MATRIX_3:def 5
                     .= len(A*r2) by MATRIX_3:def 6
                     .= len(r1*(A*r2)) by MATRIX_3:def 5;
  A2: width ((r1*A)*r2) = width (r1*A) by MATRIX_3:def 6
                       .= width A by MATRIX_3:def 5
                       .= width(A*r2) by MATRIX_3:def 6
                       .= width(r1*(A*r2)) by MATRIX_3:def 5;
  for i,j being Nat st [i,j] in Indices ((r1*A)*r2)
  holds ((r1*A)*r2) * (i,j) = (r1*(A*r2)) * (i,j)
  proof
    let i,j be Nat;
    assume A3: [i,j] in Indices ((r1*A)*r2);
    A4: len ((r1*A)*r2) = len (r1*A) by MATRIX_3:def 6
                       .= len A by MATRIX_3:def 5;
    A5: width ((r1*A)*r2) = width (r1*A) by MATRIX_3:def 6
                         .= width A by MATRIX_3:def 5;
    dom ((r1*A)*r2) = Seg len((r1*A)*r2) by FINSEQ_1:def 3
                   .= dom A by A4,FINSEQ_1:def 3;
    then [:dom A,Seg width A:] = Indices((r1*A)*r2) by A5,MATRIX_0:def 4;
    then A6: [i,j] in Indices A by A3,MATRIX_0:def 4;
    A7: [i,j] in Indices (r1*A)
    proof
      A8: dom(r1*A) = Seg len(r1*A) by FINSEQ_1:def 3
                   .= Seg len A by MATRIX_3:def 5
                   .= dom A by FINSEQ_1:def 3;
      [i,j] in [:dom A,Seg width A:] by A6,MATRIX_0:def 4;
      then [i,j] in [:dom(r1*A),Seg(width (r1*A)):] by A8,MATRIX_3:def 5;
      hence [i,j] in Indices (r1*A) by MATRIX_0:def 4;
    end;
    A9: [i,j] in Indices (A * r2)
    proof
      A10: dom(A*r2) = Seg len(A*r2) by FINSEQ_1:def 3
                    .= Seg len A by MATRIX_3:def 6
                    .= dom A by FINSEQ_1:def 3;
      [i,j] in [:dom A,Seg width A:] by A6,MATRIX_0:def 4;
      then [i,j] in [:dom(A*r2),Seg width (A*r2):] by A10,MATRIX_3:def 6;
      hence [i,j] in Indices (A*r2) by MATRIX_0:def 4;
    end;
    thus ((r1*A)*r2) * (i,j) = ((r1 * A)*(i,j)) * r2 by A7,MATRIX_3:def 6
                            .= (r1 * (A * (i,j))) * r2 by A6,MATRIX_3:def 5
                            .= r1 * ((A * (i,j)) * r2) by GROUP_1:def 3
                            .= r1 * ((A * r2) * (i,j)) by A6,MATRIX_3:def 6
                            .= (r1*(A*r2)) * (i,j) by A9,MATRIX_3:def 5;
  end;
  hence (r1*A)*r2 = r1*(A*r2) by A1,A2,MATRIX_0:21;
end;

theorem Th27:
  for r1,r2 being Element of R
  for A being Matrix of R
  holds r1*(r2*A) = (r1*r2)*A
proof
  let r1,r2 be Element of R;
  let A be Matrix of R;
  A1: len(r1*(r2*A)) = len(r2*A) & len(r2*A) = len A &
  len((r1*r2)*A) = len A by MATRIX_3:def 5;
  A2: width(r1*(r2*A)) = width(r2*A) & width(r2*A) = width A &
  width((r1*r2)*A) = width A by MATRIX_3:def 5;
  for i,j being Nat st [i,j] in Indices(r1*(r2*A))
  holds (r1*(r2*A)) * (i,j) = ((r1*r2)*A) * (i,j)
  proof
    let i,j be Nat;
    assume A3: [i,j] in Indices(r1*(r2*A));
    A4: Indices A = [:dom A,Seg width A:] by MATRIX_0:def 4
                 .= [:Seg len A,Seg width A:] by FINSEQ_1:def 3
                 .= [:dom(r2*A),Seg width(r2*A):] by A1,A2,FINSEQ_1:def 3
                 .= Indices(r2*A) by MATRIX_0:def 4;
    A5: Indices A = [:dom A,Seg width A:] by MATRIX_0:def 4
                 .= [:Seg len A,Seg width A:] by FINSEQ_1:def 3
                 .= [:dom (r1*(r2*A)),Seg width((r1*(r2*A))):]
                    by A1,A2,FINSEQ_1:def 3
                 .= Indices((r1*(r2*A))) by MATRIX_0:def 4;
    hence (r1*(r2*A)) * (i,j) = r1 * ((r2*A) * (i,j)) by A3,A4,MATRIX_3:def 5
                             .= r1 * (r2 * (A * (i,j))) by A3,A5,MATRIX_3:def 5
                             .= (r1 * r2) * (A * (i,j)) by GROUP_1:def 3
                             .= ((r1*r2)*A) * (i,j) by A3,A5,MATRIX_3:def 5;
  end;
  hence r1*(r2*A) = (r1*r2)*A by A1,A2,MATRIX_0:21;
end;

:: MATRIX_5:24 generalized and weakened
theorem Th28:
  for r being Element of R
  holds r * 0.(R,n) = 0.(R,n)
proof
  let r be Element of R;
  for i,j being Nat st [i,j] in Indices(0.(R,n))
  holds (r*0.(R,n)) * (i,j) = 0.(R,n) * (i,j)
  proof
    let i,j be Nat;
    assume A1: [i,j] in Indices(0.(R,n));
    hence (r*0.(R,n)) * (i,j) = r * (0.(R,n) * (i,j)) by MATRIX_3:def 5
                             .= r * (0.R) by A1,MATRIX_1:1
                             .= 0.(R,n) * (i,j) by A1,MATRIX_1:1;
  end;
  hence r*0.(R,n) = 0.(R,n) by MATRIX_0:27;
end;

theorem Th29:
  for k,m being Nat st k = 0 implies m = 0
  for r being Element of R
  for A being Matrix of k,m,R
  for B being Matrix of m,n,R
  holds (r*A)*B = r*(A*B)
proof
  let k,m be Nat;
  assume A1: k = 0 implies m = 0;
  let r be Element of R;
  let A be Matrix of k,m,R;
  let B be Matrix of m,n,R;
  set LHS = (r*A)*B, RHS = r*(A*B);
  per cases;
  suppose A2: k = 0; :: degenerate case
    A3: len A = 0 by A2,MATRIX_0:25;
    then A4: width A = 0 by MATRIX_0:def 3;
    A5: len B = 0 by A1,A2,MATRIX_0:25;
    A6: len (r * A) = 0 by A2,MATRIX_0:25;
    then width (r*A) = 0 by MATRIX_0:def 3;
    then A7: len LHS = 0 by A5,A6,MATRIX_3:def 4;
    len RHS = len (A * B) by MATRIX_3:def 5
           .= 0 by A3,A4,A5,MATRIX_3:def 4;
    hence RHS = {}
             .= LHS by A7;
  end;
  suppose A8: k > 0; :: textbook case
    A9: width A = len B & width (r*A) = len B
    proof
      thus width A = m by A8,MATRIX_0:23
                  .= len B by MATRIX_0:25;
      hence len B = width(r*A) by MATRIX_3:def 5;
    end;
    A10: len LHS = len RHS & width LHS = width RHS
    proof
      thus len LHS = len(r*A) by A9,MATRIX_3:def 4
                  .= len A by MATRIX_3:def 5
                  .= len (A * B) by A9,MATRIX_3:def 4
                  .= len RHS by MATRIX_3:def 5;
      thus width LHS = width B by A9,MATRIX_3:def 4
                    .= width(A*B) by A9,MATRIX_3:def 4
                    .= width RHS by MATRIX_3:def 5;
    end;
    for i,j being Nat st [i,j] in Indices LHS
    holds LHS * (i,j) = RHS * (i,j)
    proof
      let i,j be Nat;
      assume A11: [i,j] in Indices LHS;
      A12: [i,j] in Indices RHS
      proof
        Indices LHS = [:dom LHS,Seg width LHS:] by MATRIX_0:def 4
                   .= [:Seg len LHS,Seg width LHS:] by FINSEQ_1:def 3
                   .= [:dom RHS,Seg width RHS:] by A10,FINSEQ_1:def 3
                   .= Indices RHS by MATRIX_0:def 4;
        hence thesis by A11;
      end;
      A13: [i,j] in Indices (A * B)
      proof
        Indices RHS = [:dom RHS,Seg width RHS:] by MATRIX_0:def 4
                   .= [:Seg len (r*(A*B)),Seg width (r*(A*B)):]
                      by FINSEQ_1:def 3
                   .= [:Seg len (A*B),Seg width (r*(A*B)):] by MATRIX_3:def 5
                   .= [:Seg len (A*B),Seg width (A*B):] by MATRIX_3:def 5
                   .= [:dom(A*B),Seg width(A*B):] by FINSEQ_1:def 3
                   .= Indices (A*B) by MATRIX_0:def 4;
        hence thesis by A12;
      end;
      A14: Line(r*A,i) = r*Line(A,i)
      proof
        A15: width (r*A) = width A by MATRIX_3:def 5;
        for j9 being Nat st j9 in Seg width A
        holds Line(r*A,i).j9 = (r*Line(A,i)).j9
        proof
          let j9 be Nat;
          assume A16: j9 in Seg width A;
          [i,j] in [:dom(A*B),Seg width(A*B):] by A13,MATRIX_0:def 4;
          then i in dom(A*B) by ZFMISC_1:87;
          then i in Seg len (A*B) by FINSEQ_1:def 3;
          then i in Seg len A by A9,MATRIX_3:def 4;
          then i in dom A by FINSEQ_1:def 3;
          then [i,j9] in [:dom A,Seg width A:] by A16,ZFMISC_1:87;
          then A17: [i,j9] in Indices A by MATRIX_0:def 4;
          A18: Line(A,i).j9 = A*(i,j9) by A16,MATRIX_0:def 7;
          thus Line(r*A,i).j9 = (r*A) * (i,j9) by A15,A16,MATRIX_0:def 7
                             .= r * (A*(i,j9)) by A17,MATRIX_3:def 5
                             .= (r * Line(A,i)).j9 by A16,A18,FVSUM_1:51;
        end;
        hence Line(r*A,i) = r*Line(A,i) by A15,FINSEQ_2:119;
      end;
      thus LHS * (i,j) = Line(r*A,i) "*" Col(B,j) by A9,A11,MATRIX_3:def 4
                      .= Sum(mlt(Line(r*A,i), Col(B,j))) by FVSUM_1:def 9
                      .= Sum(r*mlt(Line(A,i), Col(B,j))) by A9,A14,FVSUM_1:68
                      .= r*Sum(mlt(Line(A,i), Col(B,j))) by FVSUM_1:73
                      .= r*(Line(A,i) "*" Col(B,j)) by FVSUM_1:def 9
                      .= r*((A*B)*(i,j)) by A9,A13,MATRIX_3:def 4
                      .= RHS * (i,j) by A13,MATRIX_3:def 5;
    end;

    hence (r*A)*B = r*(A*B) by A10,MATRIX_0:21;
  end;
end;

theorem
  for A being Matrix of R
  for r being Element of R
  holds (-r)*A = -(r * A)
proof
  let A be Matrix of R;
  let r be Element of R;
  A1: len ((-r)*A) = len A & len(-(r*A)) = len A & len(r*A) = len A
  proof
    thus len ((-r)*A) = len A by MATRIX_3:def 5;
    thus len(-(r*A)) = len(r*A) by MATRIX_1:def 4
                    .= len A by MATRIX_3:def 5;
    thus len(r*A) = len A by MATRIX_3:def 5;
  end;
  A2: width ((-r)*A) = width A & width(-(r*A)) = width A & width(r*A) = width A
  proof
    thus width ((-r)*A) = width A by MATRIX_3:def 5;
    thus width(-(r*A)) = width(r*A) by MATRIX_1:def 4
                      .= width A by MATRIX_3:def 5;
    thus width((r*A)) = width A by MATRIX_3:def 5;
  end;
  for i,j being Nat st [i,j] in Indices((-r)*A)
  holds ((-r)*A) * (i,j) = (-(r * A))*(i,j)
  proof
    let i,j be Nat;
    assume A3: [i,j] in Indices((-r)*A);
    A4: Indices((-r)*A) = [:dom((-r)*A),Seg width((-r)*A):] by MATRIX_0:def 4
                       .= [:Seg len((-r)*A),Seg width((-r)*A):]
                          by FINSEQ_1:def 3
                       .= [:dom A,Seg width A:] by A1,A2,FINSEQ_1:def 3
                       .= Indices A by MATRIX_0:def 4;
    A5: Indices A = [:dom A,Seg width A:] by MATRIX_0:def 4
                 .= [:Seg len A,Seg width A:] by FINSEQ_1:def 3
                 .= [:dom(r*A),Seg width(r*A):] by A1,A2,FINSEQ_1:def 3
                 .= Indices(r*A) by MATRIX_0:def 4;
    thus ((-r)*A) * (i,j) = (-r)*(A*(i,j)) by A3,A4,MATRIX_3:def 5
                         .= - (r * (A * (i,j))) by VECTSP_1:9
                         .= - ((r * A) * (i,j)) by A3,A4,MATRIX_3:def 5
                         .= (-(r * A))*(i,j) by A3,A4,A5,MATRIX_1:def 4;
  end;

  hence (-r)*A = -(r * A) by A1,A2,MATRIX_0:21;
end;

theorem ::: similar to MATRIX_3:18
  for A being Matrix of R holds (1.R) * A = A;

begin :: Results about 1-by-1 matrices

theorem Th33:
  for D being non empty set
  for M being Matrix of 1,D
  holds M = <* <* (M * (1,1)) *> *>
proof
  let D be non empty set;
  let M be Matrix of 1,D;
  A1: Indices M = [: Seg 1,Seg 1 :] & 1 in Seg 1
  by FINSEQ_1:2,MATRIX_0:24,TARSKI:def 1;
  for i,j being Nat st [i,j] in Indices M
  holds M * (i,j) = (<* <* (M * (1,1)) *> *>) * (i,j)
  proof
    let i,j be Nat;
    assume [i,j] in Indices M;
    then i in Seg 1 & j in Seg 1 by A1,ZFMISC_1:87;
    then i = 1 & j = 1 by FINSEQ_1:2,TARSKI:def 1;
    hence M * (i,j) = (<* <* (M * (1,1)) *> *>) * (i,j)
    by MATRIX_0:49;
  end;
  hence M = <* <* (M * (1,1)) *> *> by MATRIX_0:27;
end;

theorem Th34:
  for L being non empty ZeroOneStr
  holds 1.(L, 1) = <*<* (1.L) *>*>
proof
  let L be non empty ZeroOneStr;
  Indices 1.(L,1) = [:(Seg 1),(Seg 1):] & 1 in Seg 1
  by FINSEQ_1:2,MATRIX_0:24,TARSKI:def 1;
  then [1,1] in Indices 1.(L, 1) by ZFMISC_1:87;
  then (1.(L, 1)) * (1,1) = 1.L by MATRIX_1:def 3;
  hence 1.(L, 1) = <*<* (1.L) *>*> by Th33;
end;

theorem Th35:
  for x,y being Element of R
  for M1,M2 being Matrix of 1,R
  st M1 = <*<* x *>*> & M2 = <*<* y *>*>
  holds M1*M2 = <*<*(x * y)*>*> by MATRIX_3:20;

theorem Th36:
  for x,y being Element of R
  for M1,M2 being Matrix of 1,R
  st M1 = <*<* x *>*> & M2 = <*<* y *>*>
  holds M1 + M2 = <*<*(x + y)*>*>
proof
  let x,y be Element of R;
  let M1,M2 be Matrix of 1,R;
  assume A1: M1 = <*<* x *>*>;
  assume A2: M2 = <*<* y *>*>;
  A3: Indices (M1 + M2) = [:(Seg 1),(Seg 1):] & 1 in Seg 1
  by FINSEQ_1:2,MATRIX_0:24,TARSKI:def 1;
  for i,j being Nat st [i,j] in Indices (M1 + M2)
  holds (M1 + M2) * (i,j) = (<* <* (x + y) *> *>) * (i,j)
  proof
    let i,j be Nat;
    assume A4: [i,j] in Indices (M1 + M2);
    then i in Seg 1 & j in Seg 1 by A3,ZFMISC_1:87;
    then A5: i = 1 & j = 1 by FINSEQ_1:2,TARSKI:def 1;
    [i,j] in Indices M1 by A3,A4,MATRIX_0:24;
    hence (M1 + M2) * (i,j) = (M1 * (i,j)) + (M2 * (i,j)) by MATRIX_1:def 8
                          .= x + ((<*<* y *>*>) * (1,1))
                             by A1,A2,A5,MATRIX_0:49
                          .= x + y by MATRIX_0:49
                          .= (<* <* (x + y) *> *>) * (i,j) by A5,MATRIX_0:49;
  end;
  hence M1 + M2 = <*<*(x + y)*>*> by MATRIX_0:27;
end;

theorem
  for r,s being Element of R
  holds r * <*<* s *>*> = <*<* (r * s) *>*>
  & <*<* s *>*> * r = <*<* (s * r) *>*>
proof
  let r,s be Element of R;
  set M = <*<* s *>*>, M1 = <*<* (r * s) *>*>, M2 = <*<* (s * r) *>*>;
  for i,j being Nat st [i,j] in Indices (r * M)
  holds (r * M) * (i,j) = M1 * (i,j)
  proof
    let i,j be Nat;
    assume A1: [i,j] in Indices (r * M);
    A2: Indices (r * M) = [:(Seg 1),(Seg 1):] by MATRIX_0:24
                       .= Indices M by MATRIX_0:24;
    A3: i = 1 & j = 1
    proof
      [i,j] in [: Seg 1,Seg 1 :] by A1,MATRIX_0:24;
      then i in {1} & j in {1} by FINSEQ_1:2,ZFMISC_1:87;
      hence thesis by TARSKI:def 1;
    end;
    hence (r * M) * (i,j) = r * (M * (1,1)) by A1,A2,MATRIX_3:def 5
                        .= r * s by MATRIX_0:49
                        .= M1 * (i,j) by A3,MATRIX_0:49;
  end;
  hence r * M = M1 by MATRIX_0:27;
  for i,j being Nat st [i,j] in Indices (M * r)
  holds (M * r) * (i,j) = M2 * (i,j)
  proof
    let i,j be Nat;
    assume A4: [i,j] in Indices (M * r);
    A5: Indices (M * r) = [:(Seg 1),(Seg 1):] by MATRIX_0:24
                       .= Indices M by MATRIX_0:24;
    A6: i = 1 & j = 1
    proof
      [i,j] in [: Seg 1,Seg 1 :] by A4,MATRIX_0:24;
      then i in Seg 1 & j in Seg 1 by ZFMISC_1:87;
      hence thesis by FINSEQ_1:2,TARSKI:def 1;
    end;
    thus (M * r) * (i,j) = (M * (i,j)) * r by A4,A5,MATRIX_3:def 6
                        .= s * r by A6,MATRIX_0:49
                        .= M2 * (i,j) by A6,MATRIX_0:49;
  end;
  hence M * r = M2 by MATRIX_0:27;
end;

theorem Th38:
  for Y being Matrix of 1,R
  holds Y = (Y * (1,1)) * 1.(R,1)
proof
  let Y be Matrix of 1,R;
  for i,j being Nat st [i,j] in Indices Y
  holds Y * (i,j) = ((Y * (1,1)) * 1.(R,1)) * (i,j)
  proof
    let i,j be Nat;
    assume A1: [i,j] in Indices Y;
    A2: Indices Y = [:(Seg 1),(Seg 1):] by MATRIX_0:24
                 .= Indices 1.(R,1) by MATRIX_0:24;
    A3: i = 1 & j = 1
    proof
      [i,j] in [:(Seg 1),(Seg 1):] by A1,MATRIX_0:24;
      then i in Seg 1 & j in Seg 1 by ZFMISC_1:87;
      hence thesis by FINSEQ_1:2,TARSKI:def 1;
    end;
    set Y11 = Y * (1,1);
    thus Y * (i,j) = Y11 * (1.R) by A3
                  .= Y11 * (1.(R,1) * (1,1)) by A1,A2,A3,MATRIX_1:def 3
                  .= (Y11 * 1.(R,1)) * (i,j) by A1,A2,A3,MATRIX_3:def 5;
  end;
  hence Y = (Y * (1,1)) * 1.(R,1) by MATRIX_0:27;
end;

begin :: Canonical basis for matrices

::$N Bourbaki, Algebra~\cite{BourbakiAlgI}, II 10.3 defines these as E_{i,j}
definition
  let R be non empty ZeroOneStr;
  let I,K,i,k be Nat;
  func canMat (i,k,I,K,R) -> Matrix of I,K,R means :Def1:
  for i2,k2 being Nat st [i2,k2] in Indices it
  holds ([i,k] = [i2,k2] implies it * (i2,k2) = 1.R)
  & ([i,k] <> [i2,k2] implies it * (i2,k2) = 0.R);
  existence
  proof
    deffunc F() = the carrier of R;
    defpred P[object,object,object] means
    ([i,k] = [$1,$2] implies $3 = 1.R)
    & ([i,k] <>[$1,$2] implies $3 = 0.R);
    A1: for i2,k2 being Nat st [i2,k2] in [:Seg I,Seg K:]
    ex x being Element of F() st P[i2,k2,x]
    proof
      let i2,k2 be Nat;
      assume [i2,k2] in [:(Seg I),(Seg K):];
      per cases;
      suppose A2: [i,k] = [i2,k2];
        take 1.R;
        thus thesis by A2;
      end;
      suppose A3: [i,k] <> [i2,k2];
        take 0.R;
        thus thesis by A3;
      end;
    end;
    consider M being Matrix of I,K,F() such that
    A4: for i2,k2 being Nat st [i2,k2] in Indices M
    holds P[i2,k2,M*(i2,k2)] from MATRIX_0:sch 2(A1);
    take M;
    thus thesis by A4;
  end;
  uniqueness
  proof
    defpred P[Matrix of I,K,R] means
    for i2,k2 being Nat st [i2,k2] in Indices $1
    holds ([i,k] = [i2,k2] implies $1 * (i2,k2) = 1.R)
    & ([i,k] <> [i2,k2] implies $1 * (i2,k2) = 0.R);

    for M1,M2 being Matrix of I,K,R st P[M1] & P[M2]
    holds M1 = M2
    proof
      let M1,M2 be Matrix of I,K,R;
      assume A5: P[M1];
      assume A6: P[M2];
      for i2,k2 being Nat st [i2,k2] in Indices M1
      holds M1 * (i2,k2) = M2 * (i2,k2)
      proof
        let i2,k2 be Nat;
        assume A7: [i2,k2] in Indices M1;
        A8: [i2,k2] in Indices M2
        proof
          per cases;
          suppose I = 0;
            hence thesis by A7,MATRIX_0:22;
          end;
          suppose A9: I > 0;
            then Indices M1 = [:(Seg I),(Seg K):] by MATRIX_0:23
                           .= Indices M2 by A9,MATRIX_0:23;
            hence thesis by A7;
          end;
        end;
        per cases;
        suppose A10: [i,k] = [i2,k2];
          hence M1 * (i2,k2) = 1.R by A5,A7
                            .= M2 * (i2,k2) by A10,A6,A8;
        end;
        suppose A11: [i,k] <> [i2,k2];
          hence M1 * (i2,k2) = 0.R by A5,A7
                            .= M2 * (i2,k2) by A11,A6,A8;
        end;
      end;

      hence M1 = M2 by MATRIX_0:27;
    end;

    hence thesis;
  end;
end;

theorem Th40:
  for I,K,i,k,i2,k2 being Nat
  st [i2,k2] in Indices canMat(i,k,I,K,R)
  holds (i <> i2 implies canMat(i,k,I,K,R) * (i2,k2) = 0.R)
  & (k <> k2 implies canMat(i,k,I,K,R) * (i2,k2) = 0.R)
  & (i = i2 & k = k2 implies canMat(i,k,I,K,R) * (i2,k2) = 1.R)
proof
  let I,K,i,k,i2,k2 be Nat;
  assume A1: [i2,k2] in Indices canMat(i,k,I,K,R);
  thus i <> i2 implies canMat(i,k,I,K,R) * (i2,k2) = 0.R
  proof
    assume i <> i2;
    then [i,k] <> [i2,k2] by XTUPLE_0:1;
    hence canMat(i,k,I,K,R) * (i2,k2) = 0.R by A1,Def1;
  end;
  thus k <> k2 implies canMat(i,k,I,K,R) * (i2,k2) = 0.R
  proof
    assume k <> k2;
    then [i,k] <> [i2,k2] by XTUPLE_0:1;
    hence canMat(i,k,I,K,R) * (i2,k2) = 0.R by A1,Def1;
  end;
  assume i = i2 & k = k2;
  hence canMat(i,k,I,K,R) * (i2,k2) = 1.R by A1,Def1;
end;

theorem Th41:
  for I,K,i,k being Nat st not [i,k] in Indices canMat(i,k,I,K,R)
  holds canMat(i,k,I,K,R) = 0.(R, I, K)
proof
  let I,K,i,k be Nat;
  assume A1: not [i,k] in Indices canMat(i,k,I,K,R);
  for i2,k2 being Nat st [i2,k2] in Indices canMat(i,k,I,K,R)
  holds canMat(i,k,I,K,R) * (i2,k2) = 0.(R, I, K) * (i2,k2)
  proof
    let i2,k2 be Nat;
    assume A2: [i2,k2] in Indices canMat(i,k,I,K,R);
    then A3: [i2,k2] in Indices(0.(R, I, K)) by MATRIX_0:26;
    per cases by A1,A2;
    suppose i <> i2;
      hence canMat(i,k,I,K,R) * (i2,k2)
       = 0.R by A2,Th40
      .= 0.(R, I, K) * (i2,k2) by A3,MATRIX_3:1;
    end;
    suppose k <> k2;
      hence canMat(i,k,I,K,R) * (i2,k2)
       = 0.R by A2,Th40
      .= 0.(R, I, K) * (i2,k2) by A3,MATRIX_3:1;
    end;
  end;
  hence canMat(i,k,I,K,R) = 0.(R, I, K) by MATRIX_0:27;
end;

theorem
  for R being non empty ZeroOneStr
  for I,K being Nat st (I = 0 iff K = 0)
  for i,k being Nat
  holds (canMat(i,k,I,K,R))@ = canMat(k,i,K,I,R)
proof
  let R be non empty ZeroOneStr;
  let I,K be Nat;
  assume A1: I = 0 iff K = 0;
  let i,k be Nat;
  set LHS = (canMat(i,k,I,K,R))@;
  set RHS = canMat(k,i,K,I,R);
  per cases;
  suppose I = 0;
    then A2: LHS is Matrix of 0,R & RHS is Matrix of 0,R by A1;
    then for i2,j2 being Nat st [i2,j2] in Indices LHS
         holds LHS * (i2,j2) = RHS * (i2,j2) by MATRIX_0:22;
    hence LHS = RHS by A2,MATRIX_0:27;
  end;
  suppose A3: I > 0;
    A4: len(canMat(i,k,I,K,R)) = I
    & width(canMat(i,k,I,K,R)) = K
    & Indices(canMat(i,k,I,K,R)) = [:Seg I,Seg K:]
    by A3,MATRIX_0:23;
    then A5: len LHS = K & width LHS = I by A1,A3,MATRIX_0:29;
    A6: len RHS = K & width RHS = I
    & Indices RHS = [:Seg K,Seg I:] by A1,A3,MATRIX_0:23;
    for i2,j2 being Nat st [i2,j2] in Indices LHS
    holds LHS * (i2,j2) = RHS * (i2,j2)
    proof
      let i2,j2 be Nat;
      assume A7: [i2,j2] in Indices LHS;
      A8: [j2,i2] in Indices canMat(i,k,I,K,R) & [i2,j2] in Indices RHS
      proof
        thus [j2,i2] in Indices canMat(i,k,I,K,R) by A7,MATRIX_0:def 6;
        hence thesis by A4,A6,ZFMISC_1:88;
      end;
      per cases;
      suppose A9: [k,i] = [i2,j2];
        then A10: i = j2 & k = i2 by XTUPLE_0:1;
        thus LHS * (i2,j2)
         = (canMat(i,k,I,K,R)) * (j2,i2) by A8,MATRIX_0:def 6
        .= 1.R by A8,A10,Def1
        .= RHS * (i2,j2) by A8,A9,Def1;
      end;
      suppose A11: [k,i] <> [i2,j2];
        A12: [i,k] <> [j2,i2]
        proof
          assume [i,k] = [j2,i2];
          then i = j2 & k = i2 by XTUPLE_0:1;
          hence thesis by A11;
        end;
        thus LHS * (i2,j2)
         = (canMat(i,k,I,K,R)) * (j2,i2) by A8,MATRIX_0:def 6
        .= 0.R by A8,A12,Def1
        .= RHS * (i2,j2) by A8,A11,Def1;
      end;
    end;
    hence thesis by A5,A6,MATRIX_0:21;
  end;
end;

theorem Th43:
  for i,k,I,K being Nat
  holds len canMat (i,k,I,K,R) = I
  & (I = 0 implies width canMat (i,k,I,K,R) = 0)
  & (I <> 0 implies width canMat (i,k,I,K,R) = K)
  by MATRIX_0:22,23,25;

theorem Th44:
  for I,K,i,k,i2 being Nat
  st [i2,k] in Indices canMat(i,k,I,K,R)
  holds (i2 = i implies Line(canMat(i,k,I,K,R), i2) = Line(1.(R,K), k))
  & (i2 <> i implies Line(canMat(i,k,I,K,R), i2) = Line(0.(R,K), k))
proof
  let I,K,i,k,i2 be Nat;
  assume A1: [i2,k] in Indices canMat(i,k,I,K,R);
  then [i2,k] in [:dom canMat(i,k,I,K,R), Seg (width canMat(i,k,I,K,R)):]
  by MATRIX_0:def 4;
  then A2: i2 in dom canMat(i,k,I,K,R) by ZFMISC_1:87;
  set p = Line(canMat(i,k,I,K,R), i2);
  A3: dom p = Seg len p by FINSEQ_1:def 3
           .= Seg width canMat(i,k,I,K,R) by MATRIX_0:def 7;
  A4: for k9 being Nat st k9 in dom p
  holds [i2,k9] in Indices canMat(i,k,I,K,R)
  proof
    let k9 be Nat;
    assume k9 in dom p;
    then [i2,k9] in [:dom canMat(i,k,I,K,R), Seg (width canMat(i,k,I,K,R)):]
    by A2,A3,ZFMISC_1:87;
    hence [i2,k9] in Indices canMat(i,k,I,K,R) by MATRIX_0:def 4;
  end;
  per cases;
  :: default case
  suppose A5: I <> 0 & i in dom canMat(i,k,I,K,R);
    then A6: dom p = Seg K by A3,Th43;
    A7: for k9 being Nat st k9 in dom p
    holds [i,k9] in Indices canMat(i,k,I,K,R)
    proof
      let k9 be Nat;
      assume k9 in dom p;
      then [i,k9] in [:dom canMat(i,k,I,K,R), Seg (width canMat(i,k,I,K,R)):]
      by A5,A3,ZFMISC_1:87;
      hence [i,k9] in Indices canMat(i,k,I,K,R) by MATRIX_0:def 4;
    end;
    [i2,k] in [:dom canMat(i,k,I,K,R), Seg width canMat(i,k,I,K,R):]
    by A1,MATRIX_0:def 4;
    then k in Seg width canMat(i,k,I,K,R) by ZFMISC_1:87;
    then A8: k in Seg K by A5,Th43;
    thus (i2 = i implies Line(canMat(i,k,I,K,R), i2) = Line(1.(R,K), k))
    proof
      assume A9: i2 = i;
      set q = Line(1.(R,K), k);
      A10: dom q = Seg len q by FINSEQ_1:def 3
                .= Seg (width 1.(R,K)) by MATRIX_0:def 7
                .= Seg K by MATRIX_0:24;
      for k9 being Nat st k9 in dom p holds p.k9 = q.k9
      proof
        let k9 be Nat;
        assume A11: k9 in dom p;
        then A12: [i,k9] in Indices canMat(i,k,I,K,R) by A7;
        k9 in Seg len q by A6,A10,A11,FINSEQ_1:def 3;
        then A13: k9 in Seg (width 1.(R,K)) by MATRIX_0:def 7;
        [k,k9] in [:Seg K, Seg K:] by A6,A8,A11,ZFMISC_1:87;
        then A14: [k,k9] in Indices (1.(R,K)) by MATRIX_0:24;
        per cases;
        suppose A15: k9 = k;
          thus p.k9
           = (canMat(i,k,I,K,R)) * (i,k9) by A3,A9,A11,MATRIX_0:def 7
          .= 1.R by A15,A12,Th40
          .= (1.(R,K)) * (k,k) by A14,A15,MATRIX_1:def 3
          .= q.k9 by A13,A15,MATRIX_0:def 7;
        end;
        suppose A16: k9 <> k;
          thus p.k9
           = (canMat(i,k,I,K,R)) * (i,k9) by A3,A9,A11,MATRIX_0:def 7
          .= 0.R by A16,A12,Th40
          .= (1.(R,K)) * (k,k9) by A14,A16,MATRIX_1:def 3
          .= q.k9 by A13,MATRIX_0:def 7;
        end;
      end;
      hence p = q by A6,A10,FINSEQ_1:13;
    end;
    assume A17: i2 <> i;
    set q = Line(0.(R,K), k);
    A18: dom q = Seg len q by FINSEQ_1:def 3
              .= Seg (width 0.(R,K)) by MATRIX_0:def 7
              .= Seg K by MATRIX_0:24;
    for k9 being Nat st k9 in dom p
    holds p.k9 = q.k9
    proof
      let k9 be Nat;
      assume A19: k9 in dom p;
      then A20: k9 in Seg (width 0.(R,K)) by A6,MATRIX_0:24;
      [i2,k] in [:dom canMat(i,k,I,K,R),Seg(width canMat(i,k,I,K,R)):]
      by A1,MATRIX_0:def 4;
      then k in Seg(width canMat(i,k,I,K,R)) by ZFMISC_1:87;
      then k in Seg K by A5,Th43;
      then k in Seg (len 0.(R,K)) by MATRIX_0:24;
      then k in dom 0.(R,K) by FINSEQ_1:def 3;
      then [k,k9] in [:dom 0.(R,K), Seg (width 0.(R,K)):] by A20,ZFMISC_1:87;
      then A21: [k,k9] in Indices (0.(R,K)) by MATRIX_0:def 4;
      A22: k9 in Seg width canMat(i,k,I,K,R) by A5,A6,A19,Th43;
      A23: [i2,k9] in Indices canMat(i,k,I,K,R) by A4,A19;
      thus p.k9
       = (canMat(i,k,I,K,R)) * (i2,k9) by A22,MATRIX_0:def 7
      .= 0.R by A17,A23,Th40
      .= (0.(R,K)) * (k,k9) by A21,MATRIX_1:1
      .= q.k9 by A20,MATRIX_0:def 7;
    end;
    hence p = q by A6,A18,FINSEQ_1:13;
  end;
  :: degenerate cases
  suppose I = 0;
    hence thesis by A1,MATRIX_0:22;
  end;
  suppose A24: I <> 0 & not i in dom canMat(i,k,I,K,R);
    hence (i2 = i implies Line(canMat(i,k,I,K,R),i2) = Line(1.(R,K),k)) by A2;
    thus (i2 <> i implies Line(canMat(i,k,I,K,R),i2) = Line(0.(R,K),k))
    proof
      assume A25: i2 <> i;
      A26: dom p = Seg K by A3,A24,Th43;
      set q = Line(0.(R,K), k);
      A27: dom q = Seg len q by FINSEQ_1:def 3
                .= Seg width 0.(R,K) by MATRIX_0:def 7
                .= Seg K by MATRIX_0:24;
      for k9 being Nat st k9 in dom p
      holds p.k9 = q.k9
      proof
        let k9 be Nat;
        assume A28: k9 in dom p;
        then A29: k9 in Seg width 0.(R,K) by A26,MATRIX_0:24;
        [i2,k] in [:dom canMat(i,k,I,K,R),Seg width canMat(i,k,I,K,R):]
        by A1,MATRIX_0:def 4;
        then k in Seg width canMat(i,k,I,K,R) by ZFMISC_1:87;
        then k in Seg K by A24,Th43;
        then k in Seg len 0.(R,K) by MATRIX_0:24;
        then k in dom 0.(R,K) by FINSEQ_1:def 3;
        then [k,k9] in [:dom 0.(R,K), Seg (width 0.(R,K)):] by A29,ZFMISC_1:87;
        then A30: [k,k9] in Indices (0.(R,K)) by MATRIX_0:def 4;
        A31: k9 in Seg width canMat(i,k,I,K,R) by A24,A26,A28,Th43;
        A32: [i2,k9] in Indices canMat(i,k,I,K,R) by A4,A28;
        thus p.k9
         = (canMat(i,k,I,K,R)) * (i2,k9) by A31,MATRIX_0:def 7
        .= 0.R by A25,A32,Th40
        .= (0.(R,K)) * (k,k9) by A30,MATRIX_1:1
        .= q.k9 by A29,MATRIX_0:def 7;
      end;
      hence p = q by A26,A27,FINSEQ_1:13;
    end;
  end;
end;

theorem Th45:
  for I,K,i,k,k2 being Nat
  st [i,k2] in Indices canMat(i,k,I,K,R)
  holds (k2 = k implies Col(canMat(i,k,I,K,R), k2) = Col(1.(R,I), i))
  & (k2 <> k implies Col(canMat(i,k,I,K,R), k2) = Col(0.(R,I), i))
proof
  let I,K,i,k,k2 be Nat;
  assume A1: [i,k2] in Indices canMat(i,k,I,K,R);
  A2: dom canMat(i,k,I,K,R) = Seg len canMat(i,k,I,K,R) by FINSEQ_1:def 3
                           .= Seg I by Th43;
  A3: dom Col(canMat(i,k,I,K,R), k2)
     = Seg (len (Col(canMat(i,k,I,K,R), k2))) by FINSEQ_1:def 3
    .= Seg len canMat(i,k,I,K,R) by MATRIX_0:def 8
    .= Seg I by Th43;
  A4: i in dom canMat(i,k,I,K,R) & k2 in Seg(width canMat(i,k,I,K,R))
  proof
    [i,k2] in [:dom canMat(i,k,I,K,R),Seg(width canMat(i,k,I,K,R)):]
    by A1,MATRIX_0:def 4;
    hence thesis by ZFMISC_1:87;
  end;
  A5: for j9 being Nat st j9 in dom Col(canMat(i,k,I,K,R), k2)
  holds [j9,k2] in Indices canMat(i,k,I,K,R)
  proof
    let j9 be Nat;
    assume A6: j9 in dom Col(canMat(i,k,I,K,R), k2);
    dom Col(canMat(i,k,I,K,R), k2)
     = Seg len Col(canMat(i,k,I,K,R), k2) by FINSEQ_1:def 3
    .= dom canMat(i,k,I,K,R) by FINSEQ_1:def 3,MATRIX_0:def 8;
    then [j9,k2] in [:dom canMat(i,k,I,K,R),Seg(width canMat(i,k,I,K,R)):]
    by A4,A6,ZFMISC_1:87;
    hence [j9,k2] in Indices canMat(i,k,I,K,R) by MATRIX_0:def 4;
  end;

  A7: for j9 being Nat st j9 in dom Col(canMat(i,k,I,K,R), k2)
  holds [j9,i] in Indices 1.(R,I)
  proof
    let j9 be Nat;
    assume j9 in dom Col(canMat(i,k,I,K,R), k2);
    then [j9,i] in [:(Seg I),(Seg I):] by A2,A3,A4,ZFMISC_1:87;
    hence [j9,i] in Indices 1.(R,I) by MATRIX_0:24;
  end;

  thus (k2 = k implies Col(canMat(i,k,I,K,R), k2) = Col(1.(R,I), i))
  proof
    assume A8: k2 = k;
    A9: dom Col(canMat(i,k,I,K,R), k2)
     = Seg (len 1.(R,I)) by A3,MATRIX_0:24
    .= Seg len (Col(1.(R,I), i)) by MATRIX_0:def 8
    .= dom Col(1.(R,I), i) by FINSEQ_1:def 3;
    for j9 being Nat st j9 in dom Col(canMat(i,k,I,K,R), k2)
    holds Col(canMat(i,k,I,K,R), k2).j9 = Col(1.(R,I), i).j9
    proof
      let j9 be Nat;
      assume A10: j9 in dom Col(canMat(i,k,I,K,R), k2); then
      A11: [j9,k2] in Indices canMat(i,k,I,K,R) by A5;
      A12: [j9, i] in Indices 1.(R,I) by A10,A7;
      then [j9, i] in [:(dom 1.(R,I)),(Seg width 1.(R,I)):]
      by MATRIX_0:def 4;
      then A13: j9 in dom 1.(R,I) by ZFMISC_1:87;
      per cases;
      suppose A14: j9 = i;
        thus Col(canMat(i,k,I,K,R), k2).j9
         = canMat(i,k,I,K,R) * (j9, k2) by A2,A3,A10,MATRIX_0:def 8
        .= 1.R by A8,A11,A14,Th40
        .= (1.(R,I)) * (j9,i) by A12,A14,MATRIX_1:def 3
        .= Col(1.(R,I), i).j9 by A13,MATRIX_0:def 8;
      end;
      suppose A15: j9 <> i;
        thus Col(canMat(i,k,I,K,R), k2).j9
         = canMat(i,k,I,K,R) * (j9, k2) by A2,A3,A10,MATRIX_0:def 8
        .= 0.R by A11,A15,Th40
        .= (1.(R,I)) * (j9,i) by A12,A15,MATRIX_1:def 3
        .= Col(1.(R,I), i).j9 by A13,MATRIX_0:def 8;
      end;
    end;
    hence Col(canMat(i,k,I,K,R), k2) = Col(1.(R,I), i) by A9,FINSEQ_1:13;
  end;
  assume A16: k2 <> k;
  A17: for j9 being Nat st j9 in dom Col(canMat(i,k,I,K,R), k2)
  holds [j9,i] in Indices 0.(R,I)
  proof
    let j9 be Nat;
    assume j9 in dom Col(canMat(i,k,I,K,R), k2);
    then [j9,i] in [:Seg I,Seg I:] by A2,A3,A4,ZFMISC_1:87;
    hence [j9,i] in Indices 0.(R,I) by MATRIX_0:24;
  end;
  A18: dom Col(canMat(i,k,I,K,R), k2)
   = Seg (len 0.(R,I)) by A3,MATRIX_0:24
  .= Seg (len (Col(0.(R,I), i))) by MATRIX_0:def 8
  .= dom Col(0.(R,I), i) by FINSEQ_1:def 3;
  for j9 being Nat st j9 in dom Col(canMat(i,k,I,K,R), k2)
  holds Col(canMat(i,k,I,K,R), k2).j9 = Col(0.(R,I), i).j9
  proof
    let j9 be Nat;
    assume A19: j9 in dom Col(canMat(i,k,I,K,R), k2);
    A20: [j9,k2] in Indices canMat(i,k,I,K,R) by A5,A19;
    A21: [j9, i] in Indices 0.(R,I) by A19,A17;
    then [j9, i] in [:(dom 0.(R,I)),(Seg (width 0.(R,I))):] by MATRIX_0:def 4;
    then A22: j9 in dom 0.(R,I) by ZFMISC_1:87;
    thus Col(canMat(i,k,I,K,R), k2).j9
     = canMat(i,k,I,K,R) * (j9,k2) by A2,A3,A19,MATRIX_0:def 8
    .= 0.R by A20,A16,Th40
    .= (0.(R,I)) * (j9, i) by A21,MATRIX_1:1
    .= Col(0.(R,I), i).j9 by A22,MATRIX_0:def 8;
  end;

  hence Col(canMat(i,k,I,K,R), k2) = Col(0.(R,I), i) by A18,FINSEQ_1:13;
end;

::$N Bourbaki, Algebra~\cite{BourbakiAlgI}, II 10.3 equation (9)
theorem Th46:
  for I,K,L being Nat st I <> 0 & K <> 0
  for i,k1,k2,l being Nat st k1 <> k2
  holds (canMat (i,k1,I,K,R)) * (canMat(k2,l,K,L,R)) = 0.(R,I,L)
proof
  let I,K,L be Nat;
  assume A1: I <> 0;
  assume A2: K <> 0;
  let i,k1,k2,l be Nat;
  assume A3: k1 <> k2;
  set LHS = (canMat (i,k1,I,K,R)) * (canMat(k2,l,K,L,R));
  set RHS = 0.(R,I,L);
  A4: width canMat (i,k1,I,K,R) = K by A1,MATRIX_0:23
                               .= len canMat(k2,l,K,L,R) by MATRIX_0:25;
  A5: LHS is Matrix of I,L,R & RHS is Matrix of I,L,R
  proof
    A6: len LHS = len canMat (i,k1,I,K,R) by A4,MATRIX_3:def 4
               .= I by A1,MATRIX_0:23;
    width LHS = width canMat(k2,l,K,L,R) by A4,MATRIX_3:def 4
             .= L by A2,MATRIX_0:23;
    hence thesis by A1,A6,MATRIX_0:20;
  end;
  per cases;
  suppose not [i,k1] in Indices canMat (i,k1,I,K,R);
    then A7: canMat (i,k1,I,K,R) = 0.(R, I, K) by Th41;
    width 0.(R, I, K) = K &
    width canMat(k2,l,K,L,R) = L &
    len canMat(k2,l,K,L,R) = K by A1,A2,MATRIX_0:23;
    hence LHS = 0.(R, I, L) by A7,Th17;
  end;
  suppose not [k2,l] in Indices canMat(k2,l,K,L,R);
    then A9: canMat(k2,l,K,L,R) = 0.(R, K, L) by Th41;
    len canMat (i,k1,I,K,R) = I & width canMat (i,k1,I,K,R) = K &
    width 0.(R, K, L) = L by A1,A2,MATRIX_0:23;
    hence LHS = 0.(R, I, L) by A9,Th18;
  end;
  suppose A11: [i,k1] in Indices canMat(i,k1,I,K,R)
          & [k2,l] in Indices canMat(k2,l,K,L,R);
    for i9,l9 being Nat st [i9,l9] in Indices LHS
    holds LHS * (i9,l9) = RHS * (i9,l9)
    proof
      let i9,l9 be Nat;
      assume A12: [i9,l9] in Indices LHS;
      then [i9,l9] in [:Seg I, Seg L:] by A1,A5,MATRIX_0:23;
      then A13: i9 in Seg I & l9 in Seg L by ZFMISC_1:87;
      A14: [i9,k1] in Indices canMat (i,k1,I,K,R)
      proof
        [i9,l9] in [:dom LHS, Seg(width LHS):] by A12,MATRIX_0:def 4;
        then i9 in dom LHS by ZFMISC_1:87;
        then i9 in Seg len LHS by FINSEQ_1:def 3;
        then i9 in Seg len canMat (i,k1,I,K,R) by A4,MATRIX_3:def 4;
        then A15: i9 in dom canMat (i,k1,I,K,R) by FINSEQ_1:def 3;
        [i,k1] in [:dom canMat(i,k1,I,K,R),Seg(width canMat(i,k1,I,K,R)):]
        by A11,MATRIX_0:def 4;
        then i in dom canMat(i,k1,I,K,R) & k1 in Seg(width canMat(i,k1,I,K,R))
        by ZFMISC_1:87;
        then
        [i9,k1] in [:dom canMat(i,k1,I,K,R),Seg width canMat(i,k1,I,K,R):]
        by A15,ZFMISC_1:87;
        hence thesis by MATRIX_0:def 4;
      end;
      then [i9,k1] in [:Seg I, Seg K:] by A1,MATRIX_0:23;
      then A16: i9 in Seg I & k1 in Seg K by ZFMISC_1:87;
      A17: [i9,l9] in Indices RHS
      proof
        [i9,l9] in [:Seg I,Seg L:] by A13,ZFMISC_1:87;
        hence thesis by A1,MATRIX_0:23;
      end;
      k1 in Seg len canMat(k2,l,K,L,R) by A2,A16,MATRIX_0:23; then
      A18: k1 in dom canMat(k2,l,K,L,R) by FINSEQ_1:def 3;
      A19: [k1,l9] in Indices canMat(k2,l,K,L,R)
      proof
        [k1,l9] in [:Seg K,Seg L:] by A13,A16,ZFMISC_1:87;
        hence [k1,l9] in Indices canMat(k2,l,K,L,R) by A2,MATRIX_0:23;
      end;
      Indices canMat(i,k1,I,K,R) = [:Seg I, Seg K:] by A1,MATRIX_0:23;
      then k1 in Seg K by A11,ZFMISC_1:87;
      then k1 in Seg (len 1.(R,K)) by MATRIX_0:24;
      then A20: k1 in dom 1.(R,K) by FINSEQ_1:def 3;
      A21: dom 1.(R,K) = Seg (len 1.(R,K)) by FINSEQ_1:def 3
                      .= Seg K by MATRIX_0:24
                      .= Seg (len 0.(R,K)) by MATRIX_0:24
                      .= dom 0.(R,K) by FINSEQ_1:def 3;
      :: then A21: k1 in dom 0.(R,K) by A20;
      per cases;
      suppose A22: i9 = i;
        thus LHS * (i9,l9)
         = Line(canMat (i,k1,I,K,R), i9) "*" Col(canMat(k2,l,K,L,R),l9)
           by A4,A12,MATRIX_3:def 4
        .= Line(1.(R,K), k1) "*" Col(canMat(k2,l,K,L,R),l9)
           by A22,A14,Th44
        .= canMat(k2,l,K,L,R) * (k1,l9) by A20,A18,Th21
        .= 0.R by A3,A19,Th40
        .= RHS * (i9,l9) by A17,MATRIX_3:1;
      end;
      suppose A23: i9 <> i;
        thus LHS * (i9,l9)
         = Line(canMat (i,k1,I,K,R), i9) "*" Col(canMat(k2,l,K,L,R),l9)
           by A4,A12,MATRIX_3:def 4
        .= Line(0.(R,K), k1) "*" Col(canMat(k2,l,K,L,R),l9)
           by A23,A14,Th44
        .= 0.R by A20,A21,Th19
        .= RHS * (i9,l9) by A17,MATRIX_3:1;
      end;
    end;
    hence LHS = RHS by A5,MATRIX_0:27;
  end;
end;

::$N Bourbaki, Algebra~\cite{BourbakiAlgI}, II 10.3 equation (9)
theorem Th47:
  for I,K,L,i,k,l being Nat st i in Seg I & k in Seg K & l in Seg L
  holds (canMat (i,k,I,K,R)) * (canMat(k,l,K,L,R)) = canMat(i,l,I,L,R)
proof
  let I,K,L,i,k,l be Nat;
  assume A1: i in Seg I;
  assume A2: k in Seg K;
  assume A3: l in Seg L;
  set LHS = (canMat (i,k,I,K,R)) * (canMat(k,l,K,L,R));
  set RHS = canMat(i,l,I,L,R);
  per cases;
  suppose I = 0; :: degenerate cases
    hence thesis by A1;
  end;
  suppose K = 0;
    hence thesis by A2;
  end;
  suppose L = 0;
    hence thesis by A3;
  end;
  suppose A4: I <> 0 & K <> 0 & L <> 0; :: textbook case
    then A5: len canMat (i,k,I,K,R) = I & width canMat (i,k,I,K,R) = K
    & len (canMat(k,l,K,L,R)) = K & width canMat(k,l,K,L,R) = L
    by Th43;
    then A6: width canMat (i,k,I,K,R) = len canMat(k,l,K,L,R);
    A7: len LHS = len RHS & width LHS = width RHS
    proof
      thus len LHS = I by A5,MATRIX_3:def 4
                  .= len RHS by Th43;
      thus width LHS = L by A5,MATRIX_3:def 4
                    .= width RHS by A4,Th43;
    end;
    for i2,l2 being Nat st [i2,l2] in Indices LHS
    holds LHS * (i2,l2) = RHS * (i2,l2)
    proof
      let i2,l2 be Nat;
      assume A8: [i2,l2] in Indices LHS;
      A9: i2 in Seg I & l2 in Seg L
      proof
        A10: [i2,l2] in [:dom LHS, Seg(width LHS):] by A8,MATRIX_0:def 4;
        dom LHS = Seg len LHS by FINSEQ_1:def 3
               .= Seg I by A5,MATRIX_3:def 4;
        hence i2 in Seg I by A10,ZFMISC_1:87;
        i2 in dom LHS & l2 in Seg(width LHS) by A10,ZFMISC_1:87;
        hence l2 in Seg L by A5,MATRIX_3:def 4;
      end;
      A11: [i2,l2] in Indices RHS
      proof
        len RHS = I by Th43;
        then A12: i2 in dom RHS by A9,FINSEQ_1:def 3;
        width RHS = L by A4,Th43;
        then [i2,l2] in [:dom RHS, Seg(width RHS):] by A9,A12,ZFMISC_1:87;
        hence [i2,l2] in Indices RHS by MATRIX_0:def 4;
      end;
      len 0.(R,K) = K by MATRIX_0:25;
      then A13: k in dom 0.(R,K) by A2,FINSEQ_1:def 3;
      per cases;
      suppose A14: i <> i2;
        [i2,k] in Indices canMat(i,k,I,K,R)
        proof
          len canMat(i,k,I,K,R) = I by Th43;
          then A15: i2 in dom canMat(i,k,I,K,R) by A9,FINSEQ_1:def 3;
          k in Seg(width canMat(i,k,I,K,R)) by A2,A4,Th43;
          then
          [i2,k] in [:dom canMat(i,k,I,K,R), Seg(width canMat(i,k,I,K,R)):]
          by A15,ZFMISC_1:87;
          hence thesis by MATRIX_0:def 4;
        end;
        then Line(canMat(i,k,I,K,R), i2) = Line(0.(R,K), k) by A14,Th44;
        hence LHS * (i2,l2)
         = Line(0.(R,K), k) "*" Col(canMat(k,l,K,L,R),l2)
           by A6,A8,MATRIX_3:def 4
        .= 0.R by A13,Th19
        .= RHS * (i2,l2) by A11,A14,Th40;
      end;
      suppose A17: l2 <> l;
        [k,l2] in Indices canMat(k,l,K,L,R)
        proof
          len canMat(k,l,K,L,R) = K by Th43;
          then A18: k in dom canMat(k,l,K,L,R) by A2,FINSEQ_1:def 3;
          l2 in Seg(width canMat(k,l,K,L,R)) by A9,A4,Th43;
          then
          [k,l2] in [:dom canMat(k,l,K,L,R), Seg(width canMat(k,l,K,L,R)):]
          by A18,ZFMISC_1:87;
          hence thesis by MATRIX_0:def 4;
        end;
        then A19: Col(canMat(k,l,K,L,R),l2) = Col(0.(R,K), k) by A17,Th45;
        thus LHS * (i2,l2)
         = Line(canMat(i,k,I,K,R), i2) "*" Col(canMat(k,l,K,L,R),l2)
           by A6,A8,MATRIX_3:def 4
        .= 0.R by A13,A19,Th20
        .= RHS * (i2,l2) by A11,A17,Th40;
      end;
      suppose A20: i = i2 & l = l2;
        A21: k in dom 1.(R,K) & k in dom canMat(k,l,K,L,R)
        proof
          dom 1.(R,K) = Seg (len 1.(R,K)) by FINSEQ_1:def 3
                     .= Seg K by MATRIX_0:24;
          hence k in dom 1.(R,K) by A2;
          dom canMat(k,l,K,L,R) = Seg len canMat(k,l,K,L,R) by FINSEQ_1:def 3
                               .= Seg K by Th43;
          hence k in dom canMat(k,l,K,L,R) by A2;
        end;

        A22: [k,l] in Indices canMat(k,l,K,L,R)
        proof
          len canMat(k,l,K,L,R) = K by Th43;
          then A23: k in dom canMat(k,l,K,L,R) by A2,FINSEQ_1:def 3;
          width canMat(k,l,K,L,R) = L by A4,Th43;
          then [k,l] in [:dom canMat(k,l,K,L,R),Seg(width canMat(k,l,K,L,R)):]
          by A3,A23,ZFMISC_1:87;
          hence thesis by MATRIX_0:def 4;
        end;
        [i2,k] in Indices canMat(i,k,I,K,R)
        proof
          len canMat(i,k,I,K,R) = I by Th43;
          then A24: i2 in dom canMat(i,k,I,K,R) by A9,FINSEQ_1:def 3;
          width canMat(i,k,I,K,R) = K by A4,Th43;
          then [i2,k] in [:dom canMat(i,k,I,K,R),Seg(width canMat(i,k,I,K,R)):]
          by A2,A24,ZFMISC_1:87;
          hence thesis by MATRIX_0:def 4;
        end;
        then A25: Line(canMat(i,k,I,K,R), i2) = Line(1.(R,K), k) by A20,Th44;
        thus LHS * (i2,l2)
         = Line(canMat(i,k,I,K,R), i2) "*" Col(canMat(k,l,K,L,R),l2)
           by A6,A8,MATRIX_3:def 4
        .= canMat(k,l,K,L,R) * (k,l2) by A21,A25,Th21
        .= 1.R by A20,A22,Th40
        .= RHS * (i2,l2) by A20,A11,Th40;
      end;
    end;
    hence LHS = RHS by A7,MATRIX_0:21;
  end;
end;

theorem Th48:
  for I,K,L being Nat st I = 0 implies K = 0
  for i,k,l being Nat st k in Seg K
  holds (canMat (i,k,I,K,R)) * (canMat(k,l,K,L,R)) = canMat(i,l,I,L,R)
proof
  let I,K,L be Nat;
  assume A1: I = 0 implies K = 0;
  let i,k,l be Nat;
  assume A2: k in Seg K;
  set LHS = (canMat (i,k,I,K,R)) * (canMat(k,l,K,L,R));
  set RHS = canMat(i,l,I,L,R);
  per cases;
  :: degenerate cases
  suppose I = 0;
    hence thesis by A1,A2;
   end;
  suppose I <> 0 & K = 0;
    hence thesis by A2;
  end;
  :: textbook case
  suppose A3: I <> 0 & K <> 0;
    per cases;
    :: textbook subcase
    suppose i in Seg I & l in Seg L;
      hence thesis by A2,Th47;
    end;
    :: degenerate edge-cases no one thinks about
    suppose A4: not i in Seg I;
      A5: width 0.(R, I, K) = K
          & width canMat(k,l,K,L,R) = L
          & len canMat(k,l,K,L,R) = K by A3,MATRIX_0:23;
      dom canMat (i,k,I,K,R) = Seg len canMat (i,k,I,K,R) by FINSEQ_1:def 3
                            .= Seg I by MATRIX_0:25;
      then
      not [i,k] in [:dom canMat (i,k,I,K,R), Seg(width canMat (i,k,I,K,R)):]
      by A4,ZFMISC_1:87;
      then not [i,k] in Indices canMat (i,k,I,K,R) by MATRIX_0:def 4;
      then canMat (i,k,I,K,R) = 0.(R, I, K) by Th41;
      then A6: LHS = 0.(R, I, L) by A5,Th17;
      dom (canMat(i,l,I,L,R)) = Seg len (canMat(i,l,I,L,R)) by FINSEQ_1:def 3
                             .= Seg I by MATRIX_0:25;
      then
      not [i,l] in [:dom(canMat(i,l,I,L,R)), Seg(width(canMat(i,l,I,L,R))):]
      by A4,ZFMISC_1:87;
      then not [i,l] in Indices (canMat(i,l,I,L,R)) by MATRIX_0:def 4;
      hence canMat(i,l,I,L,R) = LHS by A6,Th41;
    end;
    suppose A7: not l in Seg L;
      A8: not [k,l] in Indices (canMat(k,l,K,L,R))
      proof
        set X = canMat(k,l,K,L,R);
        not l in Seg width X by A3,A7,Th43;
        then not [k,l] in [:dom X, Seg(width X):] by ZFMISC_1:87;
        hence thesis by MATRIX_0:def 4;
      end;
      A9: not [i,l] in Indices (canMat(i,l,I,L,R))
      proof
        set X = canMat(i,l,I,L,R);
        not l in Seg width X by A3,A7,Th43;
        then not [i,l] in [:dom X, Seg(width X):] by ZFMISC_1:87;
        hence thesis by MATRIX_0:def 4;
      end;
      set A = canMat (i,k,I,K,R);
      A10: L = width canMat(k,l,K,L,R)
      & I = len A & K = width A by A3,Th43;
      A11: canMat(k,l,K,L,R) = 0.(R,width A,L) by A10,A8,Th41;
      thus RHS = 0.(R,len A, L) by A10,A9,Th41
              .= LHS by A10,A11,Th18;
    end;
  end;
end;

definition
  let R,n;
  let i,k be Nat;
  func canMat (i,k,n,R) -> Matrix of n,R equals
  canMat(i,k,n,n,R);
  coherence;
end;

theorem
  for i,k,i2,k2 being Nat
  st [i2,k2] in Indices canMat(i,k,n,R)
  holds (i <> i2 implies canMat(i,k,n,R) * (i2,k2) = 0.R)
  & (k <> k2 implies canMat(i,k,n,R) * (i2,k2) = 0.R)
  & (i = i2 & k = k2 implies canMat(i,k,n,R) * (i2,k2) = 1.R)
  by Th40;

theorem Th50:
  for I,i,j1,j2,k being Nat st j1 <> j2
  holds (canMat(i,j1,I,R)) * (canMat(j2,k,I,R)) = 0.(R,I)
proof
  let I,i,j1,j2,k be Nat;
  assume A1: j1 <> j2;
  set LHS = (canMat(i,j1,I,R)) * (canMat(j2,k,I,R));
  per cases;
  suppose I = 0; then
    for i9,j9 being Nat st [i9,j9] in Indices LHS
    holds LHS * (i9, j9) = 0.(R,I) * (i9,j9) by MATRIX_0:22;
    hence thesis by MATRIX_0:27;
  end;
  suppose A3: I <> 0;
    0.(R,I) = 0.(R,I,I);
    hence (canMat(i,j1,I,R)) * (canMat(j2,k,I,R)) = 0.(R,I) by A1,A3,Th46;
  end;
end;

theorem
  for i,j being Nat st not [i,j] in Indices canMat(i,j,n,R)
  holds canMat(i,j,n,R) = 0.(R,n)
proof
  0.(R,n,n) = 0.(R,n);
  hence thesis by Th41;
end;

theorem
  for i,k,l being Nat st k in Seg n
  holds (canMat(i,k,n,R)) * (canMat(k,l,n,R)) = canMat(i,l,n,R) by Th48;

theorem Th54:
  for i,j being Nat st [i,j] in Indices canMat(i,j,n,R)
  for A being Matrix of n,R
  for i2,j2 being Nat st [i2,j2] in Indices A
  holds (i = i2 implies ((canMat(i,j,n,R)) * A) * (i2,j2) = A * (j,j2))
  & (i <> i2 implies ((canMat(i,j,n,R)) * A) * (i2,j2) = 0.R)
proof
  let i,j be Nat;
  assume A1: [i,j] in Indices canMat(i,j,n,R);
  let A be Matrix of n,R;
  let i2,j2 be Nat;
  assume A2: [i2,j2] in Indices A;
  A3: Indices ((canMat(i,j,n,R)) * A) = [:Seg n,Seg n:] by MATRIX_0:24
                                     .= Indices A by MATRIX_0:24;
  A4: [i2,j] in Indices canMat(i,j,n,R)
  proof
    [i,j] in [:Seg n,Seg n:] by A1,MATRIX_0:24;
    then A5: j in Seg n by ZFMISC_1:87;
    [i2,j2] in [:Seg n,Seg n:] by A2,MATRIX_0:24;
    then i2 in Seg n by ZFMISC_1:87;
    then [i2,j] in [:Seg n,Seg n:] by A5,ZFMISC_1:87;
    hence thesis by MATRIX_0:24;
  end;
  thus i = i2 implies ((canMat(i,j,n,R)) * A) * (i2,j2) = A * (j,j2)
  proof
    assume A6: i = i2;
    A7: j in dom 1.(R,n) & j in dom A
    proof
      A8: [i,j] in [:Seg n,Seg n:] by A1,MATRIX_0:24;
      dom 1.(R,n) = Seg (len 1.(R,n)) by FINSEQ_1:def 3
                 .= Seg n by MATRIX_0:24;
      hence j in dom 1.(R,n) by A8,ZFMISC_1:87;
      dom A = Seg len A by FINSEQ_1:def 3
           .= Seg n by MATRIX_0:24;
      hence j in dom A by A8,ZFMISC_1:87;
    end;
    width canMat(i,j,n,R) = n by MATRIX_0:24
                         .= len A by MATRIX_0:24;
    hence ((canMat(i,j,n,R)) * A) * (i2,j2)
     = Line (canMat(i,j,n,R),i2) "*" Col(A, j2) by A2,A3,MATRIX_3:def 4
    .= Line (1.(R,n), j) "*" Col(A, j2) by A6,A4,Th44
    .= A * (j, j2) by A7,Th21;
  end;
  assume A9: i <> i2;
  A10: j in dom 0.(R,n)
  proof
    A11: [i,j] in [:Seg n,Seg n:] by A1,MATRIX_0:24;
    dom 0.(R,n) = Seg (len 0.(R,n)) by FINSEQ_1:def 3
               .= Seg n by MATRIX_0:24;
    hence j in dom 0.(R,n) by A11,ZFMISC_1:87;
  end;
  width (canMat(i,j,n,R)) = n by MATRIX_0:24
                         .= len A by MATRIX_0:24;
  hence ((canMat(i,j,n,R)) * A) * (i2,j2)
   = Line(canMat(i,j,n,R),i2) "*" Col(A,j2) by A2,A3,MATRIX_3:def 4
  .= Line(0.(R,n), j) "*" Col(A,j2) by A4,A9,Th44
  .= 0.R by A10,Th19;
end;

theorem Th55:
  for i,j being Nat st [i,j] in Indices canMat(i,j,n,R)
  for A being Matrix of n,R
  for i2,j2 being Nat st [i2,j2] in Indices A
  holds (j = j2 implies (A * (canMat(i,j,n,R))) * (i2,j2) = A * (i2,i))
  & (j <> j2 implies (A * (canMat(i,j,n,R))) * (i2,j2) = 0.R)
proof
  let i,j be Nat;
  assume [i,j] in Indices canMat(i,j,n,R); then
  A6: [i,j] in [:Seg n,Seg n:] by MATRIX_0:24;
  let A be Matrix of n,R;
  let i2,j2 be Nat;
  assume A2: [i2,j2] in Indices A;
  A3: [i,j2] in Indices canMat(i,j,n,R)
  proof
    A4: i in Seg n by A6,ZFMISC_1:87;
    [i2,j2] in [:Seg n,Seg n:] by A2,MATRIX_0:24;
    then j2 in Seg n by ZFMISC_1:87;
    then [i,j2] in [:Seg n,Seg n:] by A4,ZFMISC_1:87;
    hence [i,j2] in Indices canMat(i,j,n,R) by MATRIX_0:24;
  end;
  A5: i in dom A & i in dom 1.(R,n)
  proof
    dom A = Seg len A by FINSEQ_1:def 3
         .= Seg n by MATRIX_0:24;
    hence i in dom A by A6,ZFMISC_1:87;
    dom 1.(R,n) = Seg len 1.(R,n) by FINSEQ_1:def 3
               .= Seg n by MATRIX_0:24;
    hence i in dom 1.(R,n) by A6,ZFMISC_1:87;
  end;
  A7: width A = n by MATRIX_0:24
             .= len canMat(i,j,n,R) by MATRIX_0:25;
  A8: [i2,j2] in Indices (A * (canMat(i,j,n,R)))
  proof
    Indices A = [:Seg n,Seg n:] by MATRIX_0:24
             .= Indices (A * (canMat(i,j,n,R))) by MATRIX_0:24;
    hence [i2,j2] in Indices (A * (canMat(i,j,n,R))) by A2;
  end;

  thus (j = j2 implies (A * (canMat(i,j,n,R))) * (i2,j2) = A * (i2,i))
  proof
    assume A9: j = j2;
    thus (A * (canMat(i,j,n,R))) * (i2,j2)
     = Line(A,i2) "*" Col(canMat(i,j,n,R), j2) by A7,A8,MATRIX_3:def 4
    .= Line(A,i2) "*" Col(1.(R,n), i) by A3,A9,Th45
    .= A * (i2,i) by A5,Th23;
  end;
  assume A10: j <> j2;
  A11: dom 0.(R,n) = Seg len 0.(R,n) by FINSEQ_1:def 3
                  .= Seg n by MATRIX_0:24
                  .= Seg len 1.(R,n) by MATRIX_0:24
                  .= dom 1.(R,n) by FINSEQ_1:def 3;
  thus (A * (canMat(i,j,n,R))) * (i2,j2)
   = Line(A,i2) "*" Col(canMat(i,j,n,R), j2) by A7,A8,MATRIX_3:def 4
  .= Line(A,i2) "*" Col(0.(R,n), i) by A3,A10,Th45
  .= 0.R by A5,A11,Th20;
end;

theorem Th56:
  for r being Element of R
  for i,j being Nat
  holds canMat(i,j,n,R)*r = r*canMat(i,j,n,R)
proof
  let r be Element of R;
  let i,j be Nat;
  A1: len(canMat(i,j,n,R)*r) = len(canMat(i,j,n,R)) by MATRIX_3:def 6
                            .= len(r*canMat(i,j,n,R)) by MATRIX_3:def 5;
  A2: width(canMat(i,j,n,R)*r) = width(canMat(i,j,n,R)) by MATRIX_3:def 6
                              .= width(r*canMat(i,j,n,R)) by MATRIX_3:def 5;
  for i2,j2 being Nat st [i2,j2] in Indices (canMat(i,j,n,R)*r)
  holds (canMat(i,j,n,R)*r) * (i2,j2) = (r*canMat(i,j,n,R)) * (i2,j2)
  proof
    let i2,j2 be Nat;
    assume A3: [i2,j2] in Indices (canMat(i,j,n,R)*r);
    A4: [i2,j2] in Indices canMat(i,j,n,R)
    proof
      A5: dom(canMat(i,j,n,R)*r)
       = Seg len(canMat(i,j,n,R)*r) by FINSEQ_1:def 3
      .= Seg len(canMat(i,j,n,R)) by MATRIX_3:def 6
      .= dom canMat(i,j,n,R) by FINSEQ_1:def 3;
      Seg width(canMat(i,j,n,R)*r) = Seg width(canMat(i,j,n,R))
        by MATRIX_3:def 6;
      then [:dom(canMat(i,j,n,R)*r),Seg(width(canMat(i,j,n,R)*r)):]
       = Indices canMat(i,j,n,R) by A5,MATRIX_0:def 4;
      hence thesis by A3,MATRIX_0:def 4;
    end;
    per cases;
    suppose A6: [i,j] = [i2,j2];
      thus (canMat(i,j,n,R)*r) * (i2,j2)
       = (canMat(i,j,n,R) * (i2,j2)) * r by A4,MATRIX_3:def 6
      .= (1.R) * r by A4,A6,Def1
      .= r * (1.R)
      .= r * (canMat(i,j,n,R) * (i2,j2)) by A4,A6,Def1
      .= (r*canMat(i,j,n,R)) * (i2,j2) by A4,MATRIX_3:def 5;
    end;
    suppose A7: [i,j] <> [i2,j2];
      thus (canMat(i,j,n,R)*r) * (i2,j2)
       = (canMat(i,j,n,R) * (i2,j2)) * r by A4,MATRIX_3:def 6
      .= (0.R) * r by A4,A7,Def1
      .= r * (0.R)
      .= r * (canMat(i,j,n,R) * (i2,j2)) by A4,A7,Def1
      .= (r*canMat(i,j,n,R)) * (i2,j2) by A4,MATRIX_3:def 5;
    end;
  end;
  hence canMat(i,j,n,R)*r = r*canMat(i,j,n,R) by A1,A2,MATRIX_0:21;
end;

theorem Th57:
  for i,j being Nat st i <> j
  for r being Element of R
  holds 1.(R,n) + r*canMat(i,j,n,R) is invertible Matrix of n,R
proof
  let i,j be Nat;
  assume A1: i <> j;
  let r be Element of R;
  set M = 1.(R,n) + r*canMat(i,j,n,R);
  per cases;
  suppose n = 0; :: degenerate case
    then M * M = 1.(R,n) by MATRIX_0:45;
    hence thesis by MATRIX_6:def 2,def 3;
  end;
  suppose A2: n > 0; :: textbook case
    ex M2 being Matrix of n,R st M is_reverse_of M2
    proof
      consider M2 being Matrix of n,R such that
      A3: M2 = 1.(R,n) - r*canMat(i,j,n,R);
      take M2;
      A4:  len 1.(R,n) = len (r*canMat(i,j,n,R))
         & width 1.(R,n) = width (r*canMat(i,j,n,R))
         & len (r*canMat(i,j,n,R)) = width 1.(R,n) & len 1.(R,n) > 0
         & len (r*canMat(i,j,n,R)) > 0
      proof
        thus len 1.(R,n) = n by MATRIX_0:24
                        .= len (r*canMat(i,j,n,R)) by MATRIX_0:24;
        thus width 1.(R,n) = n by MATRIX_0:24
                          .= width (r*canMat(i,j,n,R)) by MATRIX_0:24;
        thus len (r*canMat(i,j,n,R)) = n by MATRIX_0:24
                                    .= width 1.(R,n) by MATRIX_0:24;
        thus len 1.(R,n) > 0 by A2,MATRIX_0:24;
        thus len (r*canMat(i,j,n,R)) > 0 by A2,MATRIX_0:24;
      end;

      A5: len 1.(R,n) = len (r*canMat(i,j,n,R))
       & width 1.(R,n) = width (r*canMat(i,j,n,R)) & len 1.(R,n) = width M
       & len 1.(R,n) > 0 & len M > 0
      proof
        thus len 1.(R,n) = len (r*canMat(i,j,n,R)) by A4;
        thus width 1.(R,n) = width (r*canMat(i,j,n,R)) by A4;
        thus len 1.(R,n) = n by MATRIX_0:24
                        .= width M by MATRIX_0:24;
        thus len 1.(R,n) > 0 by A4;
        thus len M > 0 by A2,MATRIX_0:24;
      end;

      A6: (r*canMat(i,j,n,R))*(r*canMat(i,j,n,R))
       = ((r*canMat(i,j,n,R))*r)*canMat(i,j,n,R) by Th24
      .= (r*(canMat(i,j,n,R)*r))*canMat(i,j,n,R) by Th26
      .= (r*(r*canMat(i,j,n,R)))*canMat(i,j,n,R) by Th56
      .= ((r*r)*canMat(i,j,n,R))*canMat(i,j,n,R) by Th27
      .= (r*r)*(canMat(i,j,n,R)*canMat(i,j,n,R)) by Th29
      .= (r*r)*0.(R,n) by A1,Th50
      .= 0.(R,n) by Th28;
      A7: len 1.(R,n) = len(r*canMat(i,j,n,R)) &
      width 1.(R,n) = width(r*canMat(i,j,n,R))
      proof
        thus len 1.(R,n) = n by MATRIX_0:24
                        .= len(r*canMat(i,j,n,R)) by MATRIX_0:24;
        thus width 1.(R,n) = n by MATRIX_0:24
                          .= width(r*canMat(i,j,n,R)) by MATRIX_0:24;
      end;

      A8: M * M2
       = (M * 1.(R,n)) - (M * (r*canMat(i,j,n,R))) by A3,A5,MATRIXR2:20
      .= M - (M * (r*canMat(i,j,n,R))) by MATRIX_3:19
      .= M - ((1.(R,n)*(r*canMat(i,j,n,R)))
              + ((r*canMat(i,j,n,R)))*(r*canMat(i,j,n,R)))
         by A4,MATRIX_4:63
      .= M - ((r*canMat(i,j,n,R)) + 0.(R,n)) by A6,MATRIX_3:18
      .= M - (r*canMat(i,j,n,R)) by MATRIX_1:5
      .= 1.(R,n) by A7,MATRIX_4:38;
      A9: len 1.(R,n) = len(r*canMat(i,j,n,R))
      & width 1.(R,n) = width(r*canMat(i,j,n,R))
      & len(M) = width 1.(R,n) & len 1.(R,n) > 0 & len(M) > 0
      proof
        thus len 1.(R,n) = n by MATRIX_0:24
                        .= len(r*canMat(i,j,n,R)) by MATRIX_0:24;
        thus width 1.(R,n) = n by MATRIX_0:24
                          .= width(r*canMat(i,j,n,R)) by MATRIX_0:24;
        thus len M = n by MATRIX_0:24
                   .= width 1.(R,n) by MATRIX_0:24;
        thus len 1.(R,n) > 0 by A2,MATRIX_0:24;
        thus len M > 0 by A2,MATRIX_0:24;
      end;
      A10: len 1.(R,n) = len(r*canMat(i,j,n,R))
      & width 1.(R,n) = width(r*canMat(i,j,n,R))
      & width(r*canMat(i,j,n,R)) = len 1.(R,n)
      & len(r*canMat(i,j,n,R)) > 0 & len 1.(R,n) > 0
      proof
        thus len 1.(R,n) = len(r*canMat(i,j,n,R)) by A9;
        thus width 1.(R,n) = width(r*canMat(i,j,n,R)) by A9;
        thus width(r*canMat(i,j,n,R)) = n by MATRIX_0:24
                                     .= len 1.(R,n) by MATRIX_0:24;
        thus len(r*canMat(i,j,n,R)) > 0 by A2,MATRIX_0:24;
        thus len 1.(R,n) > 0 by A9;
      end;
      M2 * M
       = (1.(R,n) * M) - ((r*canMat(i,j,n,R)) * M) by A3,A9,MATRIXR2:16
      .= M - ((r*canMat(i,j,n,R)) * M) by MATRIX_3:18
      .= M - (((r*canMat(i,j,n,R))*(1.(R,n))) + 0.(R,n)) by A6,A10,MATRIX_4:62
      .= M - ((r*canMat(i,j,n,R))*(1.(R,n))) by MATRIX_1:5
      .= M - (r*canMat(i,j,n,R)) by MATRIX_3:19
      .= 1.(R,n) by A10,MATRIX_4:21;
      hence M is_reverse_of M2 by A8,MATRIX_6:def 2;
    end;
    hence 1.(R,n) + r*canMat(i,j,n,R) is invertible Matrix of n,R
    by MATRIX_6:def 3;
  end;
end;

theorem Th58:
  for i,j being Nat
  for r being Element of R
  for A being Matrix of n,R
  holds A * (1.(R,n) + r*canMat(i,j,n,R)) = (1.(R,n) + r*canMat(i,j,n,R)) * A
  iff A * (r*canMat(i,j,n,R)) = (r*canMat(i,j,n,R)) * A
proof
  let i,j be Nat;
  let r be Element of R;
  let A be Matrix of n,R;
  per cases;
  suppose A1: n > 0; :: default case
    A2: len 1.(R,n) = len (r*canMat(i,j,n,R))
    & width 1.(R,n) = width (r*canMat(i,j,n,R)) & width A = len 1.(R,n)
    & len A > 0 & len 1.(R,n) > 0
    proof
      thus len 1.(R,n) = n by MATRIX_0:24
                      .= len(r*canMat(i,j,n,R)) by MATRIX_0:24;
      thus width 1.(R,n) = n by MATRIX_0:24
                        .= width(r*canMat(i,j,n,R)) by MATRIX_0:24;
      thus width A = n by MATRIX_0:24
                  .= len 1.(R,n) by MATRIX_0:24;
      thus len A > 0 by A1,MATRIX_0:24;
      thus len 1.(R,n) > 0 by A1,MATRIX_0:24;
    end;
    A3: len 1.(R,n) = len (r*canMat(i,j,n,R))
    & width 1.(R,n) = width (r*canMat(i,j,n,R)) & len A = width 1.(R,n)
    & len 1.(R,n) > 0 & len A > 0
    proof
      thus len 1.(R,n) = len (r*canMat(i,j,n,R)) by A2;
      thus width 1.(R,n) = width (r*canMat(i,j,n,R)) by A2;
      thus len A = n by MATRIX_0:24
                .= width 1.(R,n) by MATRIX_0:24;
      thus len 1.(R,n) > 0 by A2;
      thus len A > 0 by A2;
    end;
    hereby
      assume A4: A * (1.(R,n) + r*canMat(i,j,n,R))
      = (1.(R,n) + r*canMat(i,j,n,R)) * A;
      A5: len(A * (r*canMat(i,j,n,R))) = len((r*canMat(i,j,n,R)) * A)
      & len((r*canMat(i,j,n,R)) * A) = len A
      & width(A * (r*canMat(i,j,n,R))) = width((r*canMat(i,j,n,R)) * A)
      & width((r*canMat(i,j,n,R)) * A) = width A
      proof
        thus len(A * (r*canMat(i,j,n,R))) = n by MATRIX_0:24
          .= len((r*canMat(i,j,n,R)) * A) by MATRIX_0:24;
        thus len((r*canMat(i,j,n,R)) * A) = n by MATRIX_0:24
                                         .= len A by MATRIX_0:24;
        thus width(A * (r*canMat(i,j,n,R))) = n by MATRIX_0:24
          .= width((r*canMat(i,j,n,R)) * A) by MATRIX_0:24;
        len A = n by MATRIX_0:24
             .= width (r*canMat(i,j,n,R)) by MATRIX_0:24;
        hence width((r*canMat(i,j,n,R)) * A) = width A by MATRIX_3:def 4;
      end;
      A6: A * (1.(R,n) + r*canMat(i,j,n,R))
       = (A * 1.(R,n)) + (A * (r*canMat(i,j,n,R))) by A2,MATRIX_4:62
      .= A + (A * (r*canMat(i,j,n,R))) by MATRIX_3:19;
      (1.(R,n) + r*canMat(i,j,n,R)) * A
       = (1.(R,n) * A) + ((r*canMat(i,j,n,R)) * A) by A3,MATRIX_4:63
      .= A + (r*canMat(i,j,n,R)) * A by MATRIX_3:18;
      then A + ((r*canMat(i,j,n,R)) * A)
       = (A * (r*canMat(i,j,n,R))) + A by A4,A6,MATRIX_1:3;
      then ((r*canMat(i,j,n,R)) * A) + A = (A * (r*canMat(i,j,n,R))) + A
      by MATRIX_1:3;
      hence A * (r*canMat(i,j,n,R)) = (r*canMat(i,j,n,R)) * A by A5,MATRIX_4:4;
    end;
    assume A * (r*canMat(i,j,n,R)) = (r*canMat(i,j,n,R)) * A;
    then A + A * (r*canMat(i,j,n,R))
     = 1.(R,n) * A + (r*canMat(i,j,n,R)) * A by MATRIX_3:18;
    then A * 1.(R,n) + A * (r*canMat(i,j,n,R))
     = 1.(R,n) * A + (r*canMat(i,j,n,R)) * A by MATRIX_3:19
    .= (1.(R,n) + (r*canMat(i,j,n,R))) * A by A3,MATRIX_4:63;
    hence (1.(R,n) + (r*canMat(i,j,n,R))) * A
    = A * (1.(R,n) + (r*canMat(i,j,n,R))) by A2,MATRIX_4:62;
  end;
  suppose n = 0; :: degenerate case
    hence thesis by MATRIX_0:45;
  end;
end;

theorem Th59:
  for i,j being Nat
  for A being Matrix of n,R
  holds A * (1.(R,n) + canMat(i,j,n,R)) = (1.(R,n) + canMat(i,j,n,R)) * A
  iff A * canMat(i,j,n,R) = canMat(i,j,n,R) * A
proof
  let i,j be Nat;
  let A be Matrix of n,R;
  (1.R)*canMat(i,j,n,R) = canMat(i,j,n,R);
  hence thesis by Th58;
end;

:: Now we can prove canMat(i,j,n,R) is triangular when i <> j
theorem Th60:
  for i,j being Nat st i > j
  holds canMat(i,j,n,R) is lower_triangular
proof
  let i,j be Nat;
  assume A1: i > j;
    let i9,j9 be Nat;
    assume A2: [i9,j9] in Indices canMat(i,j,n,R);
    assume i9 < j9;
    then i9 = i & j9 = j implies contradiction by A1;
    then [i,j] <> [i9,j9] by XTUPLE_0:1;
    hence canMat(i,j,n,R) * (i9,j9) = 0.R by A2,Def1;
end;

theorem Th61:
  for i,j being Nat st i < j
  holds canMat(i,j,n,R) is upper_triangular
proof
  let i,j be Nat;
  assume A1: i < j;
    let i9,j9 be Nat;
    assume A2: [i9,j9] in Indices canMat(i,j,n,R);
    assume i9 > j9;
    then i9 = i & j9 = j implies contradiction by A1;
    then [i,j] <> [i9,j9] by XTUPLE_0:1;
    hence canMat(i,j,n,R) * (i9,j9) = 0.R by A2,Def1;
end;

theorem Th62:
  for i,j being Nat st i > j
  for r being Element of R
  holds r*canMat(i,j,n,R) is lower_triangular
proof
  let i,j be Nat;
  assume A1: i > j;
  let r be Element of R;
    let i9,j9 be Nat;
    assume A2: [i9,j9] in Indices (r*canMat(i,j,n,R));
    assume A3: i9 < j9;
    A4: [i9,j9] in Indices canMat(i,j,n,R) by A2,MATRIX_0:26;
    thus (r*canMat(i,j,n,R)) * (i9,j9)
     = r * (canMat(i,j,n,R) * (i9,j9)) by A4,MATRIX_3:def 5
    .= r * (0.R) by A1,A3,A4,Th60,MATRIX_1:def 13
    .= 0.R;
end;

theorem Th63:
  for i,j being Nat st i < j
  for r being Element of R
  holds r*canMat(i,j,n,R) is upper_triangular
proof
  let i,j be Nat;
  assume A1: i < j;
  let r be Element of R;
    let i9,j9 be Nat;
    assume A2: [i9,j9] in Indices (r*canMat(i,j,n,R));
    assume A3: i9 > j9;
    A4: [i9,j9] in Indices canMat(i,j,n,R) by A2,MATRIX_0:26;
    hence (r*canMat(i,j,n,R)) * (i9,j9)
     = r * (canMat(i,j,n,R) * (i9,j9)) by MATRIX_3:def 5
    .= r * (0.R) by A1,A3,A4,Th61,MATRIX_1:def 12
    .= 0.R;
end;

theorem
  for i,j being Nat st i > j
  for r being Element of R
  holds 1.(R,n) + r*canMat(i,j,n,R) is lower_triangular
proof
  let i,j be Nat;
  assume A1: i > j;
  let r be Element of R;
  set M = 1.(R,n) + r*canMat(i,j,n,R);
    let i9,j9 be Nat;
    assume A2: [i9,j9] in Indices M;
    assume A3: i9 < j9;
    A4: [i9,j9] in Indices 1.(R,n) by A2,MATRIX_0:26;
    A5: [i9,j9] in Indices (r*canMat(i,j,n,R)) by A2,MATRIX_0:26;
    A6: (r*canMat(i,j,n,R)) is lower_triangular by A1,Th62;
    thus M * (i9,j9)
     = (1.(R,n) * (i9,j9)) + (r*canMat(i,j,n,R))*(i9,j9) by A4,MATRIX_1:def 8
    .= (1.(R,n) * (i9,j9)) + 0.R by A3,A5,A6
    .= 0.R by A3,A4,MATRIX_1:def 3;
end;

theorem
  for i,j being Nat st i < j
  for r being Element of R
  holds 1.(R,n) + r*canMat(i,j,n,R) is upper_triangular
proof
  let i,j be Nat;
  assume A1: i < j;
  let r be Element of R;
  set M = 1.(R,n) + r*canMat(i,j,n,R);
    let i9,j9 be Nat;
    assume A2: [i9,j9] in Indices M;
    assume A3: i9 > j9;
    A4: [i9,j9] in Indices 1.(R,n) by A2,MATRIX_0:26;
    A5: [i9,j9] in Indices (r*canMat(i,j,n,R)) by A2,MATRIX_0:26;
    A6: r*canMat(i,j,n,R) is upper_triangular by A1,Th63;
    thus M * (i9,j9)
     = (1.(R,n) * (i9,j9)) + (r*canMat(i,j,n,R))*(i9,j9) by A4,MATRIX_1:def 8
    .= (1.(R,n) * (i9,j9)) + 0.R by A3,A5,A6
    .= 0.R by A3,A4,MATRIX_1:def 3;
end;

theorem Th66:
  for i,j being Nat st i > j
  for r being Element of R
  holds canMat(i,j,n,R)*r is lower_triangular
proof
  let i,j be Nat;
  assume A1: i > j;
  let r be Element of R;
    let i9,j9 be Nat;
    assume A2: [i9,j9] in Indices (canMat(i,j,n,R)*r);
    assume A3: i9 < j9;
    A4: [i9,j9] in Indices canMat(i,j,n,R) by A2,MATRIX_0:26;
    thus (canMat(i,j,n,R) * r) * (i9,j9)
     = (canMat(i,j,n,R) * (i9,j9)) * r by A4,MATRIX_3:def 6
    .= (0.R) * r by A1,A3,A4,Th60,MATRIX_1:def 13
    .= 0.R;
end;

theorem Th67:
  for i,j being Nat st i < j
  for r being Element of R
  holds canMat(i,j,n,R)*r is upper_triangular
proof
  let i,j be Nat;
  assume A1: i < j;
  let r be Element of R;
    let i9,j9 be Nat;
    assume A2: [i9,j9] in Indices (canMat(i,j,n,R)*r);
    assume A3: i9 > j9;
    A4: [i9,j9] in Indices canMat(i,j,n,R) by A2,MATRIX_0:26;
    thus (canMat(i,j,n,R)*r) * (i9,j9)
     = (canMat(i,j,n,R) * (i9,j9)) * r by A4,MATRIX_3:def 6
    .= (0.R) * r by A1,A3,A4,Th61,MATRIX_1:def 12
    .= 0.R;
end;

theorem
  for i,j being Nat st i > j
  for r being Element of R
  holds 1.(R,n) + canMat(i,j,n,R)*r is lower_triangular
proof
  let i,j be Nat;
  assume A1: i > j;
  let r be Element of R;
  set M = 1.(R,n) + canMat(i,j,n,R)*r;
    let i9,j9 be Nat;
    assume A2: [i9,j9] in Indices M;
    assume A3: i9 < j9;
    A4: [i9,j9] in Indices 1.(R,n) by A2,MATRIX_0:26;
    A5: [i9,j9] in Indices (canMat(i,j,n,R)*r) by A2,MATRIX_0:26;
    A6: canMat(i,j,n,R)*r is lower_triangular by A1,Th66;
    thus M * (i9,j9)
     = (1.(R,n) * (i9,j9)) + (canMat(i,j,n,R)*r)*(i9,j9) by A4,MATRIX_1:def 8
    .= (1.(R,n) * (i9,j9)) + 0.R by A3,A5,A6
    .= 0.R by A3,A4,MATRIX_1:def 3;
end;

theorem
  for i,j being Nat st i < j
  for r being Element of R
  holds 1.(R,n) + canMat(i,j,n,R)*r is upper_triangular
proof
  let i,j be Nat;
  assume A1: i < j;
  let r be Element of R;
  set M = 1.(R,n) + canMat(i,j,n,R)*r;
    let i9,j9 be Nat;
    assume A2: [i9,j9] in Indices M;
    assume A3: i9 > j9;
    A4: [i9,j9] in Indices 1.(R,n) by A2,MATRIX_0:26;
    A5: [i9,j9] in Indices (canMat(i,j,n,R)*r) by A2,MATRIX_0:26;
    A6: canMat(i,j,n,R)*r is upper_triangular by A1,Th67;
    thus M * (i9,j9)
     = (1.(R,n) * (i9,j9)) + (canMat(i,j,n,R)*r)*(i9,j9) by A4,MATRIX_1:def 8
    .= (1.(R,n) * (i9,j9)) + 0.R by A3,A5,A6
    .= 0.R by A3,A4,MATRIX_1:def 3;
end;

begin :: Matrix-membered structures and sets

reserve L for non empty doubleLoopStr;

definition
  let L be non empty 1-sorted;
  let n;
  let IT be set;
  attr IT is (n,L)-matrix-membered means :Def3:
  for x being object st x in IT holds x is Matrix of n,L;
end;

registration
  let L,n;
  cluster n-Matrices_over L -> (n, L)-matrix-membered;
  coherence
  proof
    for x being object
    holds x in n-Matrices_over L iff x is Matrix of n,L
    proof
      let x be object;
      x is Element of n-Matrices_over L iff x is Matrix of n,L by MATRIX_1:2;
      hence thesis;
    end;
    hence thesis;
  end;
end;

theorem Th70:
  for L being non empty 1-sorted
  holds n-tuples_on (n-tuples_on the carrier of L) is (n,L)-matrix-membered
proof
  let L be non empty 1-sorted;
  for X being object
  st X in n-tuples_on (n-tuples_on the carrier of L)
  holds X is Matrix of n,L
  proof
    let X be object;
    assume X in n-tuples_on (n-tuples_on the carrier of L);
    then reconsider X as Element of n-tuples_on (n-tuples_on the carrier of L);
    A1: len X = n by CARD_1:def 7;
    ex m being Nat st
    for y being object st y in rng X
    ex q being FinSequence of L
    st y = q & len q = m
    proof
      take n;
      let y be object;
      assume y in rng X;
      then reconsider q=y as Element of n-tuples_on the carrier of L;
      reconsider q as FinSequence of L;
      take q;
      thus thesis by CARD_1:def 7;
    end;
    then reconsider X as Matrix of the carrier of L by MATRIX_0:9;
    for q being FinSequence of L st q in rng X
    holds len q = n
    proof
      let q be FinSequence of L;
      A2: rng X c= n-tuples_on the carrier of L by FINSEQ_1:def 4;
      assume q in rng X;
      then reconsider q as Element of n-tuples_on the carrier of L by A2;
      len q = n by CARD_1:def 7;
      hence thesis;
    end;
    hence thesis by A1,MATRIX_0:def 2;
  end;
  hence thesis;
end;

registration
  let L be non empty 1-sorted;
  let n;
  cluster non empty (n,L)-matrix-membered for set;
  existence
  proof
    take A = n-tuples_on (n-tuples_on the carrier of L);
    thus thesis by Th70;
  end;
end;

definition
  let L be non empty 1-sorted;
  let n;
  let A be non empty (n, L)-matrix-membered set;
  redefine mode Element of A -> Matrix of n,L;  :: redefines Element (SUBSET_1, definition)
  correctness by Def3;
end;

definition
  let L be non empty 1-sorted;
  let n;
  let IT be 1-sorted;
  attr IT is (n,L)-matrix-membered means
  the carrier of IT is (n,L)-matrix-membered;
end;

theorem
  for S being 1-sorted holds
  the carrier of S c= n-Matrices_over L iff S is (n,L)-matrix-membered
proof
  let S be 1-sorted;
  hereby
    assume the carrier of S c= n-Matrices_over L;
    then the carrier of S is (n,L)-matrix-membered by MATRIX_1:2;
    hence S is (n,L)-matrix-membered;
  end;
  assume A1: S is (n,L)-matrix-membered;
  for x being object st x in the carrier of S
  holds x in n-Matrices_over L
  proof
    let x be object;
    assume x in the carrier of S;
    then x is Matrix of n,L by A1,Def3;
    then x is Element of n-Matrices_over L by MATRIX_1:2;
    hence x in n-Matrices_over L;
  end;
  hence the carrier of S c= n-Matrices_over L by TARSKI:def 3;
end;

registration
  let L be non empty 1-sorted;
  let n;
  cluster non empty (n,L)-matrix-membered for 1-sorted;
  existence
  proof
    take A = 1-sorted (# n-tuples_on (n-tuples_on the carrier of L) #);
    thus thesis by Th70;
  end;
end;

registration
  let L,n;
  cluster strict non empty (n,L)-matrix-membered for 1-sorted;
  existence
  proof
    take A = 1-sorted (# n-Matrices_over L #);
    thus A is strict;
    thus A is non empty;
    thus A is (n,L)-matrix-membered;
  end;
end;

begin :: Matrix rings

definition
  let n;
  let L; :: be non empty doubleLoopStr;
  func matrix_mult (n,L) -> BinOp of n-Matrices_over L means :Def5:
  for A,B being Element of n-Matrices_over L holds it.(A,B) = A*B;
  existence
  proof
    set F1=n-Matrices_over L;
    defpred P[object, object, object] means ex X,Y,Z being Matrix of n,L
    st $1=X & $2=Y & $3=Z & Z = X*Y;
    A1: for x,y being object st x in F1 & y in F1 ex z being object st
    (z in F1 & P[x,y,z])
    proof
      let x,y be object;
      assume x in F1 & y in F1;
      then reconsider A=x, B=y as Matrix of n,L by MATRIX_1:2;
      width A = n & len B = n by MATRIX_0:24;
      then reconsider B as Matrix of width A,n,L;
      take z = A*B;
      z is Element of F1 by MATRIX_1:2;
      hence thesis;
    end;
    consider f being Function of [: F1, F1 :],F1 such that
    A2: for x,y being object st x in F1 & y in F1 holds P[x, y, f.(x,y)]
    from BINOP_1:sch 1(A1);
    reconsider f as BinOp of F1;
    take f;
    for A,B being Element of F1 holds f.(A,B) = A*B
    proof
      let A,B be Element of F1;
      P[A, B, f.(A,B)] by A2;
      hence f.(A,B) = A*B;
    end;
    hence thesis;
  end;
  uniqueness
  proof
    let f,g be BinOp of n-Matrices_over L;
    set F1=n-Matrices_over L;
    assume A3: for A,B being Element of F1 holds f.(A,B) = A*B;
    assume A4: for A,B being Element of F1 holds g.(A,B) = A*B;
    for A,B being Element of F1 holds f.(A,B) = g.(A,B)
    proof
      let A,B be Element of F1;
      thus f.(A,B) = A*B by A3
                  .= g.(A,B) by A4;
    end;
    hence thesis by BINOP_1:2;
  end;
end;

definition
  let n,L;
  func matrix_add (n,L) -> BinOp of n-Matrices_over L means :Def6:
  for A,B being Element of n-Matrices_over L holds it.(A,B) = A + B;
  existence
  proof
    set F1=n-Matrices_over L;
    defpred P[object, object, object] means ex X,Y,Z being Matrix of n,L
    st $1=X & $2=Y & $3=Z & Z = X+Y;
    A1: for x,y being object st x in F1 & y in F1 ex z being object st
    (z in F1 & P[x,y,z])
    proof
      let x,y be object;
      assume x in F1 & y in F1;
      then reconsider A=x, B=y as Matrix of n,L by MATRIX_1:2;
      take z = A + B;
      z is Element of F1 by MATRIX_1:2;
      hence z in F1;
      thus P[x, y, z];
    end;
    consider f being Function of [: F1, F1 :],F1 such that
    A2: for x,y being object st x in F1 & y in F1 holds P[x, y, f.(x,y)]
    from BINOP_1:sch 1(A1);
    reconsider f as BinOp of F1;
    take f;
    for A,B being Element of F1 holds f.(A,B) = A + B
    proof
      let A,B be Element of F1;
      P[A, B, f.(A,B)] by A2;
      hence f.(A,B) = A + B;
    end;
    hence thesis;
  end;
  uniqueness
  proof
    let f,g be BinOp of n-Matrices_over L;
    set F1=n-Matrices_over L;
    assume A3: for A,B being Element of F1 holds f.(A,B) = A+B;
    assume A4: for A,B being Element of F1 holds g.(A,B) = A+B;
    for A,B being Element of F1 holds f.(A,B) = g.(A,B)
    proof
      let A,B be Element of F1;
      thus f.(A,B) = A+B by A3
                  .= g.(A,B) by A4;
    end;
    hence thesis by BINOP_1:2;
  end;
end;

notation
   let L,n;
   synonym One(L,n) for 1.(L,n);
   synonym Zero(L,n) for 0.(L,n);
end;

definition
  let L,n;
  redefine func One(L,n) -> Element of n-Matrices_over L;  :: redefines One (MATGRP_0, synonym) → 1. (MATRIX_1, definition)
  correctness by MATRIX_1:2;
  redefine func Zero(L,n) -> Element of n-Matrices_over L;  :: redefines Zero (MATGRP_0, synonym) → 0. (MATRIX_1, definition)
  correctness;
end;

definition
  let L,n;
  func Matrix_ring(n, L) -> strict doubleLoopStr equals
  doubleLoopStr (# (n-Matrices_over L), matrix_add(n,L),
    matrix_mult(n,L),
    One(L,n),
    Zero(L,n) #);
  coherence;
end;

registration
  let L, n;
  cluster Matrix_ring(n, L) -> strict non empty (n,L)-matrix-membered;
  coherence;
end;

theorem Th72:
  for x being object
  holds x is Element of Matrix_ring(n,L) iff x is Matrix of n,L by MATRIX_1:2;

registration
  let L;
  cluster Matrix_ring(0, L) -> trivial;
  coherence
  proof
    for x,y being Element of Matrix_ring(0,L)
    holds x = y
    proof
      let x,y be Element of Matrix_ring(0,L);
      x is Matrix of 0,L & y is Matrix of 0,L;
      hence x = y by MATRIX_0:45;
    end;
    hence thesis by STRUCT_0:def 10;
  end;
end;

theorem Th73:
  for A,B being Matrix of n,L
  for X,Y being Element of Matrix_ring(n,L)
  st A = X & B = Y
  holds A + B = X + Y by Def6;

theorem
  for X,Y being Matrix of n,L
  for x,y being Element of n-Matrices_over L
  st X = x & Y = y
  holds X * Y = matrix_mult(n,L).(x,y) by Def5;

theorem Th75:
  for A,B being Matrix of n,L
  for X,Y being Element of Matrix_ring(n,L)
  st A = X & B = Y
  holds A * B = X * Y by Def5;

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

theorem
  1.(L,n) is Element of Matrix_ring(n,L);

theorem
  0.(L,n) is Element of Matrix_ring(n,L);

:: When (the addLoopStr of R) is an Abelian Group, Matrix_ring(n,R)
:: forms an Abelian group under addition
registration
  let n;
  let R be right_complementable Abelian add-associative right_zeroed
  non empty doubleLoopStr;
  cluster Matrix_ring(n,R) -> add-associative;
  coherence
  proof
    for u,v,w being Element of Matrix_ring(n,R)
    holds (u + v) + w = u + (v + w)
    proof
      let u,v,w be Element of Matrix_ring(n,R);
      reconsider U=u,V=v,W=w as Matrix of n,R by Th72;
      set uv = u+v, vw = v + w, VW = V + W, UV = U + V;
      A1: uv = UV by Th73;
      A2: vw = VW by Th73;
      thus (u + v) + w = UV + W by A1,Th73
                      .= U + (V + W) by MATRIX_1:4
                      .= u + (v + w) by A2,Th73;
    end;
    hence thesis by RLVECT_1:def 3;
  end;
  cluster Matrix_ring(n,R) -> right_zeroed;
  coherence
  proof
    for v being Element of Matrix_ring(n,R)
    holds v + (0.Matrix_ring(n,R)) = v
    proof
      let v be Element of Matrix_ring(n,R);
      reconsider V = v as Matrix of n,R by Th72;
      thus v + (0.Matrix_ring(n,R)) = V + 0.(R,n) by Th73
                                   .= v by MATRIX_1:5;
    end;
    hence thesis by RLVECT_1:def 4;
  end;
  cluster Matrix_ring(n,R) -> right_complementable;
  coherence
  proof
    for x being Element of Matrix_ring(n,R)
    holds x is right_complementable
    proof
      let x be Element of Matrix_ring(n,R);
      ex y being Element of Matrix_ring(n,R)
      st x + y = 0.(Matrix_ring(n,R))
      proof
        reconsider X = x as Matrix of n,R by Th72;
        set Y = - X;
        reconsider y = Y as Element of Matrix_ring(n,R) by Th72;
        take y;
        thus x + y = X + Y by Th73
                  .= 0.(Matrix_ring(n,R)) by MATRIX_1:6;
      end;
      hence x is right_complementable by ALGSTR_0:def 11;
    end;
    hence thesis by ALGSTR_0:def 16;
  end;
  cluster Matrix_ring(n,R) -> Abelian;
  coherence
  proof
    for v,w being Element of Matrix_ring(n,R)
    holds v + w = w + v
    proof
      let v,w be Element of Matrix_ring(n,R);
      reconsider V = v, W = w as Matrix of n,R by Th72;
      thus v + w = V + W by Th73
                .= W + V by MATRIX_1:3
                .= w + v by Th73;
    end;

    hence thesis by RLVECT_1:def 2;
  end;
end;

:: N.B.: the condition that R is a ring could be weakened, if...
registration
  let n, R;
  ::: MATRIX_3:18,19 are weakened to well-unital semirings
  cluster Matrix_ring(n,R) -> well-unital;
  coherence
  proof
    for x being Element of Matrix_ring(n,R)
    holds x * (1.(Matrix_ring(n,R))) = x
    & (1.(Matrix_ring(n,R))) * x = x
    proof
      let x be Element of Matrix_ring(n,R);
      reconsider X = x as Matrix of n,R by Th72;
      thus x * (1.(Matrix_ring(n,R))) = X * (1.(R,n)) by Th75
                                     .= x by MATRIX_3:19;
      thus (1.(Matrix_ring(n,R))) * x = (1.(R,n)) * X by Th75
                                     .= x by MATRIX_3:18;
    end;
    hence thesis by VECTSP_1:def 6;
  end;
  ::: MATRIX_4:62,63 are weakened to distributive semirings
  cluster Matrix_ring(n,R) -> distributive;
  coherence
  proof
    for x,y,z being Element of Matrix_ring(n,R)
    holds x * (y + z) = (x * y) + (x * z)
    & (y + z) * x = (y * x) + (z * x)
    proof
      let x,y,z be Element of Matrix_ring(n,R);
      reconsider X = x, Y = y, Z = z as Matrix of n,R by Th72;
      reconsider YZ = Y + Z as Matrix of n,R;
      A1: len Y = n & width Y = n & width Z = n & len Z = n & width X = n
      & len X = n by MATRIX_0:24;
      A2: x*y = X*Y & x*z = X*Z by Th75;
      A3: Y + Z = y + z by Th73;
      hence x * (y + z) = X * YZ by Th75
                       .= (X * Y) + (X * Z) by A1,MATRIX_4:62
                       .= (x * y) + (x * z) by A2,Th73;
      A4: y*x = Y*X & z*x = Z*X by Th75;
      thus (y + z) * x = YZ * X by A3,Th75
                      .= (Y * X) + (Z * X) by A1,MATRIX_4:63
                      .= (y * x) + (z * x) by A4,Th73;
    end;
    hence thesis by VECTSP_1:def 7;
  end;
  ::: MATRIX_3:33 is weakened to associative semirings
  cluster Matrix_ring(n,R) -> associative;
  coherence
  proof
    for x,y,z being Element of Matrix_ring(n,R)
    holds (x * y) * z = x * (y * z)
    proof
      let x,y,z be Element of Matrix_ring(n,R);
      reconsider X = x, Y = y, Z = z as Matrix of n,R by Th72;
      set XY = X*Y, YZ=Y*Z;
      A5: x * y = X*Y & y*z = Y*Z by Th75;
      A6: len Y = n & width Y = n & width Z = n & len Z = n & width X = n
      & len X = n by MATRIX_0:24;
      thus (x * y) * z = XY * Z by A5,Th75
                      .= X*YZ by A6,MATRIX_3:33
                      .= x * (y * z) by A5,Th75;
    end;
    hence thesis by GROUP_1:def 3;
  end;
end;

theorem Th79:
  Matrix_ring(1,R), R are_isomorphic
proof
  set UR = the carrier of R;
  defpred P[object,object] means
  $2 = <*<* $1 *>*>;
  A1: for x being Element of UR
  ex y being Element of 1-Matrices_over R
  st P[x,y]
  proof
    let x be Element of UR;
    reconsider x0 = x as Element of R;
    consider y being Matrix of 1,R such that
    A2: y = <*<* x0 *>*>;
    reconsider y as Element of 1-Matrices_over R by MATRIX_1:2;
    take y;
    thus P[x,y] by A2;
  end;

  consider f being Function of UR, 1-Matrices_over R such that
  A3: for r being Element of UR holds P[r, f.r]
  from FUNCT_2:sch 3(A1);
  reconsider f as Function of R, Matrix_ring(1,R);
  A4: f is onto
  proof
    for y being object
    st y in the carrier of Matrix_ring(1,R)
    ex x being object st x in UR & y = f.x
    proof
      let y be object;
      assume y in the carrier of Matrix_ring(1,R);
      then reconsider M = y as Matrix of 1,R by Th72;
      take x = M * (1,1);
      thus x in UR;
      thus y = <* <* x *> *> by Th33
            .= f.x by A3;
    end;
    then rng f = the carrier of Matrix_ring(1,R) by FUNCT_2:10;
    hence thesis by FUNCT_2:def 3;
  end;
  A5: f is one-to-one
  proof
    for a,b being Element of R st f.a = f.b holds a = b
    proof
      let a,b be Element of R;
      assume A6: f.a = f.b;
      A7: <* <* a *> *> = f.b by A3,A6
                       .= <* <* b *> *> by A3;
      {[1, <*a*>]} = <*<* a *>*> by FINSEQ_1:37
                  .= {[1,<*b*>]} by A7,FINSEQ_1:37;
      then [1,<*a*>] = [1,<*b*>] by ZFMISC_1:3;
      then A8: <*a*> = <*b*> by XTUPLE_0:1;
      {[1, a]} = <*a*> by FINSEQ_1:37
              .= {[1,b]} by A8,FINSEQ_1:37;
      then [1,a] = [1,b] by ZFMISC_1:3;
      hence a = b by XTUPLE_0:1;
    end;
    hence thesis by GROUP_6:1;
  end;
  f is linear
  proof
    for x,y being Element of R
    holds f.(x + y) = (f.x) + (f.y)
    proof
      let x,y be Element of R;
      reconsider M1=f.x, M2=f.y as Matrix of 1,R by Th72;
      A9: M1 = <*<* x *>*> & M2 = <*<* y *>*> by A3;
      thus (f.x) + (f.y) = M1 + M2 by Th73
                        .= <*<* (x + y) *>*> by A9,Th36
                        .= f.(x + y) by A3;
    end;
    then A10: f is additive by VECTSP_1:def 20;
    now
      let x,y be Element of R;
      reconsider M1=f.x, M2=f.y as Matrix of 1,R by Th72;
      A11: M1 = <*<* x *>*> & M2 = <*<* y *>*> by A3;
      thus (f.x) * (f.y) = M1 * M2 by Th75
                        .= <*<* (x * y) *>*> by A11,Th35
                        .= f.(x * y) by A3;
    end;
    then A12: f is multiplicative by GROUP_6:def 6;
    f is unity-preserving
    proof
      f.(1_R) = <*<* (1_R) *>*> by A3
             .= 1_(Matrix_ring(1,R)) by Th34;
      hence f is unity-preserving by GROUP_1:def 13;
    end;
    hence f is linear by A10,A12;
  end;
  hence thesis by A4,A5,QUOFIELD:def 23;
end;

begin :: Extension of underlying ring on the Matrix ring

theorem Th80:
  for D,E being non empty set st D c= E
  for X being Matrix of D
  holds X is Matrix of E
proof
  let D,E be non empty set;
  assume A1: D c= E;
  let X be Matrix of D;
  D * c= E * by A1,FINSEQ_1:62;
  then rng X c= E * by XBOOLE_1:1;
  hence X is Matrix of E by FINSEQ_1:def 4;
end;

theorem Th81:
  for m,n being Nat
  for D,E being non empty set st D c= E
  for X being Matrix of m,n,D
  holds X is Matrix of m,n,E
proof
  let m,n be Nat;
  let D,E be non empty set;
  assume A1: D c= E;
  let X be Matrix of m,n,D;
  reconsider x = X as Matrix of E by A1,Th80;
  (len x = m & ( for p being FinSequence of E st p in rng x holds
  len p = n))
  proof
    thus len x = m by MATRIX_0:def 2;
    let p be FinSequence of E;
    assume A2: p in rng x;
    then p in rng X;
    then reconsider p9 = p as FinSequence of D by FINSEQ_1:def 11;
    p9 in rng X by A2;
    hence thesis by MATRIX_0:def 2;
  end;
  hence thesis by MATRIX_0:def 2;
end;

theorem Th82:
  for X being Matrix of n,S
  holds X is Matrix of n,R
proof
  let X be Matrix of n,S;
  set US = the carrier of S, UR = the carrier of R;
  the carrier of S c= the carrier of R
  & the carrier of S is non empty & the carrier of R is non empty
  by C0SP1:def 3;
  hence X is Matrix of n,R by Th81;
end;

theorem Th83:
  for S1,S2 being non empty 1-sorted
  for X being Matrix of n,S2
  for Y being Matrix of n,S1
  holds (for i,j being Nat st [i,j] in Indices X
         holds X * (i,j) = Y * (i,j))
  iff X = Y
proof
  let S1,S2 be non empty 1-sorted;
  let X be Matrix of n,S2;
  let Y be Matrix of n,S1;
  thus (for i,j being Nat st [i,j] in Indices X holds X * (i,j) = Y * (i,j))
       implies X = Y
  proof
    assume A1: for i,j being Nat st [i,j] in Indices X
    holds X * (i,j) = Y * (i,j);

    A2: dom X = Seg len X by FINSEQ_1:def 3
             .= Seg n by MATRIX_0:25
             .= Seg len Y by MATRIX_0:25
             .= dom Y by FINSEQ_1:def 3;
    for i being Nat st i in dom X
    holds X.i = Y.i
    proof
      let i be Nat;
      assume A3: i in dom X;
      per cases;
      suppose n = 0;
        then len X = 0 by MATRIX_0:25;
        then {} = Seg len X
               .= dom X by FINSEQ_1:def 3;
        hence thesis by A3;
      end;
      suppose n > 0;
        then A4: len X > 0 & len Y > 0 by MATRIX_0:25;
        A5: X.i in rng X by A3,FUNCT_1:def 3;
        then reconsider p = X.i as FinSequence of S2 by FINSEQ_1:def 11;
        A6: Y.i in rng Y by A2,A3,FUNCT_1:def 3;
        then reconsider q = Y.i as FinSequence of S1 by FINSEQ_1:def 11;
        A7: dom p = Seg len p by FINSEQ_1:def 3
                 .= Seg width X by A5,A4,MATRIX_0:def 3
                 .= Seg n by MATRIX_0:24
                 .= Seg width Y by MATRIX_0:24
                 .= Seg len q by A6,A4,MATRIX_0:def 3
                 .= dom q by FINSEQ_1:def 3;
        for j being Nat st j in dom p holds p.j = q.j
        proof
          let j be Nat;
          assume A8: j in dom p;
          A9: [i,j] in Indices X
          proof
            dom p = Seg len p by FINSEQ_1:def 3
                 .= Seg width X by A5,A4,MATRIX_0:def 3;
            then [i,j] in [:dom X,Seg(width X):] by A3,A8,ZFMISC_1:87;
            hence thesis by MATRIX_0:def 4;
          end;
          Indices X = [:Seg n,Seg n:] by MATRIX_0:24
                   .= Indices Y by MATRIX_0:24;
          then
A10:      ex q9 being FinSequence of S1 st q9 = Y.i & Y * (i,j) = q9.j
          by A9,MATRIX_0:def 5;
          ex p9 being FinSequence of S2 st p9 = X.i & X * (i,j) = p9.j
          by A9,MATRIX_0:def 5;
          hence p.j = q.j by A1,A9,A10;
        end;
        hence X.i = Y.i by A7,FINSEQ_1:13;
      end;
    end;
    hence X = Y by A2,FINSEQ_1:13;
  end;
  assume A11: X = Y;
  let i,j be Nat;
  assume A12: [i,j] in Indices X;
  then consider q being FinSequence of S1 such that
  A13: q = Y.i & Y * (i,j) = q.j by A11,MATRIX_0:def 5;
  consider p being FinSequence of S2 such that
  A14: p = X.i & X * (i,j) = p.j by A12,MATRIX_0:def 5;
  thus thesis by A11,A13,A14;
end;

theorem Th85:
  n-Matrices_over S c= n-Matrices_over R
proof
  for x being object
  st x in n-Matrices_over S
  holds x in n-Matrices_over R
  proof
    let x be object;
    assume x in n-Matrices_over S;
    then x is Matrix of n,S by MATRIX_1:2;
    then x is Matrix of n,R by Th82;
    then x is Element of n-Matrices_over R by MATRIX_1:2;
    hence x in n-Matrices_over R;
  end;
  hence thesis by TARSKI:def 3;
end;

theorem Th86:
  for a,b being Matrix of n,S
  for A,B being Matrix of n,R
  st a = A & b = B
  holds a + b = A + B
proof
  let a,b be Matrix of n,S;
  let A,B be Matrix of n,R;
  assume A1: a = A;
  assume A2: b = B;
  set LHS = a + b, RHS = A + B;
  for i,j being Nat st [i,j] in Indices LHS
  holds LHS * (i,j) = RHS * (i,j)
  proof
    let i,j be Nat;
    assume A3: [i,j] in Indices LHS;
    A4: Indices a = [:Seg n,Seg n:] by MATRIX_0:24
                 .= Indices LHS by MATRIX_0:24;
    A5: Indices A = [:Seg n,Seg n:] by MATRIX_0:24
                 .= Indices LHS by MATRIX_0:24;
    A6: A * (i,j) + B * (i,j) = a * (i,j) + b * (i,j)
    proof
      A7: A * (i,j) = a * (i,j) by A1,A3,A5,Th83;
      Indices B = [:Seg n,Seg n:] by MATRIX_0:24
               .= Indices LHS by MATRIX_0:24;
      then B * (i,j) = b * (i,j) by A2,A3,Th83;
      hence thesis by A7,FIELD_6:15;
    end;
    thus LHS * (i,j) = (a * (i,j)) + (b * (i,j)) by A3,A4,MATRIX_1:def 8
                    .= (A + B) * (i,j) by A3,A5,A6,MATRIX_1:def 8;
  end;
  hence thesis by Th83;
end;

theorem Th87:
  matrix_add(n,S) = matrix_add(n,R) || (n-Matrices_over S)
proof
  set US = n-Matrices_over S, UR = n-Matrices_over R;
  A1: US c= UR by Th85;
  then A2: [:US,US:] c= [:UR,UR:] by ZFMISC_1:96;
  A3:  (matrix_add(n,R) || (n-Matrices_over S)) is Function of [:US,US:],UR
  by A2,FUNCT_2:32;
  A4: matrix_add(n,S) is Function of [:US,US:],UR by A1,FUNCT_2:7;
  for x,y being Element of n-Matrices_over S
  holds matrix_add(n,S).(x,y) = (matrix_add(n,R) || (n-Matrices_over S)).(x,y)
  proof
    let x,y be Element of n-Matrices_over S;
    reconsider a = x, b = y as Matrix of n,S;
    reconsider A = a, B = b as Matrix of n,R by Th82;
    reconsider X = x, Y = y as Element of n-Matrices_over R
    by Th85,TARSKI:def 3;
    thus matrix_add(n,S).(x,y) = a + b by Def6
                              .= A + B by Th86
                              .= matrix_add(n,R).(X,Y) by Def6
                              .= (matrix_add(n,R) || (n-Matrices_over S)).(x,y)
                              by FUNCT_1:49,ZFMISC_1:87;
  end;
  hence thesis by A3,A4,BINOP_1:2;
end;

theorem Th88:
  for a being Matrix of n,S
  for A being Matrix of n,R
  st a = A
  for i being Nat st i in dom a
  holds Line(a, i) = Line(A, i)
proof
  let a be Matrix of n,S;
  let A be Matrix of n,R;
  assume A1: a = A;
  let i be Nat;
  assume A2: i in dom a;
  A3: dom Line(a,i) = Seg len Line(a,i) by FINSEQ_1:def 3
                   .= Seg width a by MATRIX_0:def 7;
  A4: Seg width A = Seg len Line(A,i) by MATRIX_0:def 7
                 .= dom Line(A,i) by FINSEQ_1:def 3;
  for j being Nat st j in dom Line(a,i)
  holds Line(a,i).j = Line(A,i).j
  proof
    let j be Nat;
    assume A5: j in dom Line(a,i);
    then [i,j] in [:dom a,Seg width a:] by A2,A3,ZFMISC_1:87;
    then A6: [i,j] in Indices a by MATRIX_0:def 4;
    thus Line(a,i).j = a * (i,j) by A3,A5,MATRIX_0:def 7
                    .= A * (i,j) by A1,A6,Th83
                    .= Line(A,i).j by A1,A3,A5,MATRIX_0:def 7;
  end;
  hence Line(a, i) = Line(A, i) by A1,A3,A4,FINSEQ_1:13;
end;

theorem Th89:
  for b being Matrix of n,S
  for B being Matrix of n,R
  st b = B
  for j being Nat st j in Seg width b
  holds Col(b, j) = Col(B, j)
proof
  let b be Matrix of n,S;
  let B be Matrix of n,R;
  assume A1: b = B;
  let j be Nat;
  assume A2: j in Seg width b;
  A3: dom Col(b, j) = Seg len Col(b,j) by FINSEQ_1:def 3
                   .= Seg len b by MATRIX_0:def 8;
  A4: dom Col(B, j) = Seg len Col(B,j) by FINSEQ_1:def 3
                   .= Seg len B by MATRIX_0:def 8;
  for i being Nat st i in dom Col(b, j)
  holds Col(b, j).i = Col(B, j).i
  proof
    let i be Nat;
    assume i in dom Col(b, j);
    then A5: i in dom b by A3,FINSEQ_1:def 3;
    then [i,j] in [:dom b, Seg(width b):] by A2,ZFMISC_1:87;
    then A6: [i,j] in Indices b by MATRIX_0:def 4;
    Indices b = [:Seg n,Seg n:] by MATRIX_0:24
             .= Indices B by MATRIX_0:24;
    then [i,j] in [:dom B, Seg(width B):] by A6,MATRIX_0:def 4;
    then A7: i in dom B & j in Seg(width B) by ZFMISC_1:87;
    thus Col(b, j).i = b * (i,j) by A5,MATRIX_0:def 8
                    .= B * (i,j) by A1,A6,Th83
                    .= Col(B, j).i by A7,MATRIX_0:def 8;
  end;
  hence thesis by A1,A3,A4,FINSEQ_1:13;
end;

theorem Th90:
  for a being FinSequence of S
  for A being FinSequence of R
  st a = A
  holds Sum a = Sum A
proof
  defpred P[Nat] means
  for a being FinSequence of S
  for A being FinSequence of R
  st a = A & len a = $1
  holds Sum a = Sum A;

  A1: P[0]
  proof
    let a be FinSequence of S;
    let A be FinSequence of R;
    assume A2: a = A & len a = 0;
    hence Sum a = 0.S by RLVECT_1:75
               .= 0.R by C0SP1:def 3
               .= Sum A by A2,RLVECT_1:75;
  end;
  A3: for k being Nat st P[k] holds P[k + 1]
  proof
    let k be Nat;
    assume A4: P[k];
:::    thus P[k + 1]
:::    proof
      let a be FinSequence of S;
      let A be FinSequence of R;
      assume A5: a = A & len a = k + 1;
      then consider a0 being FinSequence of S, aN being Element of S such that
      A6: a = a0 ^ <* aN *> by FINSEQ_2:19;
      consider A0 being FinSequence of R, AN being Element of R such that
      A7: A = A0 ^ <* AN *> by A5,FINSEQ_2:19;
      A8: a0 = A0 & aN = AN by A5,A7,A6,FINSEQ_2:17;
      k + 1 = (len a0) + 1 by A5,A6,FINSEQ_2:16;
      then A9: Sum a0 = Sum A0 by A4,A8;
      A10: Sum <* aN *> = aN by RLVECT_1:44
                       .= Sum <* AN *> by A8,RLVECT_1:44;
      thus Sum a = Sum (a0) + Sum(<*aN*>) by A6,RLVECT_1:41
                .= Sum (A0) + Sum(<*AN*>) by A9,A10,FIELD_6:15
                .= Sum A by A7,RLVECT_1:41;
:::    end;
  end;

  A11: for k being Nat holds P[k] from NAT_1:sch 2(A1, A3);

  let a be FinSequence of S;
  let A be FinSequence of R;
  assume A12: a = A;
  P[len a] by A11;
  hence Sum a = Sum A by A12;
end;

theorem Th91:
  for a,b being FinSequence of S
  for A,B being FinSequence of R
  st a = A & b = B
  holds mlt(a,b) = mlt(A,B)
proof
  let a,b be FinSequence of S;
  let A,B be FinSequence of R;
  assume A1: a = A;
  assume A2: b = B;
  A3: dom mlt(a,b) = dom mlt(A,B)
  proof
    mlt(a,b) = (the multF of S) .: (a,b) by FVSUM_1:def 7;
    then A4: len mlt(a,b) = min(len a, len b) by FINSEQ_2:71;
    mlt(A,B) = (the multF of R) .: (A,B) by FVSUM_1:def 7;
    then A5: len mlt(A,B) = min(len A, len B) by FINSEQ_2:71;
    thus dom mlt(a,b) = Seg len mlt(a,b) by FINSEQ_1:def 3
                     .= dom mlt(A,B) by A1,A2,A4,A5,FINSEQ_1:def 3;
  end;
  A6: for i,j,k being Nat
  st i in Seg min(j,k) holds i in Seg j & i in Seg k
  proof
    let i,j,k be Nat;
    assume i in Seg(min(j,k));
    then i in (Seg j) /\ (Seg k) by FINSEQ_2:2;
    hence thesis by XBOOLE_0:def 4;
  end;
  for i being Nat st i in dom mlt(a,b)
  holds mlt(a,b).i = mlt(A,B).i
  proof
    let i be Nat;
    assume A7: i in dom mlt(a,b);
    A8: mlt(a,b) = (the multF of S) .: (a,b) by FVSUM_1:def 7;
    i in Seg len mlt(a,b) by A7,FINSEQ_1:def 3;
    then i in Seg min(len a, len b) by A8,FINSEQ_2:71;
    then i in Seg len a & i in Seg len b by A6;
    then a1: i in dom a & i in dom b by FINSEQ_1:def 3;
    then reconsider ai = a.i, bi = b.i as Element of S by FUNCT_1:106;
    i in dom A & i in dom B by a1,A1,A2;
    then reconsider Ai = A.i, Bi = B.i as Element of R by FUNCT_1:106;
    thus mlt(a,b).i = ai * bi by A7,FVSUM_1:60
                   .= Ai * Bi by A1,A2,FIELD_6:16
                   .= mlt(A,B).i by A3,A7,FVSUM_1:60;
  end;
  hence mlt(a,b) = mlt(A,B) by A3,FINSEQ_1:13;
end;

theorem Th92:
  for a,b being Matrix of n,S
  for A,B being Matrix of n,R
  st a = A & b = B
  holds a * b = A * B
proof
  let a,b be Matrix of n,S;
  let A,B be Matrix of n,R;
  assume A1: a = A & b = B;
  set LHS = a * b, RHS = A * B;
  A2: width a = n by MATRIX_0:24
             .= len b by MATRIX_0:25;
  A3: width A = n by MATRIX_0:24
             .= len B by MATRIX_0:25;
  for i,j being Nat st [i,j] in Indices LHS
  holds LHS * (i,j) = RHS * (i,j)
  proof
    let i,j be Nat;
    assume A4: [i,j] in Indices LHS;
    A5: Indices LHS = [:(Seg n),(Seg n):] by MATRIX_0:24
                   .= Indices RHS by MATRIX_0:24;
    A6: i in dom a & j in Seg width b
    proof
      [i,j] in [:dom LHS,Seg width LHS:] by A4,MATRIX_0:def 4;
      then A7: i in dom LHS & j in Seg width LHS by ZFMISC_1:87;
      len LHS = len a by A2,MATRIX_3:def 4;
      then Seg len LHS = dom a by FINSEQ_1:def 3;
      hence i in dom a by A7,FINSEQ_1:def 3;
      thus thesis by A2,A7,MATRIX_3:def 4;
    end;
    then A8: Line(a,i) = Line(A,i) by A1,Th88;
    Col(b,j) = Col(B,j) by A1,A6,Th89;
    then A9: Sum(mlt(Line(a,i),Col(b,j))) =
    Sum(mlt(Line(A,i),Col(B,j))) by A8,Th90,Th91;
    thus LHS * (i,j) = Line(a,i) "*" Col(b,j) by A2,A4,MATRIX_3:def 4
                    .= Sum(mlt(Line(a,i),Col(b,j))) by FVSUM_1:def 9
                    .= Line(A,i) "*" Col(B,j) by A9,FVSUM_1:def 9
                    .= RHS * (i,j) by A3,A4,A5,MATRIX_3:def 4;
  end;
  hence a * b = A * B by Th83;
end;

theorem Th93:
  matrix_mult(n,S) = matrix_mult(n,R) || (n-Matrices_over S)
proof
  set US = n-Matrices_over S, UR = n-Matrices_over R;
  A1: US c= UR by Th85;
  then A2: [:US,US:] c= [:UR,UR:] by ZFMISC_1:96;
  A3: (matrix_mult(n,R) || (n-Matrices_over S)) is Function of [:US,US:],UR
  by A2,FUNCT_2:32;
  A4: matrix_mult(n,S) is Function of [:US,US:],UR by A1,FUNCT_2:7;
  for x,y being Element of n-Matrices_over S
  holds matrix_mult(n,S).(x,y)=(matrix_mult(n,R) || (n-Matrices_over S)).(x,y)
  proof
    let x,y be Element of n-Matrices_over S;
    reconsider a = x, b = y as Matrix of n,S;
    reconsider A = a, B = b as Matrix of n,R by Th82;
    reconsider X = x, Y = y as Element of n-Matrices_over R
    by Th85,TARSKI:def 3;
    thus matrix_mult(n,S).(x,y)
     = a * b by Def5
    .= A * B by Th92
    .= matrix_mult(n,R).(X,Y) by Def5
    .= (matrix_mult(n,R) || (n-Matrices_over S)).(x,y)
    by FUNCT_1:49,ZFMISC_1:87;
  end;
  hence matrix_mult(n,S) = matrix_mult(n,R) || (n-Matrices_over S)
  by A3,A4,BINOP_1:2;
end;

theorem Th94:
  0.(S,n) = 0.(R,n) by C0SP1:def 3;

theorem Th95:
  1.(S,n) = 1.(R,n)
proof
  reconsider RHS = 1.(S,n) as Matrix of n,R by Th82;
  for i,j being Nat st [i,j] in Indices 1.(R,n)
  holds 1.(R,n) * (i,j) = RHS * (i,j)
  proof
    let i,j be Nat;
    assume A1: [i,j] in Indices 1.(R,n);
    then A2: [i,j] in Indices RHS by MATRIX_0:26;
    per cases;
    suppose A3: i = j;
      hence 1.(R,n) * (i,j) = 1.R by A1,MATRIX_1:def 3
                           .= 1.S by C0SP1:def 3
                           .= 1.(S,n) * (i,j) by A2,A3,MATRIX_1:def 3
                           .= RHS * (i,j) by A2,Th83;
    end;
    suppose A4: i <> j;
      hence 1.(R,n) * (i,j) = 0.R by A1,MATRIX_1:def 3
                           .= 0.S by C0SP1:def 3
                           .= 1.(S,n) * (i,j) by A2,A4,MATRIX_1:def 3
                           .= RHS * (i,j) by A2,Th83;
    end;
  end;
  hence 1.(R,n) = 1.(S,n) by MATRIX_0:27;
end;

theorem Th96:
  One(S,n) = One(R,n) & Zero(S,n) = Zero(R,n) by Th95,Th94;

::$N Extension of scalars for matrix rings
theorem
  Matrix_ring(n,S) is Subring of Matrix_ring(n,R)
proof
  set MR = Matrix_ring(n,R), MS = Matrix_ring(n,S);
  set U1 = the carrier of MS;
  A1: n-Matrices_over S c= n-Matrices_over R by Th85;
  A2: matrix_add(n,S) = matrix_add(n,R) || U1 by Th87;
  A3: matrix_mult(n,S) = matrix_mult(n,R) || U1 by Th93;
  1.MS = 1.MR & 0.MS = 0.MR by Th96;
  hence Matrix_ring(n,S) is Subring of Matrix_ring(n,R)
  by A1,A2,A3,C0SP1:def 3;
end;

begin :: Center of the Matrix Ring

theorem Th98:
  for z being Element of R st z in center R
  for A being Matrix of R
  holds A * z = z * A
proof
  let z be Element of R;
  assume A1: z in center R;
  let A be Matrix of R;
  A2: len(A * z) = len(z * A) & width(A * z) = width(z * A)
  proof
    thus len(A * z) = len A by MATRIX_3:def 6
                   .= len(z * A) by MATRIX_3:def 5;
    thus width(A * z) = width A by MATRIX_3:def 6
                     .= width(z * A) by MATRIX_3:def 5;
  end;
  for i,j being Nat st [i,j] in Indices(A*z)
  holds (A*z)*(i,j) = (z*A)*(i,j)
  proof
    let i,j be Nat;
    assume A3: [i,j] in Indices(A*z);
    A4: Indices(A*z) = [:dom(A*z),Seg(width(A*z)):] by MATRIX_0:def 4
                    .= [:Seg len(A*z),Seg width(A*z):] by FINSEQ_1:def 3
                    .= [:Seg len A,Seg width(A*z):] by MATRIX_3:def 6
                    .= [:Seg len A,Seg width A:] by MATRIX_3:def 6
                    .= [:dom A,Seg width A:] by FINSEQ_1:def 3
                    .= Indices A by MATRIX_0:def 4;
    hence (A*z)*(i,j) = (A*(i,j))*z by A3,MATRIX_3:def 6
                     .= z*(A*(i,j)) by A1,WEDDWITT:17
                     .= (z*A)*(i,j) by A3,A4,MATRIX_3:def 5;
  end;
  hence A * z = z * A by A2,MATRIX_0:21;
end;

theorem Th99:
  for z being Element of R st z in center R
  for A,B being Matrix of n,R
  st A*B = B*A
  holds A*(z*B) = (z*B)*A
proof
  let z be Element of R;
  assume A1: z in center R;
  let A,B be Matrix of n,R;
  assume A2: A*B = B*A;
  thus A*(z*B) = (A*z)*B by Th24
              .= (z*A)*B by A1,Th98
              .= z*(A*B) by Th29
              .= (z*B)*A by A2,Th29;
end;

theorem Th100:
  for z being Element of R st z in center R
  for A being Matrix of n,R
  holds A*(z*(1.(R,n))) = (z*(1.(R,n)))*A
proof
  let z be Element of R;
  assume A1: z in center R;
  let A be Matrix of n,R;
  A*(1.(R,n)) = A by MATRIX_3:19
             .= (1.(R,n))*A by MATRIX_3:18;
  hence thesis by A1,Th99;
end;

theorem Th101:
  for x,y being Element of R
  holds (x * 1.(R,n)) * y = (x * y) * 1.(R,n)
proof
  let x,y be Element of R;
  set LHS = (x * 1.(R,n)) * y, RHS = (x * y) * 1.(R,n);
  A1: len LHS = len RHS & width LHS = width RHS
  proof
    thus len LHS = len(x * 1.(R,n)) by MATRIX_3:def 6
                .= len 1.(R,n) by MATRIX_3:def 5
                .= len RHS by MATRIX_3:def 5;
    thus width LHS = width (x * 1.(R,n)) by MATRIX_3:def 6
                  .= width 1.(R,n) by MATRIX_3:def 5
                  .= width RHS by MATRIX_3:def 5;
  end;

  for i,j being Nat st [i,j] in Indices LHS
  holds LHS * (i,j) = RHS * (i,j)
  proof
    let i,j be Nat;
    assume A2: [i,j] in Indices LHS;
    A3: [i,j] in Indices (x * 1.(R,n)) & [i,j] in Indices 1.(R,n)
    proof
      A4: Indices LHS = [:dom LHS, Seg width LHS:] by MATRIX_0:def 4
                     .= [:Seg len LHS,Seg width LHS:] by FINSEQ_1:def 3
                     .= [:Seg len(x * 1.(R,n)), Seg width LHS:]
                        by MATRIX_3:def 6
                     .= [:Seg len(x * 1.(R,n)), Seg(width(x * 1.(R,n))):]
                        by MATRIX_3:def 6;
      then Indices LHS = [:dom(x*1.(R,n)),Seg(width(x*1.(R,n))):]
      by FINSEQ_1:def 3;
      hence [i,j] in Indices (x * 1.(R,n)) by A2,MATRIX_0:def 4;
      Indices LHS = [:Seg len 1.(R,n), Seg width(x * 1.(R,n)):]
                    by A4,MATRIX_3:def 5
                 .= [:Seg len 1.(R,n),Seg width(1.(R,n)):] by MATRIX_3:def 5
                 .= [:dom(1.(R,n)),Seg width(1.(R,n)):] by FINSEQ_1:def 3
                 .= Indices 1.(R,n) by MATRIX_0:def 4;
      hence [i,j] in Indices 1.(R,n) by A2;
    end;

    per cases;
    suppose A5: i = j;
      thus LHS * (i,j) = ((x * 1.(R,n)) * (i,j)) * y by A3,MATRIX_3:def 6
                      .= (x * (1.(R,n) * (i,j))) * y by A3,MATRIX_3:def 5
                      .= (x * (1.R)) * y by A3,A5,MATRIX_1:def 3
                      .= (x * y) * (1.R)
                      .= (x * y) * (1.(R,n) * (i,j)) by A3,A5,MATRIX_1:def 3
                      .= RHS * (i,j) by A3,MATRIX_3:def 5;
    end;
    suppose A6: i <> j;
      thus LHS * (i,j) = ((x * 1.(R,n)) * (i,j)) * y by A3,MATRIX_3:def 6
                      .= (x * (1.(R,n) * (i,j))) * y by A3,MATRIX_3:def 5
                      .= (x * (0.R)) * y by A3,A6,MATRIX_1:def 3
                      .= (x * y) * (0.R)
                      .= (x * y) * (1.(R,n) * (i,j)) by A3,A6,MATRIX_1:def 3
                      .= RHS * (i,j) by A3,MATRIX_3:def 5;
    end;
  end;
  hence (x * 1.(R,n)) * y = (x * y) * 1.(R,n) by A1,MATRIX_0:21;
end;

theorem Th102:
  for x,y being Element of R
  holds (x * 1.(R,n)) * (y * 1.(R,n)) = ((x * 1.(R,n)) * y) * 1.(R,n)
  by Th24;

::$N See, e.g., Bourbaki's "Algebra" VIII~\cite{bourbaki2023algebra} 5 no.3 corollary 2 to theorem 2
theorem Th103:
  for A being Matrix of n,R
  st (for B being Matrix of n,R
      holds A * B = B * A)
  ex z being Element of R
  st z in center R & A = z*(1.(R,n))
proof
  let A be Matrix of n,R;
  assume A1: for B being Matrix of n,R holds A * B = B * A;
  A2: for i,j being Nat st [i,j] in Indices A & i <> j
      holds A * (i,j) = 0.R
  proof
    let i,j be Nat;
    assume A3: [i,j] in Indices A;
    assume A4: i <> j;
    [i,j] in [:Seg n,Seg n:] by A3,MATRIX_0:24;
    then i in Seg n by ZFMISC_1:87;
    then [i,i] in [:Seg n,Seg n:] by ZFMISC_1:87;
    then A5: [i,i] in Indices canMat(i,i,n,R) by MATRIX_0:24;
    hence 0.R = (A * (canMat(i,i,n,R))) * (i,j) by A3,A4,Th55
            .= ((canMat(i,i,n,R)) * A) * (i,j) by A1
            .= A * (i,j) by A3,A5,Th54;
  end;
  A6: for i,j being Nat st [i,j] in Indices A
      holds A * (i,i) = A * (j,j)
  proof
    let i,j be Nat;
    assume A7: [i,j] in Indices A;
    A8: Indices A = [:Seg n,Seg n:] by MATRIX_0:24
                 .= Indices canMat(i,j,n,R) by MATRIX_0:24;
    hence A * (i,i) = (A * (canMat(i,j,n,R))) * (i,j) by A7,Th55
                  .= ((canMat(i,j,n,R)) * A) * (i,j) by A1
                  .= A * (j,j) by A7,A8,Th54;
  end;

  per cases;
  suppose A9: n = 0;
    take z = 1.R;
    A10: z = 1_R;
    A11: len A = len (z * 1.(R,n)) & width A = width (z * 1.(R,n))
    proof
      thus len A = n by MATRIX_0:25
                .= len (z * 1.(R,n)) by MATRIX_0:25;
      thus width A = n by MATRIX_0:24
                  .= width (z * 1.(R,n)) by MATRIX_0:24;
    end;
    for i,j being Nat st [i,j] in Indices A
    holds A*(i,j) = (z * (1.(R,n)))*(i,j) by A9,MATRIX_0:22;
    hence thesis by A10,A11,MATRIX_0:21,WEDDWITT:19;
  end;
  suppose n > 0;
    then 0 < 0 + n;
    then 1 <= n by NAT_1:19;
    then A12: [1,1] in Indices A by MATRIX_0:31;
    take z = A * (1,1);
    A13: len A = len (z* 1.(R,n)) & width A = width (z * 1.(R,n))
    proof
      thus len A = n by MATRIX_0:25
                .= len (z * 1.(R,n)) by MATRIX_0:25;
      thus width A = n by MATRIX_0:24
                  .= width (z * 1.(R,n)) by MATRIX_0:24;
    end;
    :: This follows from A2,A3
    for i,j being Nat st [i,j] in Indices A
    holds A*(i,j) = (z * (1.(R,n)))*(i,j)
    proof
      let i,j be Nat;
      assume A14: [i,j] in Indices A;
      A15: Indices A = [:Seg n,Seg n:] by MATRIX_0:24
                    .= Indices 1.(R,n) by MATRIX_0:24;
      per cases;
      suppose A16: i = j;
        [1,i] in Indices A
        proof
          [1,1] in [:Seg n,Seg n:] by A12,MATRIX_0:24;
          then A17: 1 in Seg n by ZFMISC_1:87;
          [i,j] in [:Seg n,Seg n:] by A14,MATRIX_0:24;
          then i in Seg n by ZFMISC_1:87;
          then [1,i] in [:Seg n,Seg n:] by A17,ZFMISC_1:87;
          hence [1,i] in Indices A by MATRIX_0:24;
        end;
        hence A*(i,j) = z * 1.R by A6,A16
                     .= z * (1.(R,n) * (i,j)) by A14,A15,A16,MATRIX_1:def 3
                     .= (z * (1.(R,n)))*(i,j) by A14,A15,MATRIX_3:def 5;
      end;
      suppose A18: i <> j;
        hence A*(i,j) = z * 0.R by A2,A14
                    .= z * (1.(R,n) * (i,j)) by A14,A15,A18,MATRIX_1:def 3
                    .= (z * (1.(R,n)))*(i,j) by A14,A15,MATRIX_3:def 5;
      end;
    end;
    then A19: A = z * 1.(R,n) by A13,MATRIX_0:21;
    for x being Element of R holds z * x = x * z
    proof
      let x be Element of R;
      A20: ((x * z) * 1.(R,n)) = ((x * z) * 1.(R,n)) * 1.(R,n) by MATRIX_3:19
                              .= ((x * 1.(R,n)) * z) * 1.(R,n) by Th101
                              .= (x * 1.(R,n)) * (z * 1.(R,n)) by Th102
                              .= A * (x * 1.(R,n)) by A1,A19
                              .= ((z * 1.(R,n)) * x) * 1.(R,n) by A19,Th102
                              .= ((z * x) * 1.(R,n)) * 1.(R,n) by Th101
                              .= (z * x) * 1.(R,n) by MATRIX_3:19;
      A21: Indices 1.(R,n) = [:Seg n, Seg n:] by MATRIX_0:24
                          .= Indices A by MATRIX_0:24;
      thus x * z = (x * z) * (1.R)
                .= (x * z) * ((1.(R,n)) * (1,1)) by A12,A21,MATRIX_1:def 3
                .= ((x * z) * 1.(R,n)) * (1,1) by A12,A21,MATRIX_3:def 5
                .= (z * x) * ((1.(R,n)) * (1,1)) by A12,A20,A21,MATRIX_3:def 5
                .= (z * x) * (1.R) by A12,A21,MATRIX_1:def 3
                .= z * x;
    end;
    hence thesis by A19,WEDDWITT:17;
  end;
end;

theorem Th105:
  for X being Element of Matrix_ring(n,R)
  for A being Matrix of n,R st A = X
  holds X in center Matrix_ring(n,R)
  iff (for B being Matrix of n,R holds A * B = B * A)
proof
  let X be Element of Matrix_ring(n,R);
  let A be Matrix of n,R;
  assume A1: A = X;
  hereby
    assume A2: X in center Matrix_ring(n,R);
    let B be Matrix of n,R;
    reconsider Y = B as Element of Matrix_ring(n,R) by Th72;
    thus A * B = X * Y by A1,Th75
              .= Y * X by A2,WEDDWITT:17
              .= B * A by A1,Th75;
  end;
  assume A3: for B being Matrix of n,R holds A * B = B * A;
  for Y being Element of Matrix_ring(n,R)
  holds X*Y = Y*X
  proof
    let Y be Element of Matrix_ring(n,R);
    reconsider B = Y as Matrix of n,R by Th72;
    thus X*Y = A * B by A1,Th75
            .= B * A by A3
            .= Y*X by A1,Th75;
  end;
  hence X in center Matrix_ring(n,R) by WEDDWITT:17;
end;

theorem
  for X being Element of Matrix_ring(n,R)
  holds X in center Matrix_ring(n,R) iff
  ex z being Element of R
  st z in center R & X = z*(1.(R,n))
proof
  let X be Element of Matrix_ring(n,R);
  hereby
    assume A1: X in center Matrix_ring(n,R);
    reconsider A = X as Matrix of n,R by Th72;
    for B being Matrix of n,R holds A * B = B * A by A1,Th105;
    then consider z being Element of R such that
    A2: z in center R & A = z * (1.(R,n))
    by Th103;
    take z;
    thus z in center R by A2;
    thus X = z*(1.(R,n)) by A2;
  end;
  given z being Element of R such that
  A3: z in center R & X = z*(1.(R,n));
  reconsider A = X as Matrix of n,R by Th72;
  for Y being Element of Matrix_ring(n,R)
  holds X * Y = Y * X
  proof
    let Y be Element of Matrix_ring(n,R);
    reconsider B = Y as Matrix of n,R by Th72;
    thus X * Y = A * B by Th75
              .= B * A by A3,Th100
              .= Y * X by Th75;
  end;

  hence X in center Matrix_ring(n,R) by WEDDWITT:17;
end;

begin :: Group of Units for unital rings

:: Most texts require M to be a Monoid, but that is too much
 reserve M for associative right_unital non empty multLoopStr;

definition
  let M be non empty multLoopStr;
  func units M -> Subset of M equals
  {x where x is Element of M : x is unital};
  coherence
  proof
    set U = {x where x is Element of M : x is unital};
    for u being object st u in U holds u in the carrier of M
    proof
      let u be object;
      assume u in U;
      then consider x being Element of M such that
      A1: u = x & x is unital;
      thus u in the carrier of M by A1;
    end;
    hence thesis by TARSKI:def 3;
  end;
end;

theorem Th107:
  for M being right_unital non empty multLoopStr
  for ell being Element of M
  holds ell is unital iff ell in units M
proof
  let M be right_unital non empty multLoopStr;
  let ell be Element of M;
  thus ell is unital implies ell in units M;
  assume ell in units M;
  then consider x being Element of M such that
  A1: ell = x & x is unital;
  thus ell is unital by A1;
end;

Th108:
  for u,v being unital Element of M
  holds u * v is unital
proof
  let u,v be unital Element of M;
  consider a being Element of M such that
  A1: u * a = 1.M & a * u = 1.M by GCD_1:def 2;
  consider b being Element of M such that
  A2: v * b = 1.M & b * v = 1.M by GCD_1:def 2;
  A3: (u * v) * (b * a) = u * (v * (b * a)) by GROUP_1:def 3
                       .= u * ((1.M) * a) by A2,GROUP_1:def 3
                       .= (u * (1.M)) * a by GROUP_1:def 3
                       .= 1.M by A1;
  (b * a) * (u * v) = ((b * a) * u) * v by GROUP_1:def 3
                   .= (b * (1.M)) * v by A1,GROUP_1:def 3
                   .= 1.M by A2;
  hence u * v is unital by A3,GCD_1:def 2;
end;

registration
  let M;
  let u,v be unital Element of M;
  cluster u * v -> unital;
  coherence by Th108;
end;

registration
  let M;
  cluster units M -> (the multF of M)-binopclosed;
  coherence
  proof
    for x being set st x in [:units M,units M:]
    holds (the multF of M).x in units M
    proof
      let x be set;
      assume x in [:units M,units M:];
      then consider x1,x2 being object such that
      A1: x1 in units M & x2 in units M & x = [x1,x2]
      by ZFMISC_1:def 2;
      reconsider x1,x2 as Element of M by A1;
      A2: (the multF of M).x = x1 * x2 by A1;
      x1 is unital & x2 is unital by A1,Th107;
      hence (the multF of M).x in units M by A2;
    end;
    hence units M is (the multF of M)-binopclosed by REALSET1:def 1;
  end;
end;

definition
  let M;
  func UnitGroup M -> strict multMagma equals
  multMagma(# units M, (the multF of M) || (units M) #);
  coherence;
end;

theorem
  1.M in UnitGroup M
proof
  1.M in the carrier of UnitGroup M;
  hence thesis by STRUCT_0:def 5;
end;

registration
  let M;
  cluster UnitGroup M -> non empty;
  coherence
  proof
    1.M in the carrier of UnitGroup M;
    hence thesis;
  end;
end;

theorem Th110:
  for a,b being Element of M
  for x,y being Element of UnitGroup M
  st a = x & b = y
  holds a * b = x * y by FUNCT_1:49,ZFMISC_1:87;

registration
  let M;
  cluster UnitGroup M -> associative;
  coherence
  proof
    for x,y,z being Element of UnitGroup M
    holds (x * y) * z = x * (y * z)
    proof
      let x,y,z be Element of UnitGroup M;
      x in units M & y in units M & z in units M;
      then reconsider a = x, b = y, c = z as Element of M;
      A1: x * y = a * b & y * z = b * c by Th110;
      hence (x * y) * z = (a * b) * c by Th110
                      .= a * (b * c) by GROUP_1:def 3
                      .= x * (y * z) by A1,Th110;
    end;
    hence thesis by GROUP_1:def 3;
  end;
end;

:: Importantly, M is a monoid for UnitGroup M to be Group-like
registration
  let M be associative left_unital right_unital non empty multLoopStr;
  cluster UnitGroup M -> Group-like;
  coherence
  proof
    ex e being Element of UnitGroup M st
    for h being Element of UnitGroup M
    holds (h * e = h & e * h = h & ex g being Element of UnitGroup M st
    (h * g = e & g * h = e))
    proof
      1.M in units M;
      then reconsider e = 1.M as Element of UnitGroup M;
      take e;
      let h be Element of UnitGroup M;
      h in units M;
      then reconsider h9 = h as Element of M;
      thus h * e = h9 * 1.M by Th110
                .= h;
      thus e * h = 1.M * h9 by Th110
                .= h;
      consider g9 being Element of M such that
      A1: 1.M = h9 * g9 & 1.M = g9 * h9 by Th107,GCD_1:def 2;
      g9 is unital by A1,GCD_1:def 2;
      then g9 in units M;
      then reconsider g = g9 as Element of UnitGroup M;
      take g;
      thus h * g = e by A1,Th110;
      thus g * h = e by A1,Th110;
    end;
    hence thesis by GROUP_1:def 2;
  end;
end;

theorem Th111:
  for M being associative well-unital non empty multLoopStr
  holds 1_(UnitGroup M) = 1.M
proof
  let M be associative well-unital non empty multLoopStr;
  1.M in the carrier of UnitGroup M;
  then reconsider e=1.M as Element of UnitGroup M;
  for x being Element of UnitGroup M
  holds x * e = x & e * x = x
  proof
    let x be Element of UnitGroup M;
    x in units M;
    then reconsider a = x as Element of M;
    thus x * e = a * (1.M) by Th110
              .= x;
    thus e * x = (1.M) * a by Th110
              .= x;
  end;
  hence 1_(UnitGroup M) = 1.M by GROUP_1:4;
end;

Th112:
  for R being commutative Ring
  holds UnitGroup R is commutative
proof
  let R be commutative Ring;
  for x,y being Element of UnitGroup R
  holds x * y = y * x
  proof
    let x,y be Element of UnitGroup R;
    x in units R & y in units R;
    then reconsider X=x,Y=y as Element of R;
    thus x * y = X * Y by Th110
              .= y * x by Th110;
  end;
  hence UnitGroup R is commutative by GROUP_1:def 12;
end;

registration
  let R be commutative Ring;
  cluster UnitGroup R -> commutative;
  coherence by Th112;
end;

theorem
  for M being associative left_unital right_unital non empty multLoopStr
  holds UnitGroup M is strict Group;

theorem Th114:
  for G being associative left_unital right_unital non empty multLoopStr
  st G is Group-like
  holds units G = the carrier of G
proof
  let G be associative left_unital right_unital non empty multLoopStr;
  assume A1: G is Group-like;
  for x being object
  st x in the carrier of G
  holds x in units G
  proof
    let x be object;
    assume x in the carrier of G;
    then reconsider g = x as Element of G;
    consider e being Element of G such that
    A2: for h being Element of G holds h * e = h & e * h = h &
    ex g9 being Element of G st h * g9 = e & g9 * h = e
    by A1,GROUP_1:def 2;
    1.G = (1.G) * e by A2
       .= e;
    then ex y being Element of G st g * y = 1.G & y * g = 1.G by A2;
    then g is unital by GCD_1:def 2;
    hence x in units G;
  end;
  then the carrier of G c= units G by TARSKI:def 3;
  hence units G = the carrier of G by XBOOLE_0:def 10;
end;

:: Morally: UnitGroup of a strict group G is identical to G itself
theorem
  for G being associative left_unital right_unital non empty multLoopStr
  st G is Group-like
  holds UnitGroup G = the multMagma of G
proof
  let G be associative left_unital right_unital non empty multLoopStr;
  assume G is Group-like;
  then units G = the carrier of G by Th114;
  hence UnitGroup G = the multMagma of G;
end;

:: Now, we can see that UnitGroup R coincides with MultGroup R when R
:: is a Skew-Field. First, a useful lemma.
theorem Th116:
  for R being Skew-Field holds NonZero R = units R
proof
  let R be Skew-Field;
  for x being object st x in NonZero R holds x in units R
  proof
    let x be object;
    assume A1: x in NonZero R;
    then reconsider X = x as Element of R;
    X <> 0.R by A1,STRUCT_0:1;
    then consider Y being Element of R such that
    A2: Y * X = 1.R by ALGSTR_0:def 27,def 39;
    X * Y = 1.R by A2,VECTSP_2:7;
    then X is unital by A2,GCD_1:def 2;
    hence x in units R;
  end;
  then A3: NonZero R c= units R by TARSKI:def 3;
  for x being object st x in units R holds x in NonZero R
  proof
    let x be object;
    assume A4: x in units R;
    then reconsider X = x as Element of R;
    consider Y being Element of R such that
    A5: X * Y = 1.R & Y * X = 1.R
    by A4,Th107,GCD_1:def 2;
    X <> 0.R & Y <> 0.R by A5;
    hence x in NonZero R by STRUCT_0:1,def 12;
  end;

  then units R c= NonZero R by TARSKI:def 3;
  hence NonZero R = units R by A3,XBOOLE_0:def 10;
end;

theorem Th117:
  for R being Skew-Field
  holds MultGroup R = UnitGroup R
proof
  let R be Skew-Field;
  the carrier of MultGroup R = NonZero R by UNIROOTS:def 1
                            .= the carrier of UnitGroup R by Th116;
  hence MultGroup R = UnitGroup R by UNIROOTS:def 1;
end;

registration
  let R be Skew-Field;
  identify units R with NonZero R;
  correctness by Th116;
  identify UnitGroup R with MultGroup R;
  correctness by Th117;
end;

theorem Th118:
  for R being commutative Ring
  for x being object
  holds x in center R & x in UnitGroup R
  iff x in center UnitGroup R
proof
  let R be commutative Ring;
  let x be object;
  thus x in center R & x in UnitGroup R implies x in center UnitGroup R
  by GROUP_5:82;
  assume A1: x in center UnitGroup R;
  then x in the carrier of UnitGroup R by GROUP_2:40,STRUCT_0:def 5;
  hence x in center R by Th13,STRUCT_0:def 5;
  thus x in UnitGroup R by A1,GROUP_5:82;
end;

:: The converse of this theorem is false for *noncommutative* rings in
:: general. See Tsit Yuen Lam's "First Course in Noncommutative Rings"
:: (Springer, GTM131, 1991), Example (1.7) for a counter-example to
:: the converse.
:: For a summary, see: https://math.stackexchange.com/a/342817/31693
theorem
  for x being object
  st x in center R & x in UnitGroup R
  holds x in center UnitGroup R
proof
  let x be object;
  assume A1: x in center R;
  assume x in UnitGroup R;
  then reconsider a = x as Element of UnitGroup R by STRUCT_0:def 5;
  for g being Element of UnitGroup R
  holds a * g = g * a
  proof
    let g be Element of UnitGroup R;
    a in units R & g in units R;
    then reconsider g9=g,a9=a as Element of R;
    thus a * g = a9 * g9 by Th110
              .= g9 * a9 by A1,WEDDWITT:43
              .= g * a by Th110;
  end;
  hence x in center UnitGroup R by GROUP_5:77;
end;

theorem Th120:
  for A being Matrix of n,R
  for z being Element of R
  st A = z * 1.(R,n) & z in UnitGroup R
  holds A is invertible
proof
  let A be Matrix of n,R;
  let z be Element of R;
  assume A1: A = z * 1.(R,n);
  assume z in UnitGroup R;
  then z in the carrier of UnitGroup R by STRUCT_0:def 5;
  then consider y being Element of R such that
  A2: z * y = 1.R & y * z = 1.R by Th107,GCD_1:def 2;
  A3: A * (y * 1.(R,n)) = ((z * 1.(R,n)) * y) * 1.(R,n) by A1,Th102
                       .= ((z * 1.(R,n)) * y) by MATRIX_3:19
                       .= (1.R) * 1.(R,n) by A2,Th101
                       .= 1.(R,n);
  (y * 1.(R,n)) * A = ((y * 1.(R,n)) * z) * 1.(R,n) by A1,Th102
                   .= (y * 1.(R,n)) * z by MATRIX_3:19
                   .= (y * z) * 1.(R,n) by Th101
                   .= 1.(R,n) by A2;
  hence A is invertible by A3,MATRIX_6:def 2,def 3;
end;

theorem Th121:
  for A being Matrix of n,R
  for z being Element of R
  st n > 0 & A = z * 1.(R,n) & A is invertible
  holds z in UnitGroup R
proof
  let A be Matrix of n,R;
  let z be Element of R;
  assume A1: n > 0;
  assume A2: A = z * 1.(R,n);
  assume A is invertible;
  then consider M2 being Matrix of n,R such that
  A3: A is_reverse_of M2
  by MATRIX_6:def 3;
  A4: A * M2 = M2 * A & A * M2 = 1.(R,n) by A3,MATRIX_6:def 2;
  then A5: 1.(R,n) = z * (1.(R,n) * M2) by A2,Th29
                  .= z * M2 by MATRIX_3:18;
  A6: [1,1] in Indices M2 & [1,1] in Indices 1.(R,n)
  proof
    0 < 0 + n by A1;
    then 1 <= n by NAT_1:19;
    hence thesis by MATRIX_0:31;
  end;
  then A7: 1.R = (1.(R,n)) * (1,1) by MATRIX_1:def 3
              .= z * (M2 * (1,1)) by A5,A6,MATRIX_3:def 5;
  A8: 1.(R,n) = (M2 * z) * 1.(R,n) by A2,A4,Th24
             .= M2 * z by MATRIX_3:19;
  1.R = (1.(R,n)) * (1,1) by A6,MATRIX_1:def 3
     .= (M2 * (1,1)) * z by A6,A8,MATRIX_3:def 6;
  then z is unital by A7,GCD_1:def 2;
  then z in the carrier of UnitGroup R;
  hence z in UnitGroup R by STRUCT_0:def 5;
end;

Th122:
  for A being invertible Matrix of n,R
  st (for B being invertible Matrix of n,R
      holds A * B = B * A)
  ex z being Element of R st A = z*(1.(R,n))
proof
  let A be invertible Matrix of n,R;
  assume A1: for B being invertible Matrix of n,R holds A * B = B * A;
  :: Step 1: A must be commute with canMat(i,j,n,R)
  A2: for i,j being Nat st i <> j
  holds A * canMat(i,j,n,R) = canMat(i,j,n,R) * A
  proof
    let i,j be Nat;
    assume A3: i <> j;
    (1.R) * canMat(i,j,n,R) = canMat(i,j,n,R);
    then 1.(R,n) + canMat(i,j,n,R) is invertible Matrix of n,R
    by A3,Th57;
    then A * (1.(R,n) + canMat(i,j,n,R)) = (1.(R,n) + canMat(i,j,n,R)) * A
    by A1;
    hence A * canMat(i,j,n,R) = canMat(i,j,n,R) * A by Th59;
  end;

  :: Step 2: A must be diagonal
  A4: for i,j being Nat st [i,j] in Indices A & i <> j
      holds A * (i,j) = 0.R
  proof
    let i,j be Nat;
    set i2=i, j2=i, i0 = j, j0 = i;
    assume A5: [i,j] in Indices A;
    assume A6: i <> j;
    [i,j] in [:Seg n,Seg n:] by A5,MATRIX_0:24;
    then A7: i in Seg n & j in Seg n by ZFMISC_1:87;
    then [j,i] in [:Seg n,Seg n:] by ZFMISC_1:87;
    then A8: [j,i] in Indices canMat(i0,j0,n,R) by MATRIX_0:24;
    [i,i] in [:Seg n,Seg n:] by A7,ZFMISC_1:87;
    then A9: [i,i] in Indices A by MATRIX_0:24;
    hence A * (i,j) = (A * canMat(i0,j0,n,R)) * (i2,j2) by A8,Th55
                   .= ((canMat(i0,j0,n,R)) * A) * (i2,j2) by A2,A6
                   .= 0.R by A6,A8,A9,Th54;
  end;
  :: Step 3: A must commute with permutation matrices, which implies A
  :: must be a scalar matrix.
  A10: for i,j being Nat st [i,j] in Indices A
      holds A * (i,i) = A * (j,j)
  proof
    let i,j be Nat;
    assume A11: [i,j] in Indices A;
    per cases;
    suppose i = j;
      hence thesis;
    end;
    suppose A12: i <> j;
      A13: Indices A = [:Seg n,Seg n:] by MATRIX_0:24
                    .= Indices canMat(i,j,n,R) by MATRIX_0:24;
      hence A * (i,i) = (A * (canMat(i,j,n,R))) * (i,j) by A11,Th55
                    .= ((canMat(i,j,n,R)) * A) * (i,j) by A2,A12
                    .= A * (j,j) by A11,A13,Th54;
    end;
  end;
  :: The rest of the proof is as before
  per cases;
  suppose A14: n = 0;
    take z = 1.R;
    thus thesis by A14,MATRIX_0:45;
  end;
  suppose n > 0;
    then 0 < 0 + n;
    then 1 <= n by NAT_1:19;
    then A15: [1,1] in Indices A by MATRIX_0:31;
    take z = A * (1,1);
    A16: len A = len (z* 1.(R,n)) & width A = width (z * 1.(R,n))
    proof
      thus len A = n by MATRIX_0:25
                .= len (z * 1.(R,n)) by MATRIX_0:25;
      thus width A = n by MATRIX_0:24
                  .= width (z * 1.(R,n)) by MATRIX_0:24;
    end;
    :: This follows from A2,A3
    for i,j being Nat st [i,j] in Indices A
    holds A*(i,j) = (z * (1.(R,n)))*(i,j)
    proof
      let i,j be Nat;
      assume A17: [i,j] in Indices A;
      Indices A = [:Seg n,Seg n:] by MATRIX_0:24
               .= Indices 1.(R,n) by MATRIX_0:24;
      then A18: [i,j] in Indices 1.(R,n) by A17;
      per cases;
      suppose A19: i = j;
        [1,i] in Indices A
        proof
          [1,1] in [:Seg n,Seg n:] by A15,MATRIX_0:24;
          then A20: 1 in Seg n by ZFMISC_1:87;
          [i,j] in [:Seg n,Seg n:] by A17,MATRIX_0:24;
          then i in Seg n by ZFMISC_1:87;
          then [1,i] in [:Seg n,Seg n:] by A20,ZFMISC_1:87;
          hence [1,i] in Indices A by MATRIX_0:24;
        end;
        hence A*(i,j) = z * 1.R by A10,A19
                     .= z * (1.(R,n) * (i,j)) by A18,A19,MATRIX_1:def 3
                     .= (z * (1.(R,n)))*(i,j) by A18,MATRIX_3:def 5;
      end;
      suppose A21: i <> j;
        hence A*(i,j) = z * 0.R by A4,A17
                    .= z * (1.(R,n) * (i,j)) by A18,A21,MATRIX_1:def 3
                    .= (z * (1.(R,n)))*(i,j) by A18,MATRIX_3:def 5;
      end;
    end;
    :: Then 'A' must be a scalar matrix.
    hence A = z * 1.(R,n) by A16,MATRIX_0:21;
  end;
end;

Lm3:
  for A being invertible Matrix of n,R
  st n = 0
  ex z being Element of R
  st z in center R & z in UnitGroup R & z in center UnitGroup R
  & A = z*(1.(R,n))
proof
  let A be invertible Matrix of n,R;
  assume A1: n = 0;
  take z = 1.R;
  A2: z in center (UnitGroup R) & z in center R &
  z in UnitGroup R
  proof
    z = 1_(UnitGroup R) by Th111;
    hence z in center (UnitGroup R) by GROUP_2:46;
    z = 1_R;
    hence z in center R by WEDDWITT:19;
    z = 1_(UnitGroup R) by Th111;
    hence z in UnitGroup R by STRUCT_0:def 5;
  end;
  A3: len A = len (z * 1.(R,n)) & width A = width (z * 1.(R,n))
  proof
    thus len A = n by MATRIX_0:25
              .= len (z * 1.(R,n)) by MATRIX_0:25;
    thus width A = n by MATRIX_0:24
                .= width (z * 1.(R,n)) by MATRIX_0:24;
  end;
  for i,j being Nat st [i,j] in Indices A
  holds A*(i,j) = (z * (1.(R,n)))*(i,j) by A1,MATRIX_0:22;
  hence thesis by A2,A3,MATRIX_0:21;
end;

Th123:
  for A being invertible Matrix of n,R
  st (for B being invertible Matrix of n,R
      holds A * B = B * A)
  holds (n = 1 implies ex z being Element of R
         st z in center UnitGroup R & A = z*(1.(R,n)))
  & (n <> 1 implies ex z being Element of R
     st z in center R & z in UnitGroup R & A = z*(1.(R,n)))
proof
  let A be invertible Matrix of n,R;
  assume A1: for B being invertible Matrix of n,R holds A * B = B * A;
  thus (n = 1 implies ex z being Element of R
                      st z in center UnitGroup R & A = z*(1.(R,n)))
  proof
    assume A2: n = 1;
    consider z being Element of R such that
    A3: A = z * 1.(R,n) by A1,Th122;
    take z;
    z in UnitGroup R by A2,A3,Th121;
    then reconsider z9 = z as Element of UnitGroup R by STRUCT_0:def 5;
    A4: [1,1] in Indices A
    & [1,1] in Indices 1.(R,n) by A2,MATRIX_0:31;
    for x9 being Element of UnitGroup R
    holds z9 * x9 = x9 * z9
    proof
      let x9 be Element of UnitGroup R;
      x9 in units R;
      then reconsider x = x9 as Element of R;
      A5: x * 1.(R,n) is invertible by Th120,STRUCT_0:def 5;
      A6: ((x * z) * 1.(R,n)) = ((x * z) * 1.(R,n)) * 1.(R,n) by MATRIX_3:19
                             .= ((x * 1.(R,n)) * z) * 1.(R,n) by Th101
                             .= (x * 1.(R,n)) * (z * 1.(R,n)) by Th102
                             .= A * (x * 1.(R,n)) by A5,A1,A3
                             .= ((z * 1.(R,n)) * x) * 1.(R,n) by A3,Th102
                             .= ((z * x) * 1.(R,n)) * 1.(R,n) by Th101
                             .= (z * x) * 1.(R,n) by MATRIX_3:19;
      thus x9 * z9 = (x * z) * (1.R) by Th110
                  .= (x * z) * ((1.(R,n)) * (1,1)) by A4,MATRIX_1:def 3
                  .= ((x * z) * 1.(R,n)) * (1,1) by A4,MATRIX_3:def 5
                  .= (z * x) * ((1.(R,n)) * (1,1)) by A6,A4,MATRIX_3:def 5
                  .= (z * x) * (1.R) by A4,MATRIX_1:def 3
                  .= z9 * x9 by Th110;
    end;
    hence z in center UnitGroup R by GROUP_5:77;
    thus A = z*(1.(R,n)) by A3;
  end;
  assume A7: n <> 1;
  per cases;
  suppose n = 0;
    then ex z being Element of R
    st z in center R & z in UnitGroup R & z in center UnitGroup R
    & A = z*(1.(R,n)) by Lm3;
    hence thesis;
  end;
  suppose A8: n > 0;
    then A9: n >= 2 by A7,NAT_1:23;
    consider z being Element of R such that
    A10: A = z*(1.(R,n)) by A1,Th122;
    take z;
    for x being Element of R
    holds x * z = z * x
    proof
      let x be Element of R;
      set M = 1.(R,n) + x * canMat(1,2,n,R);
      M is invertible Matrix of n,R by Th57;
      then M * A = A * M by A1;
      then A*(x*canMat(1,2,n,R)) = (x*canMat(1,2,n,R))*A by Th58
                                .= ((x*canMat(1,2,n,R))*z)*1.(R,n) by A10,Th24
                                .= ((x*canMat(1,2,n,R))*z) by MATRIX_3:19
                                .= x*(canMat(1,2,n,R)*z) by Th26
                                .= x*(z*canMat(1,2,n,R)) by Th56
                                .= (x*z)*canMat(1,2,n,R) by Th27;
      then A11: (x*z)*canMat(1,2,n,R)
       = ((z*1.(R,n))*x)*canMat(1,2,n,R) by A10,Th24
      .= ((z * x)*1.(R,n))*canMat(1,2,n,R) by Th101
      .= (z * x)*(1.(R,n) * canMat(1,2,n,R)) by Th29
      .= (z * x)*canMat(1,2,n,R) by MATRIX_3:18;
      1 <= 2 & 2 <= n & 1 <= 1 & 1 <= n by A9,XXREAL_0:2;
      then A12: [1,2] in Indices canMat(1,2,n,R) by MATRIX_0:31;
      thus x * z = (x * z) * (1.R)
                .= (x * z) * (canMat(1,2,n,R) * (1,2)) by A12,Def1
                .= ((x * z) * canMat(1,2,n,R)) * (1,2) by A12,MATRIX_3:def 5
                .= (z * x) * (canMat(1,2,n,R) * (1,2))
                   by A11,A12,MATRIX_3:def 5
                .= (z * x) * (1.R) by A12,Def1
                .= z * x;
    end;
    hence z in center R by WEDDWITT:17;
    thus z in UnitGroup R by A8,A10,Th121;
    thus A = z*(1.(R,n)) by A10;
  end;
end;

theorem
  for A being invertible Matrix of n,R
  st (for B being invertible Matrix of n,R
      holds A * B = B * A)
  ex z being Element of R
  st z in center UnitGroup R & A = z*(1.(R,n))
proof
  let A be invertible Matrix of n,R;
  assume A1: for B being invertible Matrix of n,R holds A * B = B * A;
  :: Step 1: A must be commute with canMat(i,j,n,R)
  A2: for i,j being Nat st i <> j
  holds A * canMat(i,j,n,R) = canMat(i,j,n,R) * A
  proof
    let i,j be Nat;
    assume A3: i <> j;
    (1.R) * canMat(i,j,n,R) = canMat(i,j,n,R);
    then 1.(R,n) + canMat(i,j,n,R) is invertible Matrix of n,R
    by A3,Th57;
    then A * (1.(R,n) + canMat(i,j,n,R)) = (1.(R,n) + canMat(i,j,n,R)) * A
    by A1;
    hence A * canMat(i,j,n,R) = canMat(i,j,n,R) * A by Th59;
  end;

  :: Step 2: A must be diagonal
  A4: for i,j being Nat st [i,j] in Indices A & i <> j
      holds A * (i,j) = 0.R
  proof
    let i,j be Nat;
    set i2=i, j2=i, i0 = j, j0 = i;
    assume A5: [i,j] in Indices A;
    assume A6: i <> j;
    [i,j] in [:Seg n,Seg n:] by A5,MATRIX_0:24;
    then A7: i in Seg n & j in Seg n by ZFMISC_1:87;
    then [j,i] in [:Seg n,Seg n:] by ZFMISC_1:87;
    then A8: [j,i] in Indices canMat(i0,j0,n,R) by MATRIX_0:24;
    [i,i] in [:Seg n,Seg n:] by A7,ZFMISC_1:87;
    then A9: [i,i] in Indices A by MATRIX_0:24;
    hence A * (i,j) = (A * canMat(i0,j0,n,R)) * (i2,j2) by A8,Th55
                   .= ((canMat(i0,j0,n,R)) * A) * (i2,j2) by A2,A6
                   .= 0.R by A6,A8,A9,Th54;
  end;
  :: Step 3: A must commute with permutation matrices, which implies A
  :: must be a scalar matrix.
  :: A * canMat(i,j,n,R) = canMat(i,j,n,R) * A implies A*(i,i) = A*(j,j)
  A10: for i,j being Nat st [i,j] in Indices A
      holds A * (i,i) = A * (j,j)
  proof
    let i,j be Nat;
    assume A11: [i,j] in Indices A;
    per cases;
    suppose i = j;
      hence thesis;
    end;
    suppose A12: i <> j;
      A13: Indices A = [:Seg n,Seg n:] by MATRIX_0:24
                    .= Indices canMat(i,j,n,R) by MATRIX_0:24;
      hence A * (i,i) = (A * (canMat(i,j,n,R))) * (i,j) by A11,Th55
                    .= ((canMat(i,j,n,R)) * A) * (i,j) by A2,A12
                    .= A * (j,j) by A11,A13,Th54;
    end;
  end;
  :: The rest of the proof is as before
  per cases;
  suppose A14: n = 0;
    take z = 1.R;
    z = 1_(UnitGroup R) by Th111;
    then z in center UnitGroup R by GROUP_2:46;
    hence thesis by A14,MATRIX_0:45;
  end;
  suppose A15: n > 0;
    then 0 < 0 + n;
    then 1 <= n by NAT_1:19;
    then A16: [1,1] in Indices A by MATRIX_0:31;
    take z = A * (1,1);
    A17: len A = len (z* 1.(R,n)) & width A = width (z * 1.(R,n))
    proof
      thus len A = n by MATRIX_0:25
                .= len (z * 1.(R,n)) by MATRIX_0:25;
      thus width A = n by MATRIX_0:24
                  .= width (z * 1.(R,n)) by MATRIX_0:24;
    end;
    :: This follows from A2,A3
    for i,j being Nat st [i,j] in Indices A
    holds A*(i,j) = (z * (1.(R,n)))*(i,j)
    proof
      let i,j be Nat;
      assume A18: [i,j] in Indices A;
      Indices A = [:Seg n,Seg n:] by MATRIX_0:24
               .= Indices 1.(R,n) by MATRIX_0:24;
      then A19: [i,j] in Indices 1.(R,n) by A18;
      per cases;
      suppose A20: i = j;
        [1,i] in Indices A
        proof
          [1,1] in [:Seg n,Seg n:] by A16,MATRIX_0:24;
          then A21: 1 in Seg n by ZFMISC_1:87;
          [i,j] in [:Seg n,Seg n:] by A18,MATRIX_0:24;
          then i in Seg n by ZFMISC_1:87;
          then [1,i] in [:Seg n,Seg n:] by A21,ZFMISC_1:87;
          hence [1,i] in Indices A by MATRIX_0:24;
        end;
        hence A*(i,j) = z * 1.R by A10,A20
                     .= z * (1.(R,n) * (i,j)) by A19,A20,MATRIX_1:def 3
                     .= (z * (1.(R,n)))*(i,j) by A19,MATRIX_3:def 5;
      end;
      suppose A22: i <> j;
        hence A*(i,j) = z * 0.R by A4,A18
                    .= z * (1.(R,n) * (i,j)) by A19,A22,MATRIX_1:def 3
                    .= (z * (1.(R,n)))*(i,j) by A19,MATRIX_3:def 5;
      end;
    end;
    :: Then 'A' must be a scalar matrix.
    then A23: A = z * 1.(R,n) by A17,MATRIX_0:21;
    :: ...but how to prove that z is in the center of R?
    then reconsider z9 = z as Element of UnitGroup R
    by A15,Th121,STRUCT_0:def 5;
    for x9 being Element of UnitGroup R
    holds z9 * x9 = x9 * z9
    proof
      let x9 be Element of UnitGroup R;
      x9 in units R;
      then reconsider x = x9 as Element of R;
      A24: x * 1.(R,n) is invertible by Th120,STRUCT_0:def 5;
      A25: ((x * z) * 1.(R,n)) = ((x * z) * 1.(R,n)) * 1.(R,n) by MATRIX_3:19
                              .= ((x * 1.(R,n)) * z) * 1.(R,n) by Th101
                              .= (x * 1.(R,n)) * A by A23,Th102
                              .= (z * 1.(R,n)) * (x * 1.(R,n)) by A23,A24,A1
                              .= ((z * 1.(R,n)) * x) * 1.(R,n) by Th102
                              .= ((z * x) * 1.(R,n)) * 1.(R,n) by Th101
                              .= (z * x) * 1.(R,n) by MATRIX_3:19;
      Indices 1.(R,n) = [:Seg n, Seg n:] by MATRIX_0:24
                     .= Indices A by MATRIX_0:24;
      then A26: [1,1] in Indices 1.(R,n) by A16;
      thus x9 * z9 = (x * z) * (1.R) by Th110
                  .= (x * z) * ((1.(R,n)) * (1,1)) by A26,MATRIX_1:def 3
                  .= ((x * z) * 1.(R,n)) * (1,1) by A26,MATRIX_3:def 5
                  .= (z * x) * ((1.(R,n)) * (1,1)) by A25,A26,MATRIX_3:def 5
                  .= (z * x) * (1.R) by A26,MATRIX_1:def 3
                  .= z9 * x9 by Th110;
    end;
    hence thesis by A23,GROUP_5:77;
  end;
end;

theorem Th125:
  for R1,R2 being Ring
  st R1,R2 are_isomorphic
  holds UnitGroup R1, UnitGroup R2 are_isomorphic
proof
  let R1,R2 be Ring;
  assume R1,R2 are_isomorphic;
  then consider phi being Function of R1,R2 such that
  A1: phi is RingIsomorphism by QUOFIELD:def 23;
  set psi = phi | (the carrier of UnitGroup R1);
  A2: psi is Function of units R1, R2 by FUNCT_2:32;
  then A3: dom psi = units R1 by FUNCT_2:def 1;
  now
    let y be object;
    assume y in rng psi;
    then consider x being object such that
    A4: x in dom psi & psi.x = y by FUNCT_1:def 3;
    reconsider x9 = x as unital Element of R1 by A3,A4,Th107;
    psi.x in the carrier of R2 by A2,A3,A4,FUNCT_2:5;
    then reconsider y9=y as Element of R2 by A4;
    consider w being Element of R1 such that
    A5: x9 * w = 1.R1 & w * x9 = 1.R1
    by GCD_1:def 2;
    (phi.w) * y9 = 1.R2 & y9 * (phi.w) = 1.R2
    proof
      x9 in the carrier of UnitGroup R1;
      then A6: phi.x9 = y9 by A4,FUNCT_1:49;
      thus 1.R2 = phi.(w * x9) by A1,A5,Th1
               .= (phi.w) * y9 by A1,A6,GROUP_6:def 6;
      thus 1.R2 = phi.(x9 * w) by A1,A5,Th1
               .= y9 * (phi.w) by A1,A6,GROUP_6:def 6;
    end;
    then y9 is unital by GCD_1:def 2;
    hence y in units R2;
  end;
  then reconsider psi as Function of UnitGroup R1, UnitGroup R2
    by A3,FUNCT_2:2,TARSKI:def 3;
  A7: for x being Element of R1
  st x in units R1 holds psi.x = phi.x by FUNCT_1:49;
  A8: for a being Element of UnitGroup R1
  ex x being Element of R1 st a = x & phi.x = psi.a
  proof
    let a be Element of UnitGroup R1;
    a in units R1;
    then reconsider x = a as Element of R1;
    take x;
    thus a = x;
    thus phi.x = psi.a by FUNCT_1:49;
  end;

  A9: psi is one-to-one by A1,FUNCT_1:52;

  for a,b being Element of UnitGroup R1
  holds psi.(a * b) = (psi.a) * (psi.b)
  proof
    let a,b be Element of UnitGroup R1;
    consider x being Element of R1 such that
    A10: a = x & phi.x = psi.a by A8;
    consider y being Element of R1 such that
    A11: b = y & phi.y = psi.b by A8;
    x is unital & y is unital by A10,A11,Th107;
    then x * y in units R1;
    then psi.(x * y) = phi.(x * y) by A7
                    .= (phi.x) * (phi.y) by A1,GROUP_6:def 6
                    .= (psi.a) * (psi.b)
                      by A10,A11,FUNCT_1:49,ZFMISC_1:87;
    hence psi.(a * b) = (psi.a) * (psi.b) by A10,A11,Th110;
  end;
  then reconsider psi as Homomorphism of UnitGroup R1,UnitGroup R2
  by GROUP_6:def 6;
  for y being object st y in the carrier of UnitGroup R2
  ex x being object st x in the carrier of UnitGroup R1 & y = psi.x
  proof
    let y be object;
    assume A13: y in the carrier of UnitGroup R2;
    then reconsider y9 = y as Element of UnitGroup R2;
    reconsider y0 = y as Element of R2 by A13;
    A14: rng phi = the carrier of R2 by A1,FUNCT_2:def 3;
    consider x0 being object such that
    A15: x0 in dom phi & y0 = phi.x0
    by A14,FUNCT_1:def 3;
    reconsider x0 as Element of R1 by A15;
    consider z0 being Element of R2 such that
    A16: y0 * z0 = 1.R2 & z0 * y0 = 1.R2
      by A13,Th107,GCD_1:def 2;
    consider w0 being object such that
    A17: w0 in dom phi & z0 = phi.w0
      by A14,FUNCT_1:def 3;
    reconsider w0 as Element of R1 by A17;
    phi.(w0 * x0) = 1.R2 by A1,A15,A16,A17,GROUP_6:def 6;
    then A18: w0 * x0 = 1.R1 by A1,Th11;
    phi.(x0 * w0) = 1.R2 by A1,A15,A16,A17,GROUP_6:def 6;
    then x0 * w0 = 1.R1 by A1,Th11;
    then A19: x0 is unital by A18,GCD_1:def 2;
    take x0;
    A20: x0 in units R1 by A19;
    hence x0 in the carrier of UnitGroup R1;
    thus y = psi.x0 by A15,A20,A7;
  end;
  then rng psi = the carrier of UnitGroup R2 by FUNCT_2:10;
  then psi is onto by FUNCT_2:def 3;
  hence UnitGroup R1, UnitGroup R2 are_isomorphic by A9,GROUP_6:def 11;
end;

begin :: General Linear Group over a ring

:: This can be weakened to semirings
definition
  let n, R;
  func GL(n,R) -> strict Group equals
  UnitGroup Matrix_ring(n,R);
  coherence;
end;

registration
  let R;
  cluster GL(0,R) -> trivial;
  coherence;
end;

theorem Th126:
  for x being object
  holds x is Element of GL(n, R) iff x is invertible Matrix of n, R
proof
  let x be object;
  set M = Matrix_ring(n,R);
  hereby
    assume x is Element of GL(n, R);
    then x in units (Matrix_ring(n,R));
    then reconsider x2=x as unital Element of Matrix_ring(n, R) by Th107;
    consider y being Element of Matrix_ring(n, R) such that
    A1: x2 * y = 1.M & y * x2 = 1.M by GCD_1:def 2;
    reconsider X=x2, Y=y as Matrix of n,R by Th72;
    Y is_reverse_of X
    proof
      X * Y = 1.(R,n) by A1,Th75
           .= Y * X by A1,Th75;
      hence thesis by A1,Th75,MATRIX_6:def 2;
    end;
    hence x is invertible Matrix of n, R by MATRIX_6:def 3;
  end;
  assume A2: x is invertible Matrix of n, R;
  x is unital Element of Matrix_ring(n, R)
  proof
    reconsider x2=x as invertible Matrix of n,R by A2;
    consider y being Matrix of n,R such that
    A3: y is_reverse_of x2 by MATRIX_6:def 3;
    A4: y*x2 = One(R,n) & x2*y=One(R,n) by A3,MATRIX_6:def 2;
    reconsider x3=x2,y3=y as Element of Matrix_ring(n,R) by Th72;
    y3*x3 = 1.M & x3*y3 = 1.M by A4,Th75;
    hence thesis by GCD_1:def 2;
  end;
  hence x is Element of GL(n, R) by Th107;
end;

registration
  let R, n;
  cluster GL(n, R) -> (n,R)-matrix-membered;
  coherence
  proof
    the carrier of GL(n,R) is (n,R)-matrix-membered by Def3;
    hence thesis;
  end;
end;

registration
  let R, n;
  cluster the carrier of GL(n,R) -> non empty;
  coherence;
  cluster the carrier of GL(n,R) -> (n,R)-matrix-membered;
  coherence by Def3; ::: give general reg. instead of this one
end;

theorem Th127:
  for x,y being Element of GL(n,R)
  for X,Y being Matrix of n,R
  st X = x & Y = y
  holds X * Y = x * y
proof
  let x,y be Element of GL(n,R);
  let X,Y be Matrix of n,R;
  assume A1: X = x & Y = y;
  reconsider x2=X,y2=Y as Element of Matrix_ring(n,R) by Th72;
  thus x * y = x2 * y2 by A1,Th110
            .= X * Y by Th75;
end;

scheme GLSubset{ n() -> Nat, R() -> Ring, P[Matrix of R()] } :
  ex A being Subset of GL(n(), R())
  st for X being invertible Matrix of n(), R()
  holds X in A iff P[X]
proof
  set A = {g where g is Element of GL(n(), R()) : ex X being
  Matrix of n(), R() st g = X & P[X] };
  for g being object st g in A holds g in the carrier of GL(n(), R())
  proof
    let g be object;
    assume g in A;
    then ex g1 being Element of GL(n(),R())
    st g = g1 & ex X being Matrix of n(),R() st g1 = X & P[X];
    hence g in the carrier of GL(n(), R());
  end;
  then reconsider A as Subset of GL(n(), R()) by TARSKI:def 3;
  take A;
  thus for X being invertible Matrix of n(), R()
  holds X in A iff P[X]
  proof
    let X be invertible Matrix of n(), R();
    hereby
      assume X in A;
      then ex g1 being Element of GL(n(),R())
      st X = g1 & ex X1 being Matrix of n(),R() st g1 = X1 & P[X1];
      hence P[X];
    end;
    reconsider g = X as Element of GL(n(),R()) by Th126;
    assume P[X];
    then g = X & P[X];
    hence X in A;
  end;
end;

scheme GLSubset2{ n() -> Nat, R() -> Ring, P[Matrix of R()] } :
  ex A being Subset of GL(n(), R())
  st for X being Matrix of n(), R() st X is invertible
  holds X in A iff P[X]
proof
  set A = {g where g is Element of GL(n(), R()) : ex X being
  Matrix of n(), R() st g = X & P[X] };
  for g being object st g in A holds g in the carrier of GL(n(), R())
  proof
    let g be object;
    assume g in A;
    then ex g1 being Element of GL(n(),R())
    st g = g1 & ex X being Matrix of n(),R() st g1 = X & P[X];
    hence g in the carrier of GL(n(), R());
  end;
  then reconsider A as Subset of GL(n(), R()) by TARSKI:def 3;
  take A;
  thus for X being Matrix of n(), R() st X is invertible
  holds X in A iff P[X]
  proof
    let X be Matrix of n(), R();
    assume A1: X is invertible;
    hereby
      assume X in A;
      then ex g1 being Element of GL(n(),R())
      st X = g1 & ex X1 being Matrix of n(),R() st g1 = X1 & P[X1];
      hence P[X];
    end;
    assume A2: P[X];
    reconsider g = X as Element of GL(n(),R()) by A1,Th126;
    g = X & P[X] by A2;
    hence X in A;
  end;
end;

theorem Th128:
  for X being Matrix of n, R
  holds X is Element of GL(n,R) iff X is invertible by Th126;

theorem Th129:
  1.(R, n) is Element of GL(n, R) by Th126;

theorem Th130:
  1_GL(n,R) = 1.(R,n)
proof
  reconsider I=1.(R,n) as Element of GL(n,R) by Th129;
  for x being Element of GL(n,R)
  holds x * I = x & I * x = x
  proof
    let x be Element of GL(n,R);
    reconsider X = x as invertible Matrix of n,R by Th126;
    thus x * I = X * (1.(R,n)) by Th127
              .= x by MATRIX_3:19;
    thus I * x = (1.(R,n)) * X by Th127
              .= x by MATRIX_3:18;
  end;
  hence thesis by GROUP_1:4;
end;

theorem Th131:
  for x being Element of GL(n, R)
  for X being invertible Matrix of n,R st x = X
  holds x" = X~
proof
  let x be Element of GL(n, R);
  let X be invertible Matrix of n,R;
  assume A1: x = X;
  reconsider h = X~ as Element of GL(n,R) by Th126;
  X~ is_reverse_of X by MATRIX_6:def 4;
  then X~ * X = X * X~ & X~ * X = 1.(R,n) by MATRIX_6:def 2;
  then X * X~ = 1_GL(n,R) & X~ * X = 1_GL(n,R) by Th130;
  then 1_GL(n,R) = x * h & 1_GL(n,R) = h * x by A1,Th127;
  hence x" = X~ by GROUP_1:5;
end;

theorem
  for g being Element of GL(n,R)
  for X,Y being Matrix of n,R st X = g
  holds Y = (inverse_op GL(n,R)).g iff Y is_reverse_of X
proof
  let g be Element of GL(n,R);
  let X,Y be Matrix of n,R;
  assume A1: X = g;
  hereby
    assume Y = (inverse_op GL(n,R)).g;
    then A2: Y = g" by GROUP_1:def 6;
    A3: X * Y = g * (g ") by A1,A2,Th127
             .= 1_(GL(n,R)) by GROUP_1:def 5
             .= 1.(R,n) by Th130;
    Y * X = (g ") * g by A1,A2,Th127
         .= 1_(GL(n,R)) by GROUP_1:def 5
         .= 1.(R,n) by Th130;
    hence Y is_reverse_of X by A3,MATRIX_6:def 2;
  end;
  assume A4: Y is_reverse_of X;
  then reconsider h = Y as Element of GL(n,R) by Th128,MATRIX_6:def 3;
  A5: Y * X = X * Y & Y * X = 1.(R,n) by A4,MATRIX_6:def 2;
  A6: 1_(GL(n,R)) = 1.(R,n) by Th130
                 .= h * g by A1,A5,Th127;
  1_(GL(n,R)) = 1.(R,n) by Th130
             .= g * h by A1,A5,Th127;
  then h = g" by A6,GROUP_1:5
        .= (inverse_op GL(n,R)).g by GROUP_1:def 6;
  hence Y = (inverse_op GL(n,R)).g;
end;

scheme GLSubgroup{ n() -> Nat, R() -> Ring, P[Matrix of R()] } :
  ex H being strict Subgroup of GL(n(), R())
  st for X being invertible Matrix of n(), R()
  holds X in H iff P[X]
provided
A1: for X,Y being invertible Matrix of n(), R()
    st P[X] & P[Y]
    holds P[X * Y] and
A2: for X being invertible Matrix of n(), R()
    st P[X] holds P[X~] and
A3: P[1.(R(), n())]
proof
  consider A being Subset of GL(n(), R()) such that
  A4: for X being invertible Matrix of n(), R()
  holds X in A iff P[X]
  from GLSubset;
  A5: for g1,g2 being Element of GL(n(), R())
  st g1 in A & g2 in A
  holds g1 * g2 in A
  proof
    let g1,g2 be Element of GL(n(), R());
    reconsider X1 = g1, X2 = g2 as invertible Matrix of n(), R() by Th126;
    A6: X1 * X2 is invertible by MATRIX_6:45;
    assume g1 in A & g2 in A;
    then P[X1] & P[X2] by A4;
    then (X1 * X2) in A by A1,A4,A6;
    hence g1 * g2 in A by Th127;
  end;
  A7: for g being Element of GL(n(), R())
  st g in A
  holds g" in A
  proof
    let g be Element of GL(n(), R());
    reconsider X = g as invertible Matrix of n(), R() by Th126;
    assume g in A;
    then P[X~] by A2,A4;
    then X~ in A by A4;
    hence g" in A by Th131;
  end;
  A <> {} by A3,A4;
  then consider H being strict Subgroup of GL(n(), R()) such that
  A8: the carrier of H = A
  by A5,A7,GROUP_2:52;
  take H;
  thus thesis by A4,A8,STRUCT_0:def 5;
end;

scheme GLSubgroup2{ n() -> Nat, R() -> Ring, P[Matrix of n(), R()] } :
  ex H being strict Subgroup of GL(n(), R())
  st for X being invertible Matrix of n(), R()
  holds X in H iff P[X]
provided
A1: for X,Y being invertible Matrix of n(), R()
    st P[X] & P[Y]
    holds P[X * Y] and
A2: for X being invertible Matrix of n(), R()
    st P[X] holds P[X~] and
A3: P[1.(R(), n())]
proof
  defpred Q[Matrix of R()] means
  ex M being Matrix of n(), R() st M = $1 & P[M];

  A4: for X,Y being invertible Matrix of n(), R()
      st Q[X] & Q[Y]
      holds Q[X * Y] by A1;
  A5: for X being invertible Matrix of n(), R()
      st Q[X] holds Q[X~] by A2;
  A6: Q[1.(R(), n())] by A3;

  consider H being strict Subgroup of GL(n(), R()) such that
  A7: for X being invertible Matrix of n(), R()
  holds X in H iff Q[X] from GLSubgroup(A4, A5, A6);

  take H;

  thus for X being invertible Matrix of n(), R()
  holds X in H iff P[X]
  proof
    let X be invertible Matrix of n(), R();
    Q[X] iff P[X];
    hence thesis by A7;
  end;
end;

begin :: Center of general linear group

theorem
  for X being Element of GL(n,R)
  st (ex z being Element of R st z in center R & X = z * 1.(R,n))
  holds X in center GL(n,R)
proof
  let X be Element of GL(n,R);
  given z being Element of R such that
  A1: z in center R & X = z * 1.(R,n);
  reconsider A = X as Matrix of n,R by Th126;
  for Y being Element of GL(n,R)
  holds X * Y = Y * X
  proof
    let Y be Element of GL(n,R);
    reconsider B = Y as Matrix of n,R by Th126;
    thus X * Y = A * B by Th127
              .= B * A by A1,Th100
              .= Y * X by Th127;
  end;
  hence X in center GL(n,R) by GROUP_5:77;
end;

theorem Th134:
  for X being invertible Matrix of n,R st n <> 1
  holds X in center GL(n,R) iff
  ex z being Element of R
  st z in center R & z in UnitGroup R & X = z * 1.(R,n)
proof
  let X be invertible Matrix of n,R;
  assume A1: n <> 1;
  reconsider g = X as Element of GL(n,R) by Th126;
  hereby
    assume A2: X in center GL(n,R);
    for Y being invertible Matrix of n,R
    holds X * Y = Y * X
    proof
      let Y be invertible Matrix of n,R;
      reconsider h = Y as Element of GL(n,R) by Th126;
      thus X * Y = g * h by Th127
                .= h * g by A2,GROUP_5:77
                .= Y * X by Th127;
    end;
    then consider z being Element of R such that
    A3: z in center R & z in UnitGroup R & X = z*(1.(R,n))
    by A1,Th123;
    take z;
    thus z in center R by A3;
    thus z in UnitGroup R by A3;
    thus X = z * 1.(R,n) by A3;
  end;
  given z being Element of R such that
  A4: z in center R & z in UnitGroup R & X = z * 1.(R,n);
  for h being Element of GL(n,R)
  holds g * h = h * g
  proof
    let h be Element of GL(n,R);
    reconsider Y = h as invertible Matrix of n,R by Th126;
    thus g * h = X * Y by Th127
              .= Y * (z * 1.(R,n)) by A4,Th100
              .= h * g by A4,Th127;
  end;
  hence X in center GL(n,R) by GROUP_5:77;
end;

theorem Th135:
  for r being Element of R st r in center UnitGroup R
  for s being Element of R st s in UnitGroup R
  holds r * s = s * r
proof
  let r be Element of R;
  assume A1: r in center UnitGroup R;
  then reconsider r9 = r as Element of UnitGroup R
  by GROUP_2:40,STRUCT_0:def 5;
  let s be Element of R;
  assume s in UnitGroup R;
  then reconsider s9 = s as Element of UnitGroup R by STRUCT_0:def 5;
  thus r * s = r9 * s9 by Th110
            .= s9 * r9 by A1,GROUP_5:77
            .= s * r by Th110;
end;

theorem Th136:
  for X being invertible Matrix of n,R st n = 1
  holds X in center GL(n,R) iff
  ex z being Element of R
  st z in center UnitGroup R & X = z * 1.(R,n)
proof
  let X be invertible Matrix of n,R;
  reconsider g = X as Element of GL(n,R) by Th126;
  assume A1: n = 1;
  hereby
    assume A2: X in center GL(n,R);
    for Y being invertible Matrix of n,R
    holds X * Y = Y * X
    proof
      let Y be invertible Matrix of n,R;
      reconsider h = Y as Element of GL(n,R) by Th126;
      thus X * Y = g * h by Th127
                .= h * g by A2,GROUP_5:77
                .= Y * X by Th127;
    end;
    then consider z being Element of R such that
    A3: z in center UnitGroup R & X = z*(1.(R,n)) by A1,Th123;
    take z;
    thus z in center UnitGroup R by A3;
    thus X = z * 1.(R,n) by A3;
  end;
  given z being Element of R such that
  A4: z in center UnitGroup R & X = z * 1.(R,n);
  :: A1,Th14 gives us X = <*<* (X * (1,1)) *>*>
  for h being Element of GL(n,R)
  holds g * h = h * g
  proof
    let h be Element of GL(n,R);
    reconsider Y = h as invertible Matrix of n,R by Th126;
    A5: Y = (Y * (1,1)) * 1.(R,1) by A1,Th38;
    set Y11 = Y * (1,1);
    A6: Y11 in UnitGroup R by A1,A5,Th121;
    thus h * g = Y * X by Th127
              .= ((Y11 * 1.(R,n)) * z) * 1.(R,n) by A1,A4,A5,Th102
              .= ((Y11 * z) * 1.(R,n)) * 1.(R,n) by Th101
              .= ((z * Y11) * 1.(R,n)) * 1.(R,n) by A4,A6,Th135
              .= ((z * 1.(R,n)) * Y11) * 1.(R,n) by Th101
              .= (z * 1.(R,n)) * (Y11 * 1.(R,n)) by Th102
              .= g * h by A1,A4,A5,Th127;
  end;
  hence X in center GL(n,R) by GROUP_5:77;
end;

:: The results about center GL(1,R) is so surprising at first glance,
:: because our intuition expects the commutative R case to generalize to
:: the general situation. But we're not mistaken, and here's a slick proof.
theorem
  center GL(1,R), center UnitGroup R are_isomorphic
proof
  GL(1,R), UnitGroup R are_isomorphic by Th79,Th125;
  hence center GL(1,R), center UnitGroup R are_isomorphic
  by Th12;
end;

theorem
  for R being commutative Ring
  for X being invertible Matrix of n,R
  holds X in center GL(n,R) iff
  ex z being Element of R
  st z in center R & z in UnitGroup R & X = z * 1.(R,n)
proof
  let R be commutative Ring;
  let X be invertible Matrix of n,R;
  per cases;
  suppose A1: n = 1;
    hereby
      assume X in center GL(n,R);
      then consider z being Element of R such that
      A2: z in center UnitGroup R & X = z * 1.(R,n)
      by A1,Th136;
      take z;
      thus z in center R & z in UnitGroup R by A2,Th118;
      thus X = z * 1.(R,n) by A2;
    end;
    given z being Element of R such that
    A3: z in center R & z in UnitGroup R & X = z * 1.(R,n);
    z in center (UnitGroup R) by A3,Th118;
    hence X in center GL(n,R) by A1,A3,Th136;
  end;
  suppose n <> 1;
    hence thesis by Th134;
  end;
end;

begin :: Extension of scalars for general linear group

theorem Th139:
  for M1 being Matrix of n,R
  for M2 being Matrix of n,S
  st M1 = M2 & M2 is invertible
  holds M1 is invertible
proof
  let M1 be Matrix of n,R;
  let M2 be Matrix of n,S;
  assume A1: M1 = M2;
  assume M2 is invertible;
  then consider N2 being Matrix of n,S such that
  A2: M2 is_reverse_of N2 by MATRIX_6:def 3;
  A3: M2 * N2 = N2 * M2 & M2 * N2 = 1.(S,n) by A2,MATRIX_6:def 2;
  reconsider N1 = N2 as Matrix of n,R by Th82;
  M1 * N1 = N1 * M1 & M1 * N1 = 1.(R,n)
  proof
    thus M1 * N1 = M2 * N2 by A1,Th92
                .= N1 * M1 by A1,A3,Th92;
    thus M1 * N1 = M2 * N2 by A1,Th92
                .= 1.(R,n) by A3,Th95;
  end;
  hence M1 is invertible by MATRIX_6:def 2,def 3;
end;

theorem Th140:
  the carrier of GL(n,S) c= the carrier of GL(n,R)
proof
  for x being object
  st x in the carrier of GL(n,S)
  holds x in the carrier of GL(n,R)
  proof
    let x be object;
    assume x in the carrier of GL(n,S);
    then reconsider g = x as Element of GL(n,S);
    reconsider M1 = g as invertible Matrix of n,S by Th126;
    reconsider M2 = M1 as Matrix of n,R by Th82;
    M2 is Element of GL(n,R) by Th128,Th139;
    hence x in the carrier of GL(n,R);
  end;
  hence the carrier of GL(n,S) c= the carrier of GL(n,R) by TARSKI:def 3;
end;

theorem Th141:
  the multF of GL(n,S) = (the multF of GL(n,R)) || (the carrier of GL(n,S))
proof
  set US = the carrier of GL(n,S);
  set UR = the carrier of GL(n,R);
  set fS = the multF of GL(n,S);
  set fR = the multF of GL(n,R);
  A1: US c= UR by Th140;
  then A2: [:US,US:] c= [:UR,UR:] by ZFMISC_1:96;
  A3: (fR || US) is Function of [:US,US:],UR
  by A2,FUNCT_2:32;
  A4: fS is Function of [:US,US:],UR by A1,FUNCT_2:7;
  for x,y being Element of US
  holds fS.(x,y)=(fR || US).(x,y)
  proof
    let x,y be Element of US;
    reconsider x9=x,y9=y as Element of GL(n,S);
    A5: [x,y] in [:US,US:];
    then fS.(x,y) is Element of GL(n,R) by A4,FUNCT_2:5;
    then reconsider LHS = fS.(x,y) as Matrix of n,R by Th126;
    (fR || US).(x,y) in UR by A3,A5,FUNCT_2:5;
    then reconsider RHS = (fR || US).(x,y) as Matrix of n,R by Th126;
    reconsider a = x9, b = y9 as invertible Matrix of n,S by Th126;
    reconsider X = x9, Y = y9 as Element of GL(n,R) by A1,TARSKI:def 3;
    reconsider A = X, B = Y as invertible Matrix of n,R by Th126;
    thus fS.(x,y) = x9 * y9
                 .= a * b by Th127
                 .= A * B by Th92
                 .= X * Y by Th127
                 .= (fR || US).(x,y) by FUNCT_1:49,ZFMISC_1:87;
  end;
  hence fS = fR || US by A3,A4,BINOP_1:2;
end;

theorem
  GL(n,S) is strict Subgroup of GL(n,R)
proof
  the carrier of GL(n,S) c= the carrier of GL(n,R)
  & the multF of GL(n,S) = (the multF of GL(n,R)) || (the carrier of GL(n,S))
  by Th140,Th141;
  hence thesis by GROUP_2:def 5;
end;

begin :: Appendix 1: Matrix inversion as a unary operator

theorem Th143:
  for x being Element of Matrix_ring(n,R)
  holds x is invertible
  iff ex X being invertible Matrix of n,R st X = x
proof
  let x be Element of Matrix_ring(n,R);
  hereby
    assume A1: x is invertible;
    then consider a being Element of Matrix_ring(n,R) such that
    A2: a * x = 1.(Matrix_ring(n,R))
    by ALGSTR_0:def 27;
    consider b being Element of Matrix_ring(n,R) such that
    A3: x * b = 1.(Matrix_ring(n,R))
    by A1,ALGSTR_0:def 28;
    A4: a = a * (1.Matrix_ring(n,R))
         .= (a * x) * b by A3,GROUP_1:def 3
         .= b by A2;
    reconsider X = x, A = a as Matrix of n,R by Th72;
    A is_reverse_of X
    proof
      A * X = 1.(R,n) by A2,Th75
           .= X * A by A3,A4,Th75;
      hence thesis by A2,Th75,MATRIX_6:def 2;
    end;
    then reconsider X as invertible Matrix of n,R by MATRIX_6:def 3;
    take X;
    thus X = x;
  end;
  given X being invertible Matrix of n,R such that
  A5: X = x;
  consider A being Matrix of n,R such that
  A6: X is_reverse_of A by MATRIX_6:def 3;
  reconsider a = A as Element of Matrix_ring(n,R) by Th72;
  A7: X * A = A * X & X * A = 1.(R,n) by A6,MATRIX_6:def 2;
  A8: x * a = (1.Matrix_ring(n,R)) by A5,A7,Th75;
  a * x = (1.Matrix_ring(n,R)) by A5,A7,Th75;
  then x is left_invertible & x is right_invertible
  by A8,ALGSTR_0:def 27,def 28;
  hence x is invertible;
end;

registration
  let n, R;
  cluster invertible for Element of Matrix_ring(n, R);
  existence by Th143;
end;

theorem
  for x being object
  holds x is invertible Element of Matrix_ring(n,R)
  iff x is invertible Matrix of n,R
proof
  let x be object;
  hereby
    assume x is invertible Element of Matrix_ring(n,R);
    then ex X9 being invertible Matrix of n,R st X9 = x by Th143;
    hence x is invertible Matrix of n,R;
  end;
  assume x is invertible Matrix of n,R;
  hence x is invertible Element of Matrix_ring(n,R) by Th143,Th72;
end;

definition
  let n,R;
  func n-invertible_Matrices_over R -> Subset of n-Matrices_over R
  equals
  { X where X is Element of n-Matrices_over R :
  X is invertible Matrix of n,R };
  coherence
  proof
    set IT = { X where X is Element of n-Matrices_over R :
               X is invertible Matrix of n,R };
    for x being object st x in IT holds x in n-Matrices_over R
    proof
      let x be object;
      assume x in IT;
      then ex X being Element of n-Matrices_over R st
      X = x & X is invertible Matrix of n,R;
      hence x in n-Matrices_over R;
    end;
    hence thesis by TARSKI:def 3;
  end;
end;

theorem Th145:
  for x being object holds
  x in n-invertible_Matrices_over R iff x is invertible Matrix of n,R
proof
  let x be object;
  hereby
    assume x in n-invertible_Matrices_over R;
    then ex X being Element of n-Matrices_over R
    st X = x & X is invertible Matrix of n,R;
    hence x is invertible Matrix of n,R;
  end;
  assume A1: x is invertible Matrix of n,R;
  then x is Element of n-Matrices_over R by MATRIX_1:2;
  hence x in n-invertible_Matrices_over R by A1;
end;

registration
  let n,R;
  cluster n-invertible_Matrices_over R -> non empty;
  coherence
  proof
    1.(R,n) in n-invertible_Matrices_over R by Th145;
    hence thesis;
  end;
end;

theorem Th146:
  the carrier of GL(n,R) = n-invertible_Matrices_over R
proof
  for x being object
  holds x in the carrier of GL(n,R) iff x in n-invertible_Matrices_over R
  proof
    let x be object;
    x is Element of GL(n,R) iff x in the carrier of GL(n,R);
    then x in the carrier of GL(n,R) iff x is invertible Matrix of n,R
    by Th126;
    hence thesis by Th145;
  end;
  hence the carrier of GL(n,R) = n-invertible_Matrices_over R by TARSKI:2;
end;

theorem
  n-invertible_Matrices_over R is (matrix_mult (n,R))-binopclosed
proof
  set U = n-invertible_Matrices_over R;
  set V = n-Matrices_over R;
  for x being set st x in [: U, U :]
  holds (matrix_mult (n,R)).x in U
  proof
    let x be set;
    assume x in [: U, U :];
    then consider a,b being object such that
    A1: a in U & b in U & x = [a,b]
    by ZFMISC_1:def 2;
    reconsider A=a,B=b as Element of V by A1;
    A2: A * B is invertible Matrix of n,R
    proof
      reconsider X = A, Y = B as invertible Matrix of n,R by A1,Th145;
      X * Y is invertible & (X * Y)~ = (Y ~) * (X ~) by MATRIX_6:36;
      hence thesis;
    end;
    (matrix_mult (n,R)).x = (matrix_mult (n,R)).(A, B) by A1
                         .= A*B by Def5;
    hence (matrix_mult (n,R)).x in U by A2,Th145;
  end;
  hence thesis by REALSET1:def 1;
end;

theorem Th148:
  One(R,n) is_a_unity_wrt matrix_mult(n,R)
proof
  set mu = matrix_mult(n,R);
  for x being Element of n-Matrices_over R
  holds mu.(One(R,n), x) = x & mu.(x, One(R,n)) = x
  proof
    let x be Element of n-Matrices_over R;
    reconsider X = x as Matrix of n,R;
    thus mu.(One(R,n), x) = (1.(R,n)) * X by Def5
                         .= x by MATRIX_3:18;
    thus mu.(x, One(R,n)) = X * (1.(R,n)) by Def5
                         .= x by MATRIX_3:19;
  end;
  hence One(R,n) is_a_unity_wrt mu by BINOP_1:3;
end;

registration
  let n,R;
  cluster matrix_mult(n,R) -> associative;
  coherence
  proof
    set mu = matrix_mult(n,R);
    for a,b,c being Element of n-Matrices_over R
    holds mu.(a, mu.(b, c)) = mu.(mu.(a,b), c)
    proof
      let a,b,c be Element of n-Matrices_over R;
      reconsider A=a,B=b,C=c as Matrix of n,R;
      reconsider bc = B*C, ab = A*B as Element of n-Matrices_over R
      by MATRIX_1:2;
      A1: len A = n & width A = n & len B = n & width B = n & len C = n &
      width C = n by MATRIX_0:24;
      thus mu.(a, mu.(b, c)) = mu.(a, bc) by Def5
                            .= A*(B*C) by Def5
                            .= (A*B)*C by A1,MATRIX_3:33
                            .= mu.(ab,c) by Def5
                            .= mu.(mu.(a,b), c) by Def5;
    end;
    hence thesis by BINOP_1:def 3;
  end;
  cluster matrix_mult(n,R) -> having_a_unity;
  coherence
  proof
    ex x being Element of n-Matrices_over R
    st x is_a_unity_wrt matrix_mult(n,R)
    proof
      take One(R,n);
      thus thesis by Th148;
    end;
    hence thesis by SETWISEO:def 2;
  end;
end;

theorem
  One(R,n) = the_unity_wrt matrix_mult(n,R)
proof
  ex e being Element of n-Matrices_over R
  st e is_a_unity_wrt matrix_mult(n,R)
  proof
    take e = One(R,n);
    thus e is_a_unity_wrt matrix_mult(n,R) by Th148;
  end;
  then A1: (the_unity_wrt matrix_mult(n,R)) is_a_unity_wrt (matrix_mult(n,R))
  by BINOP_1:def 8;
  One(R,n) is_a_unity_wrt matrix_mult(n,R) by Th148;
  hence thesis by A1,BINOP_1:10;
end;

definition
  let n,R;
  func matrix_inv(n,R) -> UnOp of n-invertible_Matrices_over R means
  :Def12:
  for x being Element of n-invertible_Matrices_over R
  for X being invertible Matrix of n,R st x = X
  holds it.x = X ~;
  existence
  proof
    deffunc F1() = n-invertible_Matrices_over R;
    defpred P[object,object] means
    ex X being invertible Matrix of n,R st $1 = X & $2 = X~;
    A1: for x being object st x in F1()
    ex y being object st y in F1() & P[x, y]
    proof
      let x be object;
      assume x in F1();
      then reconsider X = x as invertible Matrix of n,R by Th145;
      take y = X ~;
      thus y in F1() by Th145;
      thus P[x, y];
    end;
    consider f being Function of F1(), F1() such that
    A2: for x being object st x in F1() holds P[x, f.x]
    from FUNCT_2:sch 1(A1);
    take f;
    thus for x being Element of n-invertible_Matrices_over R
    for X being invertible Matrix of n,R st x = X
    holds f.x = X ~
    proof
      let x be Element of n-invertible_Matrices_over R;
      let X be invertible Matrix of n,R;
      assume A3: x = X;
      P[x, f.x] by A2;
      hence f.x = X ~ by A3;
    end;
  end;
  uniqueness
  proof
    defpred P[UnOp of n-invertible_Matrices_over R] means
    for x being Element of n-invertible_Matrices_over R
    for X being invertible Matrix of n,R st x = X
    holds $1.x = X ~;
    let f1,f2 be UnOp of n-invertible_Matrices_over R;
    assume A4: P[f1];
    assume A5: P[f2];
    for x being Element of n-invertible_Matrices_over R
    holds f1.x = f2.x
    proof
      let x be Element of n-invertible_Matrices_over R;
      reconsider X = x as invertible Matrix of n,R by Th145;
      thus f1.x = X~ by A4
               .= f2.x by A5;
    end;
    hence f1 = f2 by FUNCT_2:def 8;
  end;
end;

theorem Th150:
  inverse_op GL(n,R) = matrix_inv(n,R)
proof
  A1: dom (inverse_op GL(n,R)) = the carrier of GL(n,R) by FUNCT_2:def 1
                              .= n-invertible_Matrices_over R by Th146
                              .= dom matrix_inv(n,R) by FUNCT_2:def 1;
  for x being object st x in dom matrix_inv(n,R)
  holds matrix_inv(n,R).x = (inverse_op GL(n,R)).x
  proof
    let x be object;
    assume A2: x in dom matrix_inv(n,R);
    then reconsider g = x as Element of GL(n,R) by A1;
    reconsider X = g as invertible Matrix of n,R by Th126;
    reconsider M = x as Element of n-invertible_Matrices_over R by A2;
    thus (inverse_op GL(n,R)).x = g " by GROUP_1:def 6
                               .= X~ by Th131
                               .= matrix_inv(n,R).M by Def12
                               .= matrix_inv(n,R).x;
  end;
  hence inverse_op GL(n,R) = matrix_inv(n,R) by A1,FUNCT_1:2;
end;

theorem Th151:
  for F being BinOp of n-invertible_Matrices_over R
  st F = matrix_mult(n,R) || (n-invertible_Matrices_over R)
  holds One(R,n) is_a_unity_wrt F
proof
  let F be BinOp of n-invertible_Matrices_over R;
  assume A1: F = matrix_mult(n,R) || (n-invertible_Matrices_over R);
  set mu = matrix_mult(n,R);
  reconsider e1 = One(R,n) as Element of n-invertible_Matrices_over R
  by Th145;
  for x being Element of n-invertible_Matrices_over R
  holds F.(e1, x) = x & F.(x, e1) = x
  proof
    let x be Element of n-invertible_Matrices_over R;
    reconsider X = x as invertible Matrix of n,R by Th145;
    set U = n-invertible_Matrices_over R;
    thus F.(e1, x) = mu.(One(R,n), x) by A1,FUNCT_1:49,ZFMISC_1:87
                  .= (1.(R,n)) * X by Def5
                  .= x by MATRIX_3:18;
    thus F.(x, e1) = mu.(x, (One(R,n))) by A1,FUNCT_1:49,ZFMISC_1:87
                  .= X * (1.(R,n)) by Def5
                  .= x by MATRIX_3:19;
  end;
  hence thesis by BINOP_1:3;
end;

Th152:
  for F being BinOp of n-invertible_Matrices_over R
  st F = matrix_mult(n,R) || (n-invertible_Matrices_over R)
  ex e1 being Element of n-invertible_Matrices_over R
  st e1 is_a_unity_wrt F
proof
  let F be BinOp of n-invertible_Matrices_over R;
  assume A1: F = matrix_mult(n,R) || (n-invertible_Matrices_over R);
  reconsider e1 = One(R,n) as Element of n-invertible_Matrices_over R
  by Th145;
  take e1;
  thus thesis by A1,Th151;
end;

theorem Th153:
  for F being BinOp of n-invertible_Matrices_over R
  st F = matrix_mult(n,R) || (n-invertible_Matrices_over R)
  holds One(R,n) = the_unity_wrt F
proof
  let F be BinOp of n-invertible_Matrices_over R;
  assume A1: F = matrix_mult(n,R) || (n-invertible_Matrices_over R);
  reconsider e1 = One(R,n) as Element of n-invertible_Matrices_over R
  by Th145;
  ex e being Element of n-invertible_Matrices_over R
  st e is_a_unity_wrt F by A1,Th152;
  then (the_unity_wrt F) is_a_unity_wrt F
  & e1 is_a_unity_wrt F by A1,Th151,BINOP_1:def 8;
  hence thesis by BINOP_1:10;
end;

theorem Th154:
  for F being BinOp of n-invertible_Matrices_over R
  st F = matrix_mult(n,R) || (n-invertible_Matrices_over R)
  holds matrix_inv(n,R) is_an_inverseOp_wrt F
proof
  let F be BinOp of n-invertible_Matrices_over R;
  assume A1: F = matrix_mult(n,R) || (n-invertible_Matrices_over R);
  set i = matrix_inv(n,R);
  set U = (n-invertible_Matrices_over R);
  set mu = matrix_mult(n,R);
  reconsider e1 = One(R,n) as Element of n-invertible_Matrices_over R
  by Th145;
  A2: e1 = the_unity_wrt F by A1,Th153;
  for x being Element of n-invertible_Matrices_over R
  holds F.(x, i.x) = the_unity_wrt F & F.(i.x, x) = the_unity_wrt F
  proof
    let x be Element of n-invertible_Matrices_over R;
    reconsider X = x, Y = i.x as invertible Matrix of n,R by Th145;
    reconsider a = x, b = i.x as Element of n-Matrices_over R by TARSKI:def 3;
    A3: [x,i.x] in [:U,U:] & [i.x,x] in [:U,U:];
    A4: i.x = X~ by Def12;
    X~ is_reverse_of X by MATRIX_6:def 4;
    then A5: (X~)*X = X*(X~) & (X~)*X = 1.(R,n) by MATRIX_6:def 2;
    thus F.(x, i.x) = mu.(a, b) by A1,A3,FUNCT_1:49
                   .= the_unity_wrt F by A2,A4,A5,Def5;
    thus F.(i.x, x) = mu.(b, a) by A1,A3,FUNCT_1:49
                   .= the_unity_wrt F by A2,A4,A5,Def5;
  end;
  hence matrix_inv(n,R) is_an_inverseOp_wrt F by FINSEQOP:def 1;
end;

Th155:
  for F being BinOp of n-invertible_Matrices_over R
  st F = matrix_mult(n,R) || (n-invertible_Matrices_over R)
  holds F is having_an_inverseOp
proof
  let F be BinOp of n-invertible_Matrices_over R;
  assume F = matrix_mult(n,R) || (n-invertible_Matrices_over R);
  then matrix_inv(n,R) is_an_inverseOp_wrt F by Th154;
  hence F is having_an_inverseOp by FINSEQOP:def 2;
end;

theorem Th156:
  for F being BinOp of n-invertible_Matrices_over R
  st F = matrix_mult(n,R) || (n-invertible_Matrices_over R)
  holds F is having_a_unity & F is associative &
  F is having_an_inverseOp
proof
  let F be BinOp of n-invertible_Matrices_over R;
  assume A1: F = matrix_mult(n,R) || (n-invertible_Matrices_over R);
  then ex e1 being Element of n-invertible_Matrices_over R
  st e1 is_a_unity_wrt F by Th152;
  hence F is having_a_unity by SETWISEO:def 2;
  for a,b,c being Element of n-invertible_Matrices_over R
  holds F.(a, F.(b, c)) = F.(F.(a,b), c)
  proof
    let a,b,c be Element of n-invertible_Matrices_over R;
    reconsider X = a, Y = b, Z = c as invertible Matrix of n,R by Th145;
    reconsider A = a, B = b, C = c as Element of n-Matrices_over R;
    set mu = matrix_mult(n, R), U = n-invertible_Matrices_over R;
    A2: [a, F.(b,c)] in [:U,U:] & [F.(a,b),c] in [:U,U:] & [a,b] in [:U,U:]
    & [b,c] in [:U,U:];
    A3: F.(a,b) = mu.(A,B) & mu.(A,B) = X * Y by A1,A2,Def5,FUNCT_1:49;
    A4: F.(b,c) = mu.(B,C) & mu.(B,C) = Y * Z by A1,A2,Def5,FUNCT_1:49;
    A5: len X = n & width X = n & len Y = n & width Y = n &
    len Z = n & width Z = n by MATRIX_0:24;
    thus F.(a, F.(b, c)) = mu.(A, mu.(B,C)) by A1,A2,A4,FUNCT_1:49
                        .= X * (Y * Z) by A4,Def5
                        .= (X * Y) * Z by A5,MATRIX_3:33
                        .= mu.(mu.(A,B),C) by A3,Def5
                        .= F.(F.(a,b), c) by A1,A2,A3,FUNCT_1:49;
  end;
  hence F is associative by BINOP_1:def 3;
  thus F is having_an_inverseOp by A1,Th155;
end;

theorem
  for F being BinOp of n-invertible_Matrices_over R
  st F = matrix_mult(n,R) || (n-invertible_Matrices_over R)
  holds matrix_inv(n,R) = the_inverseOp_wrt F
proof
  let F be BinOp of n-invertible_Matrices_over R;
  assume A1: F = matrix_mult(n,R) || (n-invertible_Matrices_over R);
  then A2: F is having_a_unity & F is associative &
  F is having_an_inverseOp by Th156;
  for x being Element of n-invertible_Matrices_over R
  holds (matrix_inv(n,R)).x = (the_inverseOp_wrt F).x
  proof
    let x be Element of n-invertible_Matrices_over R;
    reconsider X = x as invertible Matrix of n,R by Th145;
    reconsider Y = (the_inverseOp_wrt F).x as invertible Matrix of n,R
    by Th145;
    reconsider a = x as Element of n-Matrices_over R;
    (the_inverseOp_wrt F).x in n-invertible_Matrices_over R;
    then reconsider b = (the_inverseOp_wrt F).x
                    as Element of n-Matrices_over R;
    reconsider e1 = One(R,n) as Element of n-invertible_Matrices_over R
    by Th145;
    set U = n-invertible_Matrices_over R;
    set mu = matrix_mult(n,R);
    One(R,n) = the_unity_wrt F by A1,Th153; then
    1.(R,n) = F.(x, (the_inverseOp_wrt F).x) by A2,FINSEQOP:59
           .= mu.(a, b) by A1,FUNCT_1:49,ZFMISC_1:87
           .= X * Y by Def5;
    then X is_reverse_of Y by MATRIX_6:38;
    then Y = X~ by MATRIX_6:def 4;
    hence (matrix_inv(n,R)).x = (the_inverseOp_wrt F).x by Def12;
  end;

  hence matrix_inv(n,R) = the_inverseOp_wrt F by FUNCT_2:def 8;
end;

Lm4:
  for a,b being Element of R
  st a * b = 1.R
  holds (for b9 being Element of R
         st a * b9 = 1.R
         holds b9 = b)
  implies (for x being Element of R holds a * x <> 0.R or x = 0.R)
proof
  let a,b be Element of R;
  assume A1: a * b = 1.R;
  assume A2: for b9 being Element of R st a * b9 = 1.R holds b9 = b;
  let x be Element of R;
  assume A3: a * x = 0.R;
  a * (b + x) = a * b + a * x by VECTSP_1:def 7
             .= 1.R by A1,A3;
  then b + x = b by A2;
  then b - b = (b + (- b)) + x by RLVECT_1:def 3
            .= 0.R + x by RLVECT_1:5
            .= x;
  hence x = 0.R by RLVECT_1:5;
end;

Lm5:
  for a,b being Element of R
  st a * b = 1.R
  holds (for x being Element of R holds a * x <> 0.R or x = 0.R)
  implies a is invertible
proof
  let a,b be Element of R;
  assume A1: a * b = 1.R;
  assume A2: for x being Element of R holds a * x <> 0.R or x = 0.R;
  a is right_invertible & a is left_invertible
  proof
    thus a is right_invertible by A1,ALGSTR_0:def 28;
    set x = 1.R - b * a;
    a * x = (a * (1.R)) - a * (b * a) by VECTSP_1:11
         .= a - (a * b) * a by GROUP_1:def 3
         .= 0.R by A1,RLVECT_1:5;
    then x = 0.R by A2;
    then b * a = x + b * a
              .= 1.R + ((- (b * a)) + (b * a)) by RLVECT_1:def 3
              .= 1.R + 0.R by RLVECT_1:5
              .= 1.R;
    hence a is left_invertible by ALGSTR_0:def 27;
  end;
  hence a is invertible;
end;

Lm6:
  for a,b being Element of R
  st a * b = 1.R
  holds a is invertible
  implies (for b9 being Element of R
           st a * b9 = 1.R
           holds b9 = b)
proof
  let a,b be Element of R;
  assume A1: a * b = 1.R;
  assume A2: a is invertible;
  let b9 be Element of R;
  assume A3: a * b9 = 1.R;
  consider c being Element of R such that
  A4: c * a = 1.R by A2,ALGSTR_0:def 27;
  A5: b9 = (1.R) * b9
        .= c * (a * b9) by A4,GROUP_1:def 3
        .= c by A3;
  thus b = (1.R) * b
        .= c * (1.R) by A1,A4,GROUP_1:def 3
        .= b9 by A5;
end;

::$N Rudin's results~\cite{rudin1985unique} concerning two-sided inverses and unique right invertibility, as discussed by Almira and Cid~\cite{almira2023ring}.
theorem
  for a,b being Element of R
  st a * b = 1.R
  holds (for b9 being Element of R
         st a * b9 = 1.R
         holds b9 = b)
  iff (for x being Element of R holds a * x <> 0.R or x = 0.R)
proof
  let a,b be Element of R;
  assume A1: a * b = 1.R;
  thus (for b9 being Element of R
         st a * b9 = 1.R
         holds b9 = b)
  implies (for x being Element of R holds a * x <> 0.R or x = 0.R) by A1,Lm4;
  assume for x being Element of R holds a * x <> 0.R or x = 0.R;
  then a is invertible by A1,Lm5;
  hence thesis by A1,Lm6;
end;

theorem
  for a,b being Element of R
  st a * b = 1.R
  holds (for x being Element of R holds a * x <> 0.R or x = 0.R)
  iff a is invertible
proof
  let a,b be Element of R;
  assume A1: a * b = 1.R;
  hence (for x being Element of R holds a * x <> 0.R or x = 0.R)
  implies a is invertible by Lm5;
  assume a is invertible;
  then for b9 being Element of R
        st a * b9 = 1.R
        holds b9 = b by A1,Lm6;
  hence for x being Element of R holds a * x <> 0.R or x = 0.R by A1,Lm4;
end;

theorem
  for a,b being Element of R
  st a * b = 1.R
  holds (for b9 being Element of R
         st a * b9 = 1.R
         holds b9 = b)
  iff a is invertible
proof
  let a,b be Element of R;
  assume A1: a * b = 1.R;
  hereby
    assume (for b9 being Element of R
            st a * b9 = 1.R
            holds b9 = b);
    then (for x being Element of R holds a * x <> 0.R or x = 0.R) by A1,Lm4;
    hence a is invertible by A1,Lm5;
  end;
  assume a is invertible;
  hence thesis by A1,Lm6;
end;

:: Note:
:: (1) these conditions are equivalent to saying that R is Dedekind-finite.
:: (2) for R being commutative Ring
::     holds Matrix_ring(n,R) is Dedekind-finite.

begin :: Appendix 2: Linear groups

theorem Th161:
  for G being Group
  holds the multMagma of G is Subgroup of G
proof
  let G be Group;
  set UMG = the carrier of the multMagma of G;
  set UG = the carrier of G;
  (the multF of G) || UMG = the multF of the multMagma of G;
  hence the multMagma of G is Subgroup of G by GROUP_2:def 5;
end;

registration
  let G be Group;
  cluster the multMagma of G -> associative Group-like;
  coherence by Th161;
end;

theorem Th162:
  for G being Group
  holds inverse_op G = inverse_op (the multMagma of G)
proof
  let G be Group;
  set UMG = the carrier of the multMagma of G;
  set UG = the carrier of G;
  reconsider H = the multMagma of G as Subgroup of G by Th161;
  thus inverse_op (the multMagma of G) = (inverse_op H)
                                      .= (inverse_op G) | UMG by GROUP_2:49
                                      .= inverse_op G;
end;

definition
  let n be Nat, R be Ring;
  let IT be Group;
  attr IT is (n,R)-linear means :Def13:
  the multMagma of IT is Subgroup of GL(n,R);
end;

registration
  let n, R;
  cluster GL(n,R) -> (n,R)-linear;
  coherence by GROUP_2:54;
end;

registration
  let n, R;
  cluster strict (n,R)-linear for Group;
  existence
  proof
    take GL(n,R);
    thus thesis;
  end;
end;

 reserve G for (n,R)-linear Group;

theorem Th163:
  for H being Subgroup of GL(n,R)
  holds H is (n,R)-linear
proof
  let H be Subgroup of GL(n,R);
  the multMagma of H is Subgroup of H by Th161;
  hence H is (n,R)-linear by GROUP_2:56;
end;

registration
  let n,R;
  cluster -> (n,R)-linear for Subgroup of GL(n,R);
  coherence by Th163;
end;

theorem Th164:
  the carrier of G c= the carrier of GL(n,R)
proof
  the multMagma of G is Subgroup of GL(n,R) by Def13;
  hence thesis by GROUP_2:def 5;
end;

theorem
  the carrier of G c= n-invertible_Matrices_over R
proof
  the carrier of G c= the carrier of GL(n,R)
  & the carrier of GL(n,R) = n-invertible_Matrices_over R
  by Th146,Th164;
  hence thesis;
end;

registration
  let n,R;
  cluster (n,R)-linear -> (n,R)-matrix-membered for Group;
  coherence
  proof
    let G be Group;
    assume G is (n,R)-linear;
    then the carrier of G c= the carrier of GL(n,R) by Th164;
    then for x being object st x in the carrier of G holds x is Matrix of n,R
    by Def3;
    hence thesis by Def3;
  end;
end;

theorem Th166:
  1_G = 1_(GL(n,R))
proof
  A1: the multMagma of G is Subgroup of GL(n,R) by Def13;
  the carrier of the multMagma of G = the carrier of G
  & the multF of the multMagma of G = (the multF of G) || (the carrier
  of the multMagma of G);
  then the multMagma of G is Subgroup of G by GROUP_2:def 5;
  hence 1_G = 1_(the multMagma of G) by GROUP_2:44
           .= 1_(GL(n,R)) by A1,GROUP_2:44;
end;

theorem
  1_G = 1.(R,n)
proof
  thus 1_G = 1_(GL(n,R)) by Th166
          .= 1.(R,n) by Th130;
end;

registration
  let n,R,G;
  cluster the carrier of G -> non empty (n,R)-matrix-membered;
  coherence
  proof
    for x being object st x in the carrier of G
    holds x is Matrix of n,R
    proof
      let x be object;
      assume x in the carrier of G;
      then x in the carrier of GL(n,R) by Th164,TARSKI:def 3;
      hence x is Matrix of n,R by Def3;
    end;
    hence thesis;
  end;
end;

theorem Th168:
  the multF of G = (the multF of GL(n,R)) || (the carrier of G)
proof
  set UG = the carrier of G;
  the multMagma of G is Subgroup of GL(n,R) by Def13;
  hence the multF of G = (the multF of GL(n,R)) || UG by GROUP_2:def 5;
end;

theorem
  the multF of G = (matrix_mult (n, R)) || (the carrier of G)
proof
  set UG = the carrier of G;
  set UGL = the carrier of GL(n,R);
  UG c= UGL by Th164;
  then A1: [:UG,UG:] c= [: UGL, UGL :] by ZFMISC_1:96;
  the multMagma of G is Subgroup of GL(n,R) by Def13;
  hence the multF of G = (the multF of GL(n,R)) || UG by GROUP_2:def 5
                      .= matrix_mult(n,R) || UG by A1,RELAT_1:74;
end;

theorem
  the multF of GL(n,R) = (matrix_mult (n, R)) || (n-invertible_Matrices_over R)
  by Th146;

theorem Th171:
  for H being Subgroup of G
  holds H is (n,R)-linear
proof
  let H be Subgroup of G;
  A1: the carrier of H c= the carrier of GL(n,R)
  proof
    A2: the carrier of H c= the carrier of G by GROUP_2:def 5;
    the carrier of G c= the carrier of GL(n, R) by Th164;
    hence thesis by A2,XBOOLE_1:1;
  end;
  the multF of H = (the multF of GL(n,R)) || (the carrier of H)
  proof
    set UH = the carrier of H, UG = the carrier of G;
    UH c= UG by GROUP_2:def 5;
    then A3: [:UH,UH:] c= [:UG,UG:] by ZFMISC_1:96;
    thus the multF of H = (the multF of G) || UH by GROUP_2:def 5
                       .= ((the multF of GL(n,R)) || UG) || UH by Th168
                       .= (the multF of GL(n,R)) || UH by A3,FUNCT_1:51;
  end;
  hence H is (n,R)-linear by A1,GROUP_2:def 5;
end;

registration
  let n, R, G;
  cluster -> (n,R)-linear for Subgroup of G;
  coherence by Th171;
end;

theorem Th172:
  inverse_op G = (inverse_op GL(n,R)) | (the carrier of G)
proof
  set UG = the carrier of G, UMG = the carrier of the multMagma of G;
  A1: the multMagma of G is Subgroup of GL(n,R) by Def13;
  thus inverse_op G = inverse_op (the multMagma of G) by Th162
                   .= (inverse_op GL(n,R)) | UG by A1,GROUP_2:49;
end;

theorem
  inverse_op G = (matrix_inv(n,R)) | (the carrier of G)
proof
  thus inverse_op G = (inverse_op GL(n,R)) | (the carrier of G) by Th172
                   .= (matrix_inv(n,R)) | (the carrier of G) by Th150;
end;

begin :: Appendix 3: *General* linear groups

:: To *readably* distinguish the general (n,R)-linear Lie group from
:: the general (n,R)-linear algebraic group from the general
:: (n,R)-linear strict Group from ...

definition
  let n,R;
  let IT be (n,R)-linear Group;
  attr IT is general means :Def14:
  for x being object
  holds x in IT iff x is invertible Matrix of n,R;
end;

registration
  let n,R;
  cluster GL(n,R) -> general;
  coherence
  proof
    for x being object
    holds x in GL(n, R) iff x is Element of GL(n,R) by STRUCT_0:def 5;
    hence GL(n,R) is general by Th126;
  end;
end;

registration
  let n,R;
  cluster general strict for (n,R)-linear Group;
  existence
  proof
    take GL(n,R);
    thus thesis;
  end;
  cluster general for (n,R)-linear Group;
  existence
  proof
    take GL(n,R);
    thus thesis;
  end;
end;

theorem Th174:
  for G being general (n,R)-linear Group
  holds the carrier of G = the carrier of GL(n,R)
proof
  let G be general (n,R)-linear Group;
  for x being object
  holds x in the carrier of G iff x in the carrier of GL(n,R)
  proof
    let x be object;
    x is Element of GL(n,R) iff x in the carrier of GL(n,R);
    then x in the carrier of GL(n,R) iff x is invertible Matrix of n,R
    by Th126;
    then x in the carrier of GL(n,R) iff x in G by Def14;
    hence thesis by STRUCT_0:def 5;
  end;
  hence the carrier of G = the carrier of GL(n,R) by TARSKI:2;
end;

theorem Th175:
  for G being general (n,R)-linear Group
  holds the multF of G = the multF of GL(n,R)
proof
  let G be general (n,R)-linear Group;
  set UG = the carrier of G;
  A1: UG = the carrier of GL(n,R) by Th174;
  the multMagma of G is Subgroup of GL(n,R) by Def13;
  hence the multF of G = (the multF of GL(n,R)) || UG by GROUP_2:def 5
                      .= the multF of GL(n,R) by A1;
end;

theorem Th176:
  for G being general (n,R)-linear Group
  holds the multMagma of G = GL(n,R)
proof
  let G be general (n,R)-linear Group;
  the multF of G = the multF of GL(n,R) by Th175;
  hence thesis by Th174;
end;

theorem
  the general (n,R)-linear strict Group = GL(n,R) by Th176;

:: And, in the end, it turns out the real general linear group is the
:: friends we made alone the way...