:: Associated Matrix of Linear Map
::  by Robert Milewski
::
:: Received June 30, 1995
:: Copyright (c) 1995-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, NAT_1, XBOOLE_0, MATRIX_1, FINSEQ_3, RELAT_1, FINSEQ_1,
      TARSKI, ARYTM_3, XXREAL_0, CARD_1, TREES_1, FUNCT_1, INCSP_1, ORDINAL4,
      SUBSET_1, VECTSP_1, RLVECT_2, RLVECT_3, CARD_3, ARYTM_1, SUPINF_2,
      RLVECT_5, FINSET_1, STRUCT_0, RLSUB_1, ALGSTR_0, PARTFUN1, RLVECT_1,
      ZFMISC_1, QC_LANG1, FUNCT_2, VALUED_1, PRE_POLY, FINSEQ_2, RVSUM_1,
      FINSEQ_4, FVSUM_1, MATRLIN, MSSUBFAM, UNIALG_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XCMPLX_0, ORDINAL1,
      NAT_1, MOD_2, FINSEQ_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCT_3,
      STRUCT_0, ALGSTR_0, MATRIX_1, MATRIX_3, FVSUM_1, RLVECT_1, VECTSP_1,
      VECTSP_4, VECTSP_6, VECTSP_7, FINSET_1, FINSEQ_3, FINSEQ_2, FINSEQOP,
      BINOP_1, XXREAL_0, PRE_POLY, GRCAT_1;
 constructors PARTFUN1, BINOP_1, FUNCT_3, SQUARE_1, NAT_1, VECTSP_6, VECTSP_7,
      MOD_2, FVSUM_1, MATRIX_3, RELSET_1, PRE_POLY, GRCAT_1;
 registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, FUNCT_2, FINSET_1,
      XXREAL_0, XREAL_0, NAT_1, FINSEQ_1, STRUCT_0, VECTSP_1, MATRIX_1, CARD_1,
      VECTSP_7, MOD_2, GRCAT_1, PRE_POLY, RELAT_1, FUNCT_1, FINSEQ_4;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
 definitions TARSKI, FVSUM_1, FUNCOP_1, ALGSTR_0, PRE_POLY;
 theorems TARSKI, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_4, VECTSP_1, VECTSP_4,
      VECTSP_6, VECTSP_7, RLVECT_1, FUNCT_1, FUNCT_2, FUNCT_3, MATRIX_1,
      MATRIX_2, MATRIX_3, MOD_2, ZFMISC_1, NAT_1, FVSUM_1, SUBSET_1, FINSEQOP,
      FUNCOP_1, RELAT_1, PARTFUN2, XBOOLE_0, XBOOLE_1, RLVECT_2, ORDINAL1,
      PARTFUN1, PRE_POLY;
 schemes FINSEQ_1, FINSEQ_2, FUNCT_2, MATRIX_1, NAT_1, FINSEQ_4;

begin :: Preliminaries

reserve k,t,i,j,m,n for Nat,
  x,y,y1,y2 for set,
  D for non empty set;

definition
  let D be non empty set;
  let k;
  let M be Matrix of D;
  redefine func Del(M,k) -> Matrix of D;
  coherence
  proof
    ex n st for x st x in rng Del(M,k) ex p be FinSequence of D st x = p &
    len p = n
    proof
      consider n such that
A1:   for x st x in rng M ex p be FinSequence of D st x = p & len p =
      n by MATRIX_1:9;
      take n;
      let x such that
A2:   x in rng Del(M,k);
      Del(M,k) is FinSequence of D* by FINSEQ_3:105;
      then rng Del(M,k) c= D* by FINSEQ_1:def 4;
      then reconsider p = x as FinSequence of D by A2,FINSEQ_1:def 11;
      take p;
      rng Del(M,k) c= rng M by FINSEQ_3:106;
      then ex p1 be FinSequence of D st x = p1 & len p1 = n by A1,A2;
      hence thesis;
    end;
    hence thesis by MATRIX_1:9;
  end;
end;

theorem Th1:
  for M be FinSequence st len M = n+1 holds len Del(M,n+1) = n
proof
  let M be FinSequence;
  assume
A1: len M = n+1;
  then n+1 in Seg len M by FINSEQ_1:4;
  then n+1 in dom M by FINSEQ_1:def 3;
  hence thesis by A1,FINSEQ_3:109;
end;

theorem Th2:
  for M be Matrix of n+1,m,D for M1 be Matrix of D holds
  ( n > 0 implies width M = width Del(M,n+1) ) &
  ( M1 = <*M.(n+1)*> implies width M = width M1 )
proof
  let M be Matrix of n+1,m,D;
  let M1 be Matrix of D;
A1: len M = n + 1 by MATRIX_1:def 2;
  then n + 1 in Seg len M by FINSEQ_1:4;
  then n + 1 in dom M by FINSEQ_1:def 3;
  then
A2: M.(n+1) = Line(M,n+1) by MATRIX_2:16;
  now
    assume
A3: n > 0;
    len Del(M,n+1) = n by A1,Th1;
    then consider s be FinSequence such that
A4: s in rng Del(M,n+1) and
A5: len s = width Del(M,n+1) by A3,MATRIX_1:def 3;
    consider n1 be Nat such that
A6: for x st x in rng M ex p be FinSequence of D st x = p & len p = n1
    by MATRIX_1:9;
    consider s1 be FinSequence such that
A7: s1 in rng M and
A8: len s1 = width M by A1,MATRIX_1:def 3;
A9: ex p2 be FinSequence of D st s1 = p2 & len p2 = n1 by A7,A6;
    rng Del(M,n+1) c= rng M by FINSEQ_3:106;
    then ex p1 be FinSequence of D st s = p1 & len p1 = n1 by A4,A6;
    hence width M = width Del(M,n+1) by A5,A8,A9;
  end;
  hence n > 0 implies width M = width Del(M,n+1);
  assume M1 = <*M.(n+1)*>;
  then reconsider M2 = M1 as Matrix of 1,len(Line(M,n+1)),D by A2,MATRIX_1:11;
  thus width M = len(Line(M,n+1)) by MATRIX_1:def 7
    .= width M2 by MATRIX_1:23
    .= width M1;
end;

theorem Th3:
  for M be Matrix of n+1,m,D holds Del(M,n+1) is Matrix of n,m,D
proof
  let M be Matrix of n+1,m,D;
A1: len M = n + 1 by MATRIX_1:def 2;
  then
A2: len Del(M,n+1) = n by Th1;
  per cases;
  suppose
A3: n = 0;
    then Del(M,n+1) = {} by A2;
    hence thesis by A3,MATRIX_1:13;
  end;
  suppose
A4: n > 0;
    width M = m by A1,MATRIX_1:20;
    then width Del(M,n+1) = m by A4,Th2;
    hence thesis by A2,A4,MATRIX_1:20;
  end;
end;

theorem Th4:
  for M being FinSequence st M <> {} holds M = Del(M,len M) ^ <*M.(len M)*>
proof
  let M be FinSequence;
  assume M <> {};
  then consider q be FinSequence,x such that
A1: M = q ^ <*x*> by FINSEQ_1:46;
A2: len M = len q + len <*x*> by A1,FINSEQ_1:22
    .= len q + 1 by FINSEQ_1:39; then
A3: len Del(M,len M) = len q by Th1;
A4: dom q = Seg len q by FINSEQ_1:def 3;
A5: now
    let i be Nat;
    assume
A6: i in dom q;
    then i<=len q by A4,FINSEQ_1:1;
    then i in NAT & i<len M by A2,NAT_1:13,ORDINAL1:def 12;
    hence Del(M,len M).i = M.i by FINSEQ_3:110
      .= q.i by A1,A6,FINSEQ_1:def 7;
  end;
  M.(len M) = x by A1,A2,FINSEQ_1:42;
  hence thesis by A1,A3,A5,FINSEQ_2:9;
end;

definition
  let D;
  let P be FinSequence of D;
  redefine func <*P*> -> Matrix of 1,len P,D;
  coherence by MATRIX_1:11;
end;

begin :: More on Finite Sequences

begin :: Sequences and Matrices Concerning Linear Transformations

reserve K for Field,
  V for VectSp of K,
  a for Element of K,
  W for Element of V;
reserve KL1,KL2,KL3 for Linear_Combination of V,
  X for Subset of V;

theorem Th5:
  X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X &
  Sum KL1 = Sum KL2 implies KL1 = KL2
proof
  assume that
A1: X is linearly-independent and
A2: Carrier KL1 c= X & Carrier KL2 c= X and
A3: Sum KL1 = Sum KL2;
  Sum(KL1) - Sum(KL2) = 0.V by A3,VECTSP_1:19;
  then
A4: KL1 - KL2 is Linear_Combination of Carrier(KL1 - KL2) & Sum(KL1 - KL2) =
  0.V by VECTSP_6:7,47;
A5: Carrier(KL1 - KL2) c= Carrier(KL1) \/ Carrier(KL2) by VECTSP_6:41;
  Carrier(KL1) \/ Carrier(KL2) c= X by A2,XBOOLE_1:8;
  then
A6: Carrier(KL1 - KL2) is linearly-independent by A1,A5,VECTSP_7:1,XBOOLE_1:1;
  now
    let v be Vector of V;
    not v in Carrier(KL1 - KL2) by A6,A4,VECTSP_7:def 1;
    then (KL1 - KL2).v = 0.K by VECTSP_6:2;
    then KL1.v - KL2.v = 0.K by VECTSP_6:40;
    hence KL1.v = KL2.v by RLVECT_1:21;
  end;
  hence thesis by VECTSP_6:def 7;
end;

theorem Th6:
  X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X
  & Carrier KL3 c= X & Sum KL1 = Sum KL2 + Sum KL3 implies KL1 = KL2 + KL3
proof
  assume that
A1: X is linearly-independent & Carrier KL1 c= X and
A2: Carrier KL2 c= X & Carrier KL3 c= X and
A3: Sum KL1 = Sum(KL2) + Sum(KL3);
  Carrier(KL2 + KL3) c= Carrier(KL2) \/ Carrier(KL3) & Carrier(KL2) \/
  Carrier (KL3) c= X by A2,VECTSP_6:23,XBOOLE_1:8;
  then
A4: Carrier(KL2 + KL3) c= X by XBOOLE_1:1;
  Sum(KL1) = Sum(KL2 + KL3) by A3,VECTSP_6:44;
  hence thesis by A1,A4,Th5;
end;

theorem Th7:
  X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X
  & a <> 0.K & Sum KL1 = a * Sum KL2 implies KL1 = a * KL2
proof
  assume that
A1: X is linearly-independent & Carrier KL1 c= X and
A2: Carrier KL2 c= X & a <> 0.K & Sum(KL1) = a * Sum(KL2);
  Carrier(a * KL2) c= X & Sum(KL1) = Sum(a * KL2) by A2,VECTSP_6:29,45;
  hence thesis by A1,Th5;
end;

theorem Th8:
  for b2 be Basis of V ex KL be Linear_Combination of V st W = Sum
  KL & Carrier KL c= b2
proof
  let b2 be Basis of V;
  W in the VectSpStr of V by RLVECT_1:1;
  then W in Lin b2 by VECTSP_7:def 3;
  then consider KL1 being Linear_Combination of b2 such that
A1: W = Sum KL1 by VECTSP_7:7;
  take KL = KL1;
  thus W = Sum KL by A1;
  thus thesis by VECTSP_6:def 4;
end;

definition

  let K be Field;
  let V be VectSp of K;
  attr V is finite-dimensional means
  :Def1:
  ex A being finite Subset of V st A is Basis of V;
end;

registration
  let K be Field;
  cluster strict finite-dimensional for VectSp of K;
  existence
  proof
    set V = the VectSp of K;
    take (0).V;
    thus (0).V is strict;
    take A = {}(the carrier of (0).V);
    Lin A = (0).(0).V by VECTSP_7:9;
    then Lin A = the VectSpStr of (0).V by VECTSP_4:36;
    hence thesis by VECTSP_7:def 3;
  end;
end;

definition
  let K be Field;
  let V be finite-dimensional VectSp of K;
  mode OrdBasis of V -> FinSequence of V means
    :Def2:
    it is one-to-one & rng it is Basis of V;
  existence
  proof
    consider A being finite Subset of V such that
A1: A is Basis of V by Def1;
    consider p be FinSequence such that
A2: rng p = A and
A3: p is one-to-one by FINSEQ_4:58;
    reconsider p as FinSequence of V by A2,FINSEQ_1:def 4;
    take f = p;
    thus f is one-to-one by A3;
    thus thesis by A1,A2;
  end;
end;

reserve s for FinSequence,
  V1,V2,V3 for finite-dimensional VectSp of K,
  f,f1,f2 for Function of V1,V2,
  g for Function of V2,V3,
  b1 for OrdBasis of V1,
  b2 for OrdBasis of V2,
  b3 for OrdBasis of V3,
  v1,v2 for Vector of V2,
  v,w for Element of V1;
reserve p2,F for FinSequence of V1,
  p1,d for FinSequence of K,
  KL for Linear_Combination of V1;

definition
  let K be non empty doubleLoopStr;
  let V1,V2 be non empty VectSpStr over K;
  let f1,f2 be Function of V1, V2;
  func f1+f2 -> Function of V1,V2 means
  :Def3:
  for v be Element of V1 holds it .v = f1.v + f2.v;
  existence
  proof
    deffunc F(Element of V1) = f1.$1 + f2.$1;
    consider F be Function of V1, V2 such that
A1: for v be Element of V1 holds F.v = F(v) from FUNCT_2:sch 4;
    reconsider F as Function of V1,V2;
    take F;
    thus thesis by A1;
  end;
  uniqueness
  proof
    let F,G be Function of V1,V2 such that
A2: for v be Element of V1 holds F.v = f1.v + f2.v and
A3: for v be Element of V1 holds G.v = f1.v + f2.v;
    now
      let v be Element of V1;
      thus F.v = f1.v + f2.v by A2
        .= G.v by A3;
    end;
    hence F = G by FUNCT_2:63;
  end;
end;

definition
  let K be non empty doubleLoopStr;
  let V1,V2 be non empty VectSpStr over K;
  let f be Function of V1,V2;
  let a be Element of K;
  func a*f -> Function of V1,V2 means
  :Def4:
  for v be Element of V1 holds it.v = a * (f.v);
  existence
  proof
    deffunc F(Element of V1) = a * (f.$1);
    consider F be Function of V1, V2 such that
A1: for v be Element of V1 holds F.v = F(v) from FUNCT_2:sch 4;
    reconsider F as Function of V1,V2;
    take F;
    thus thesis by A1;
  end;
  uniqueness
  proof
    let F,G be Function of V1,V2 such that
A2: for v be Element of V1 holds F.v = a * (f.v) and
A3: for v be Element of V1 holds G.v = a * (f.v);
    now
      let v be Element of V1;
      thus F.v = a * (f.v) by A2
        .= G.v by A3;
    end;
    hence F = G by FUNCT_2:63;
  end;
end;

theorem Th9:
  for a being Element of V1 for F being FinSequence of V1 for G
  being FinSequence of K st len F = len G & for k for v being Element of K st k
  in dom F & v = G.k holds F.k = v * a holds Sum(F) = Sum(G) * a
proof
  let a be Element of V1;
  let F be FinSequence of V1;
  let G be FinSequence of K;
  defpred P[Nat] means for H being FinSequence of V1, I being FinSequence of K
st len H = len I & len H = $1 & (for k for v be Element of K st k in dom H & v
  = I.k holds H.k = v * a ) holds Sum(H) = Sum(I) * a;
A1: for n st P[n] holds P[n+1]
  proof
    let n;
    assume
A2: for H being FinSequence of V1, I being FinSequence of K st len H =
    len I & len H = n & (for k for v being Element of K st k in dom H & v = I.k
    holds H.k = v * a) holds Sum(H) = Sum(I) * a;
    let H be FinSequence of V1, I be FinSequence of K;
    assume that
A3: len H = len I and
A4: len H = n + 1 and
A5: for k for v being Element of K st k in dom H & v = I.k holds H.k = v * a;
    reconsider q = I | (Seg n) as FinSequence of K by FINSEQ_1:18;
    reconsider p = H | (Seg n) as FinSequence of V1 by FINSEQ_1:18;
A6: n <= n + 1 by NAT_1:12;
    then
A7: len p = n by A4,FINSEQ_1:17;
A8: dom p = Seg n by A4,A6,FINSEQ_1:17;
A9: len q = n by A3,A4,A6,FINSEQ_1:17;
A10: dom q = Seg n by A3,A4,A6,FINSEQ_1:17;
A11: now
      len p <= len H by A4,A6,FINSEQ_1:17;
      then
A12:  dom p c= dom H by FINSEQ_3:30;
      let k;
      let v be Element of K;
      assume that
A13:  k in dom p and
A14:  v = q.k;
      I.k = q.k by A8,A10,A13,FUNCT_1:47;
      then H.k = v * a by A5,A13,A14,A12;
      hence p.k = v * a by A13,FUNCT_1:47;
    end;
    reconsider n as Element of NAT by ORDINAL1:def 12;
    n + 1 in Seg(n + 1) by FINSEQ_1:4;
    then
A15: n + 1 in dom H by A4,FINSEQ_1:def 3;
    then reconsider v1 = H.(n + 1) as Element of V1 by FINSEQ_2:11;
    dom H = dom I by A3,FINSEQ_3:29;
    then reconsider v2 = I.(n + 1) as Element of K by A15,FINSEQ_2:11;
A16: v1 = v2 * a by A5,A15;
    thus Sum(H) = Sum(p) + v1 by A4,A7,A8,RLVECT_1:38
      .= Sum(q) * a + v2 * a by A2,A7,A9,A11,A16
      .= (Sum(q) + v2) * a by VECTSP_1:def 15
      .= Sum(I) * a by A3,A4,A9,A10,RLVECT_1:38;
  end;
A17: P[0]
  proof
    let H be FinSequence of V1, I be FinSequence of K;
    assume that
A18: len H = len I and
A19: len H = 0 and
    for k for v being Element of K st k in dom H & v = I.k holds H.k = v * a;
    H = <*>(the carrier of V1) by A19;
    then
A20: Sum(H) = 0.V1 by RLVECT_1:43;
    I = <*>(the carrier of K) by A18,A19;
    then Sum(I) = 0.K by RLVECT_1:43;
    hence thesis by A20,VECTSP_1:14;
  end;
  for n holds P[n] from NAT_1:sch 2(A17,A1);
  hence thesis;
end;

theorem Th10:
  for a be Element of V1 for F being FinSequence of K for G being
FinSequence of V1 st len F = len G & for k st k in dom F holds G.k = (F/.k) * a
  holds Sum(G) = Sum(F) * a
proof
  let a be Element of V1;
  let F be FinSequence of K;
  let G be FinSequence of V1;
  assume that
A1: len F = len G and
A2: for k st k in dom F holds G.k = (F/.k) * a;
  now
    let k;
    let v be Element of K;
    assume that
A3: k in dom G and
A4: v = F.k;
A5: k in dom F by A1,A3,FINSEQ_3:29;
    then v = F/.k by A4,PARTFUN1:def 6;
    hence G.k = v * a by A2,A5;
  end;
  hence thesis by A1,Th9;
end;

theorem Th11:
  for V1 being add-associative right_zeroed right_complementable
  non empty addLoopStr
  for F being FinSequence of V1 st for k st k in dom F holds
  F/.k = 0.V1 holds Sum(F) = 0.V1
proof
  let V1 be add-associative right_zeroed right_complementable non empty
  addLoopStr;
  let F be FinSequence of V1;
  assume
A1: for k st k in dom F holds F/.k = 0.V1;
  defpred P[FinSequence of V1] means (( for k st k in dom $1 holds $1/.k = 0.
  V1) implies Sum($1) = 0.V1 );
A2: for p being FinSequence of V1, x being Element of V1 holds P[p] implies
  P[p^<*x*>]
  proof
    let p be FinSequence of V1;
    let x be Element of V1;
    assume
A3: (for k st k in dom p holds p/.k = 0.V1) implies Sum(p) = 0.V1;
A4: len p + 1 in Seg (len p + 1) by FINSEQ_1:4;
    assume
A5: for k st k in dom(p^<*x*>) holds (p^<*x*>)/.k = 0.V1;
A6: for k st k in dom p holds p/.k = 0.V1
    proof
A7:   dom p c= dom(p^<*x*>) by FINSEQ_1:26;
      let k such that
A8:   k in dom p;
      reconsider k1=k as Element of NAT by ORDINAL1:def 12;
      thus p/.k = p.k by A8,PARTFUN1:def 6
        .= (p^<*x*>).k1 by A8,FINSEQ_1:def 7
        .= (p^<*x*>)/.k by A8,A7,PARTFUN1:def 6
        .= 0.V1 by A5,A8,A7;
    end;
    len(p^<*x*>) = len p + len<*x*> by FINSEQ_1:22
      .= len p + 1 by FINSEQ_1:39;
    then
A9: len p + 1 in dom(p^<*x*>) by A4,FINSEQ_1:def 3;
A10: x = (p^<*x*>).(len p + 1) by FINSEQ_1:42;
    thus Sum(p^<*x*>) = Sum(p) + Sum(<*x*>) by RLVECT_1:41
      .= Sum(p) + x by RLVECT_1:44
      .= Sum(p) + (p^<*x*>)/.(len p + 1) by A9,A10,PARTFUN1:def 6
      .= 0.V1 + 0.V1 by A3,A5,A6,A9
      .= 0.V1 by RLVECT_1:def 4;
  end;
A11: P[<*>the carrier of V1] by RLVECT_1:43;
  for p being FinSequence of V1 holds P[p] from FINSEQ_2:sch 2(A11,A2 );
  hence thesis by A1;
end;

definition
  let K, V1, p1,p2;
  func lmlt(p1,p2) -> FinSequence of V1 equals
  (the lmult of V1).:(p1,p2);
  coherence;
end;

theorem Th12:
  dom p1 = dom p2 implies dom lmlt(p1,p2) = dom p1
proof
  assume
A1: dom p1 = dom p2;
  rng p1 c= the carrier of K & rng p2 c= the carrier of V1 by FINSEQ_1:def 4;
  then
A2: [:rng p1,rng p2:] c= [:the carrier of K,the carrier of V1:] by ZFMISC_1:96
;
  rng <:p1,p2:> c= [:rng p1,rng p2:] & [:the carrier of K,the carrier of
  V1:] = dom (the lmult of V1) by FUNCT_2:def 1,FUNCT_3:51;
  hence dom lmlt(p1,p2) = dom <:p1,p2:> by A2,RELAT_1:27,XBOOLE_1:1
    .= dom p1 /\ dom p2 by FUNCT_3:def 7
    .= dom p1 by A1;
end;

definition
  let V1 be non empty addLoopStr, M be FinSequence of (the carrier of V1)*;
  func Sum M -> FinSequence of V1 means
  :Def6:
  len it = len M & for k st k in dom it
   holds it/.k = Sum (M/.k);
  existence
  proof
    deffunc F(Nat) = Sum (M/.$1);
    consider F being FinSequence of V1 such that
A1: len F = len M & for k be Nat st k in dom F holds F.k = F(k) from
    FINSEQ_2:sch 1;
    take F;
    thus len F = len M by A1;
    hereby
      let k;
      assume
A2:   k in dom F;
      hence F/.k = F.k by PARTFUN1:def 6
        .= Sum (M/.k) by A1,A2;
    end;
  end;
  uniqueness
  proof
    let F1,F2 be FinSequence of V1 such that
A3: len F1 = len M and
A4: for k st k in dom F1 holds F1/.k = Sum (M/.k) and
A5: len F2 = len M and
A6: for k st k in dom F2 holds F2/.k = Sum (M/.k);
A7: dom F1 = Seg len F1 by FINSEQ_1:def 3;
    now
      let k be Nat;
      assume
A8:   k in dom F1;
      then
A9:   k in dom F2 by A3,A5,A7,FINSEQ_1:def 3;
      thus F1.k = F1/.k by A8,PARTFUN1:def 6
        .= Sum (M/.k) by A4,A8
        .= F2/.k by A6,A9
        .= F2.k by A9,PARTFUN1:def 6;
    end;
    hence thesis by A3,A5,FINSEQ_2:9;
  end;
end;

theorem Th13:
  for M be Matrix of the carrier of V1 st len M = 0 holds Sum Sum M = 0.V1
proof
  let M be Matrix of the carrier of V1;
  assume len M = 0;
  then len Sum M = 0 by Def6;
  then Sum M = <*>(the carrier of V1);
  hence thesis by RLVECT_1:43;
end;

theorem Th14:
  for M be Matrix of m+1,0,the carrier of V1 holds Sum Sum M = 0.V1
proof
  let M be Matrix of m+1,0,the carrier of V1;
  for k st k in dom Sum M holds (Sum M)/.k = 0.V1
  proof
    let k such that
A1: k in dom Sum M;
    reconsider k1=k as Element of NAT by ORDINAL1:def 12;
    len M = len Sum M by Def6;
    then dom M = dom Sum M by FINSEQ_3:29;
    then M/.k1 in rng M by A1,PARTFUN2:2;
    then len(M/.k) = 0 by MATRIX_1:def 2;
    then
A2: M/.k = <*>(the carrier of V1);
    thus (Sum M)/.k = Sum (M/.k) by A1,Def6
      .= 0.V1 by A2,RLVECT_1:43;
  end;
  hence thesis by Th11;
end;

theorem Th15:
  for x be Element of D holds <*<*x*>*> = <*<*x*>*>@
proof
  let x be Element of D;
  set P = <*<*x*>*>, R = (<*<*x*>*>@);
A1: len P = 1 by FINSEQ_1:40;
  then
A2: width P = len <*x*> by MATRIX_1:20
    .= 1 by FINSEQ_1:40;
  then
A3: len R = 1 by MATRIX_2:10;
A4: now
    let i,j;
    assume
A5: [i,j] in Indices P;
    then
A6: [i,j] in [:dom P,Seg 1:] by A2,MATRIX_1:def 4;
    then i in dom P by ZFMISC_1:87;
    then i in Seg 1 by A1,FINSEQ_1:def 3;
    then
A7: i = 1 by FINSEQ_1:2,TARSKI:def 1;
    j in Seg 1 by A6,ZFMISC_1:87;
    then j = 1 by FINSEQ_1:2,TARSKI:def 1;
    hence P*(i,j) = R*(i,j) by A5,A7,MATRIX_1:def 6;
  end;
  width R = 1 by A1,A2,MATRIX_2:10;
  hence thesis by A1,A2,A3,A4,MATRIX_1:21;
end;

theorem Th16:
  for V1,V2 being VectSp of K, f being Function of V1,V2, p being
  FinSequence of V1 st f is additive homogeneous holds f.Sum p = Sum(f*p)
proof
  let V1,V2 be VectSp of K, f be Function of V1,V2;
  let p be FinSequence of V1;
  defpred P[FinSequence of V1] means f.Sum($1) = Sum(f*$1);
  assume
A1: f is additive homogeneous;
A2: for p being FinSequence of V1 for w being Element of V1 st P[p] holds P[
  p^<*w*>]
  proof
    let p be FinSequence of V1;
    let w be Element of V1 such that
A3: f.Sum p = Sum (f*p);
    thus f.Sum(p^<*w*>) = f.(Sum(p) + Sum<*w*>) by RLVECT_1:41
      .= Sum(f*p) + f.Sum<*w*> by A1,A3,VECTSP_1:def 20
      .= Sum(f*p) + f.w by RLVECT_1:44
      .= Sum(f*p) + Sum<*f.w*> by RLVECT_1:44
      .= Sum(f*p^<*f.w*>) by RLVECT_1:41
      .= Sum(f*(p^<*w*>)) by FINSEQOP:8;
  end;
  f.Sum(<*>(the carrier of V1)) = f.(0.V1) by RLVECT_1:43
    .= f.(0.K*0.V1) by VECTSP_1:14
    .= 0.K*f.(0.V1) by A1,MOD_2:def 2
    .= 0.V2 by VECTSP_1:14
    .= Sum(<*>(the carrier of V2)) by RLVECT_1:43
    .= Sum(f*<*>(the carrier of V1));
  then
A4: P[<*>(the carrier of V1)];
  for p being FinSequence of V1 holds P[p] from FINSEQ_2:sch 2(A4,A2 );
  hence thesis;
end;

theorem Th17:
  for a be FinSequence of K, p being FinSequence of V1 st len p =
  len a holds f is additive homogeneous implies f*lmlt(a,p) = lmlt(a,f*p)
proof
  let a be FinSequence of K, p be FinSequence of V1;
  assume len p = len a;
  then
A1: dom p = dom a by FINSEQ_3:29;
  dom f = the carrier of V1 by FUNCT_2:def 1;
  then rng p c= dom f by FINSEQ_1:def 4;
  then
A2: dom p = dom (f*p) by RELAT_1:27;
  assume
A3: f is additive homogeneous;
A4: now
    set P = f*p;
    let k be Nat;
    assume
A5: k in dom (f*lmlt(a,p));
A6: dom (f*lmlt(a,p)) c= dom lmlt(a,p) by RELAT_1:25;
    then k in dom lmlt(a,p) by A5;
    then
A7: k in dom p by A1,Th12;
    then
A8: p/.k = p.k by PARTFUN1:def 6;
A9: k in dom lmlt(a,f*p) by A1,A2,A7,Th12;
A10: a/.k = a.k by A1,A7,PARTFUN1:def 6;
A11: P/.k = (f*p).k by A2,A7,PARTFUN1:def 6;
    thus (f*lmlt(a,p)).k = f.(lmlt(a,p).k) by A5,FUNCT_1:12
      .= f.((the lmult of V1).(a.k,p.k)) by A5,A6,FUNCOP_1:22
      .= f.((a/.k)*(p/.k)) by A10,A8,VECTSP_1:def 12
      .= (a/.k)*(f.(p/.k)) by A3,MOD_2:def 2
      .= (a/.k)*(P/.k) by A7,A8,A11,FUNCT_1:13
      .= (the lmult of V2).(a.k,(f*p).k) by A10,A11,VECTSP_1:def 12
      .= lmlt(a,f*p).k by A9,FUNCOP_1:22;
  end;
  dom lmlt(a,p) = dom p by A1,Th12
    .= dom lmlt(a,f*p) by A1,A2,Th12;
  then len lmlt(a,p) = len lmlt(a,f*p) by FINSEQ_3:29;
  then len (f*lmlt(a,p)) = len lmlt(a,f*p) by FINSEQ_2:33;
  hence thesis by A4,FINSEQ_2:9;
end;

theorem Th18:
  for a be FinSequence of K st len a = len b2 & g is additive homogeneous holds
  g.Sum(lmlt(a,b2)) = Sum(lmlt(a,g*b2))
proof
  let a be FinSequence of K such that
A1: len a = len b2 and
A2: g is additive homogeneous;
  thus g.Sum(lmlt(a,b2)) = Sum(g*lmlt(a,b2)) by A2,Th16
    .= Sum(lmlt(a,g*b2)) by A1,A2,Th17;
end;

theorem Th19:
  for F, F1 being FinSequence of V1, KL being Linear_Combination
of V1, p being Permutation of dom F st F1 = F * p holds KL (#) F1 = (KL (#) F)
  * p
proof
  let F, F1 be FinSequence of V1;
  let KL be Linear_Combination of V1;
  let p be Permutation of dom F such that
A1: F1 = F * p;
  dom F = Seg len F by FINSEQ_1:def 3;
  then dom F = Seg len (KL (#) F) by VECTSP_6:def 5;
  then
A2: dom F = dom (KL (#) F) by FINSEQ_1:def 3;
  then reconsider F2 = (KL (#) F) * p as FinSequence of V1 by FINSEQ_2:47;
  len (KL (#) F1) = len F1 by VECTSP_6:def 5
    .= len F by A1,FINSEQ_2:44
    .= len (KL (#) F) by VECTSP_6:def 5
    .= len F2 by A2,FINSEQ_2:44;
  then
A3: dom (KL (#) F1) = dom ((KL (#) F) * p) by FINSEQ_3:29;
  len (KL (#) F1) = len F1 by VECTSP_6:def 5;
  then
A4: dom (KL (#) F1) = dom F1 by FINSEQ_3:29;
  now
    let k be Nat;
    reconsider k0=k as Element of NAT by ORDINAL1:def 12;
    assume
A5: k in dom (KL (#) F1);
    then k in dom p by A3,FUNCT_1:11;
    then p.k in rng p by FUNCT_1:def 3;
    then
A6: p.k in dom F by FUNCT_2:def 3;
    then reconsider k1 = p.k0 as Element of NAT by FINSEQ_3:23;
    F1/.k = F1.k by A4,A5,PARTFUN1:def 6
      .= F.(p.k) by A1,A4,A5,FUNCT_1:12
      .= F/.(p.k) by A6,PARTFUN1:def 6;
    hence (KL (#) F1).k = KL.(F/.k1) * (F/.k1) by A5,VECTSP_6:def 5
      .= (KL (#) F).k1 by A2,A6,VECTSP_6:def 5
      .= F2.k by A3,A5,FUNCT_1:12;
  end;
  hence thesis by A3,FINSEQ_1:13;
end;

theorem Th20:
  F is one-to-one & Carrier KL c= rng F implies Sum(KL (#) F) = Sum KL
proof
  assume
A1: F is one-to-one;
  assume
A2: Carrier KL c= rng F;
  then reconsider A = Carrier KL as Subset of rng F;
  consider p1 being Permutation of dom F such that
A3: (F-A`)^(F-A) = F * p1 by FINSEQ_3:115;
  reconsider G1 = F - A`, G2 = F - A as FinSequence of V1 by FINSEQ_3:86;
A4: G1 is one-to-one by A1,FINSEQ_3:87;
  len (KL (#) F) = len F by VECTSP_6:def 5;
  then dom (KL (#) F) = dom F by FINSEQ_3:29;
  then reconsider p1 as Permutation of dom (KL (#) F);
A5: rng G1 = rng F \ A` by FINSEQ_3:65
    .= rng F \ ((rng F) \ Carrier KL) by SUBSET_1:def 4
    .= rng F /\ Carrier KL by XBOOLE_1:48
    .= Carrier KL by A2,XBOOLE_1:28;
  for k st k in dom (KL (#) G2) holds (KL (#) G2)/.k = 0.V1
  proof
    let k such that
A6: k in dom (KL (#) G2);
    len (KL (#) G2) = len G2 by VECTSP_6:def 5;
    then
A7: dom (KL (#) G2) = dom G2 by FINSEQ_3:29;
    then G2.k in rng G2 by A6,FUNCT_1:def 3;
    then G2.k in rng F \ Carrier KL by FINSEQ_3:65;
    then not G2.k in Carrier KL by XBOOLE_0:def 5;
    then
A8: not G2/.k in Carrier KL by A6,A7,PARTFUN1:def 6;
    reconsider k1=k as Element of NAT by ORDINAL1:def 12;
    thus (KL (#) G2)/.k = (KL (#) G2).k by A6,PARTFUN1:def 6
      .= KL.(G2/.k1) * (G2/.k1) by A6,VECTSP_6:def 5
      .= 0.K * (G2/.k) by A8,VECTSP_6:2
      .= 0.V1 by VECTSP_1:14;
  end;
  then
A9: Sum(KL (#) G2) = 0.V1 by Th11;
  KL (#) (G1^G2) = (KL (#) F) * p1 by A3,Th19;
  hence Sum(KL (#) F) = Sum(KL (#) (G1 ^ G2)) by RLVECT_2:7
    .= Sum((KL (#) G1) ^ (KL (#) G2)) by VECTSP_6:13
    .= Sum(KL (#) G1) + Sum(KL (#) G2) by RLVECT_1:41
    .= Sum(KL) + 0.V1 by A4,A5,A9,VECTSP_6:def 6
    .= Sum KL by RLVECT_1:4;
end;

theorem Th21:
  for A be set for p be FinSequence of V1 st rng p c= A holds f1
is additive homogeneous & f2 is additive homogeneous &
 (for v st v in A holds f1.v = f2.v) implies f1.Sum p
  = f2.Sum p
proof
  let A be set;
  let p be FinSequence of V1 such that
A1: rng p c= A;
  defpred P[FinSequence of V1] means rng $1 c= A implies f1.Sum($1) = f2.Sum(
  $1);
  assume
A2: f1 is additive homogeneous;
  assume
A3: f2 is additive homogeneous;
  assume
A4: for v st v in A holds f1.v = f2.v;
A5: for p being FinSequence of V1, x being Element of V1 st P[p]holds P[p^<*
  x*>]
  proof
    let p be FinSequence of V1, x be Element of V1 such that
A6: rng p c= A implies f1.Sum p = f2.Sum p;
A7: rng p c= rng p \/ rng <*x*> by XBOOLE_1:7;
    assume rng (p^<*x*>) c= A;
    then
A8: rng p \/ rng <*x*> c= A by FINSEQ_1:31;
    rng <*x*> c= rng p \/ rng <*x*> by XBOOLE_1:7;
    then rng <*x*> c= A by A8,XBOOLE_1:1;
    then {x} c= A by FINSEQ_1:39;
    then
A9: x in A by ZFMISC_1:31;
    thus f1.Sum(p^<*x*>) = f1.(Sum(p) + Sum(<*x*>)) by RLVECT_1:41
      .= f2.(Sum p) + f1.(Sum(<*x*>)) by A2,A6,A8,A7,VECTSP_1:def 20,XBOOLE_1:1
      .= f2.(Sum p) + f1.x by RLVECT_1:44
      .= f2.(Sum p) + f2.x by A4,A9
      .= f2.(Sum p) + f2.(Sum(<*x*>)) by RLVECT_1:44
      .= f2.(Sum(p) + Sum(<*x*>)) by A3,VECTSP_1:def 20
      .= f2.Sum(p^<*x*>) by RLVECT_1:41;
  end;
A10: P[<*>(the carrier of V1)]
  proof
    assume rng<*>(the carrier of V1) c= A;
    thus f1.Sum(<*>(the carrier of V1)) = f1.(0.V1) by RLVECT_1:43
      .= f1.(0.K*0.V1) by VECTSP_1:14
      .= 0.K*f1.(0.V1) by A2,MOD_2:def 2
      .= 0.V2 by VECTSP_1:14
      .= 0.K*f2.(0.V1) by VECTSP_1:14
      .= f2.(0.K*0.V1) by A3,MOD_2:def 2
      .= f2.(0.V1) by VECTSP_1:14
      .= f2.Sum(<*>(the carrier of V1)) by RLVECT_1:43;
  end;
  for p being FinSequence of V1 holds P[p] from FINSEQ_2:sch 2(A10,A5 );
  hence thesis by A1;
end;

theorem Th22:
  f1 is additive homogeneous & f2 is additive homogeneous implies
   for b1 being OrdBasis of V1
  st len b1 > 0 holds f1*b1 = f2*b1 implies f1 = f2
proof
  assume that
A1: f1 is additive homogeneous and
A2: f2 is additive homogeneous;
  let b1 be OrdBasis of V1 such that
A3: len b1 > 0;
  reconsider b = rng b1 as Basis of V1 by Def2;
  assume
A4: f1*b1 = f2*b1;
  now
    len b1 in Seg len b1 by A3,FINSEQ_1:3;
    then reconsider D = dom b1 as non empty set by FINSEQ_1:def 3;
    let v be Element of V1;
    Lin(b) = the VectSpStr of V1 by VECTSP_7:def 3;
    then v in Lin(b) by RLVECT_1:1;
    then consider KL be Linear_Combination of b such that
A5: v = Sum(KL) by VECTSP_7:7;
    set p = KL (#) b1;
    set A = { KL.(b1/.i)*(b1/.i) where i is Element of D : not contradiction };
A6: rng p c= A
    proof
      let x;
      assume x in rng p;
      then consider i be Nat such that
A7:   i in dom p and
A8:   p.i = x by FINSEQ_2:10;
      dom p = Seg len p by FINSEQ_1:def 3;
      then i in Seg len b1 by A7,VECTSP_6:def 5;
      then
A9:   i in dom b1 by FINSEQ_1:def 3;
      (KL (#) b1).i = KL.(b1/.i) * (b1/.i) by A7,VECTSP_6:def 5;
      hence thesis by A8,A9;
    end;
A10: for w st w in A holds f1.w = f2.w
    proof
      let w;
      assume w in A;
      then consider i be Element of D such that
A11:  w = KL.(b1/.i)*(b1/.i);
      f1.(b1/.i) = f1.(b1.i) by PARTFUN1:def 6
        .= (f2*b1).i by A4,FUNCT_1:13
        .= f2.(b1.i) by FUNCT_1:13
        .= f2.(b1/.i) by PARTFUN1:def 6;
      then f1.(KL.(b1/.i)*(b1/.i)) = KL.(b1/.i)*(f2.(b1/.i)) by A1,MOD_2:def 2
        .= f2.(KL.(b1/.i)*(b1/.i)) by A2,MOD_2:def 2;
      hence thesis by A11;
    end;
A12: b1 is one-to-one & Carrier KL c= rng b1 by Def2,VECTSP_6:def 4;
    hence f1.v = f1.Sum(KL (#) b1) by A5,Th20
      .= f2.Sum p by A1,A2,A6,A10,Th21
      .= f2.v by A5,A12,Th20;
  end;
  hence thesis by FUNCT_2:63;
end;

registration
  let D be non empty set;
  cluster -> FinSequence-yielding for Matrix of D;
  coherence;
end;

definition
  let D be non empty set;
  let F,G be Matrix of D;
  redefine func F^^G -> Matrix of D;
  coherence
  proof
    reconsider M = F^^G as FinSequence;
    ex n st for x st x in rng M ex p be FinSequence of D st x = p & len p = n
    proof
      take n = width F + width G;
      let x;
A1:   rng F c= D* & rng G c= D* by FINSEQ_1:def 4;
      assume x in rng M;
      then consider y such that
A2:   y in dom M and
A3:   x = M.y by FUNCT_1:def 3;
A4:   dom M = dom F /\ dom G by PRE_POLY:def 4;
      then
A5:   y in dom G by A2,XBOOLE_0:def 4;
      then
A6:   G.y in rng G by FUNCT_1:def 3;
A7:   y in dom F by A2,A4,XBOOLE_0:def 4;
      then F.y in rng F by FUNCT_1:def 3;
      then reconsider f = F.y, g = G.y as FinSequence of D by A6,A1,
FINSEQ_1:def 11;
      reconsider y as Nat by A2,FINSEQ_3:23;
A8:   G.y = Line(G,y) by A5,MATRIX_2:16;
A9:   x = f ^ g by A2,A3,PRE_POLY:def 4;
      then reconsider p = x as FinSequence of D;
      take p;
      thus x = p;
      F.y = Line(F,y) by A7,MATRIX_2:16;
      hence len p = len Line(F,y) + len Line(G,y) by A9,A8,FINSEQ_1:22
        .= width F + len Line(G,y) by MATRIX_1:def 7
        .= n by MATRIX_1:def 7;
    end;
    hence thesis by MATRIX_1:9;
  end;
end;

definition
  let D be non empty set;
  let n,m,k;
  let M1 be Matrix of n,k,D, M2 be Matrix of m,k,D;
  redefine func M1^M2 -> Matrix of n+m,k,D;
  coherence
  proof
    per cases;
    suppose
A1:   n = 0;
      then len M1 = 0 by MATRIX_1:def 2;
      then M1 = {};
      hence thesis by A1,FINSEQ_1:34;
    end;
    suppose
A2:   m = 0;
      then len M2 = 0 by MATRIX_1:def 2;
      then M2 = {};
      hence thesis by A2,FINSEQ_1:34;
    end;
    suppose that
A3:   n <> 0 and
A4:   m <> 0;
      len M2 = m by MATRIX_1:def 2;
      then
A5:   width M2 = k by A4,MATRIX_1:20;
      len M1 = n by MATRIX_1:def 2;
      then
A6:   width M1 = k by A3,MATRIX_1:20;
      ex n st for x st x in rng (M1^M2) ex p be FinSequence of D st x = p
      & len p = n
      proof
        take k;
        let x such that
A7:     x in rng (M1^M2);
        rng (M1^M2) c= D* by FINSEQ_1:def 4;
        then reconsider p = x as FinSequence of D by A7,FINSEQ_1:def 11;
        take p;
A8:     x in rng M1 \/ rng M2 by A7,FINSEQ_1:31;
        now
          per cases by A8,XBOOLE_0:def 3;
          suppose
            x in rng M1;
            then consider y1 such that
A9:         y1 in dom M1 and
A10:        x = M1.y1 by FUNCT_1:def 3;
            reconsider y1 as Nat by A9,FINSEQ_3:23;
            x = Line(M1,y1) by A9,A10,MATRIX_2:16;
            hence len p = k by A6,MATRIX_1:def 7;
          end;
          suppose
            x in rng M2;
            then consider y2 such that
A11:        y2 in dom M2 and
A12:        x = M2.y2 by FUNCT_1:def 3;
            reconsider y2 as Nat by A11,FINSEQ_3:23;
            x = Line(M2,y2) by A11,A12,MATRIX_2:16;
            hence len p = k by A5,MATRIX_1:def 7;
          end;
        end;
        hence thesis;
      end;
      then reconsider M3 = M1^M2 as Matrix of D by MATRIX_1:9;
      len M1 = n & len M2 = m by MATRIX_1:def 2;
      then
A13:  len M3 = n + m by FINSEQ_1:22;
      then consider s be FinSequence such that
A14:  s in rng M3 and
A15:  len s = width M3 by A3,MATRIX_1:def 3;
A16:  s in rng M1 \/ rng M2 by A14,FINSEQ_1:31;
      now
        per cases by A16,XBOOLE_0:def 3;
        suppose
          s in rng M1;
          then consider y1 such that
A17:      y1 in dom M1 and
A18:      s = M1.y1 by FUNCT_1:def 3;
          reconsider y1 as Nat by A17,FINSEQ_3:23;
          s = Line(M1,y1) by A17,A18,MATRIX_2:16;
          hence width M3 = k by A6,A15,MATRIX_1:def 7;
        end;
        suppose
          s in rng M2;
          then consider y2 such that
A19:      y2 in dom M2 and
A20:      s = M2.y2 by FUNCT_1:def 3;
          reconsider y2 as Nat by A19,FINSEQ_3:23;
          s = Line(M2,y2) by A19,A20,MATRIX_2:16;
          hence width M3 = k by A5,A15,MATRIX_1:def 7;
        end;
      end;
      hence thesis by A3,A13,MATRIX_1:20;
    end;
  end;
end;

theorem
  for M1 be Matrix of n,k,D, M2 be Matrix of m,k,D st i in dom M1 holds
  Line(M1^M2,i) = Line(M1,i)
proof
  let M1 be Matrix of n,k,D;
  let M2 be Matrix of m,k,D such that
A1: i in dom M1;
  reconsider i1=i as Element of NAT by ORDINAL1:def 12;
  dom M1 c= dom (M1^M2) by FINSEQ_1:26;
  hence Line(M1^M2,i) = (M1^M2).i by A1,MATRIX_2:16
    .= M1.i1 by A1,FINSEQ_1:def 7
    .= Line(M1,i) by A1,MATRIX_2:16;
end;

theorem Th24:
  for M1 be Matrix of n,k,D, M2 be Matrix of m,k,D st
  width M1 = width M2 holds width (M1^M2) = width M1
proof
  let M1 be Matrix of n,k,D;
  let M2 be Matrix of m,k,D such that
A1: width M1 = width M2;
  consider n such that
A2: for x st x in rng (M1^M2) ex P be FinSequence of D st x = P & len P
  = n by MATRIX_1:9;
  per cases;
  suppose
A3: len (M1^M2) = 0;
    then len M1 + len M2 = 0 by FINSEQ_1:22;
    then
A4: len M1 = 0;
    width (M1^M2) = 0 by A3,MATRIX_1:def 3
      .= width M1 by A4,MATRIX_1:def 3;
    hence thesis;
  end;
  suppose
A5: len (M1^M2) > 0;
    then
A6: len M1 + len M2 > 0+0 by FINSEQ_1:22;
    consider s be FinSequence such that
A7: s in rng (M1^M2) and
A8: len s = width (M1^M2) by A5,MATRIX_1:def 3;
A9: ex P be FinSequence of D st s = P & len P = n by A2,A7;
    per cases by A6;
    suppose
      len M1 > 0;
      then consider s1 be FinSequence such that
A10:  s1 in rng M1 and
A11:  len s1 = width M1 by MATRIX_1:def 3;
      rng M1 c= rng (M1^M2) by FINSEQ_1:29;
      then ex P1 be FinSequence of D st s1 = P1 & len P1 = n by A2,A10;
      hence thesis by A8,A9,A11;
    end;
    suppose
      len M2 > 0;
      then consider s2 be FinSequence such that
A12:  s2 in rng M2 and
A13:  len s2 = width M2 by MATRIX_1:def 3;
      rng M2 c= rng (M1^M2) by FINSEQ_1:30;
      then ex P2 be FinSequence of D st s2 = P2 & len P2 = n by A2,A12;
      hence thesis by A1,A8,A9,A13;
    end;
  end;
end;

theorem
  for M1 be Matrix of t,k,D, M2 be Matrix of m,k,D st n in dom M2 & i =
  len M1 + n holds Line(M1^M2,i) = Line(M2,n)
proof
  let M1 be Matrix of t,k,D;
  let M2 be Matrix of m,k,D;
  assume that
A1: n in dom M2 and
A2: i = len M1 + n;
  reconsider n1=n as Element of NAT by ORDINAL1:def 12;
  i in dom (M1^M2) by A1,A2,FINSEQ_1:28;
  hence Line(M1^M2,i) = (M1^M2).i by MATRIX_2:16
    .= M2.n1 by A1,A2,FINSEQ_1:def 7
    .= Line(M2,n) by A1,MATRIX_2:16;
end;

theorem Th26:
  for M1 be Matrix of n,k,D, M2 be Matrix of m,k,D st width M1 =
  width M2 for i st i in Seg width M1 holds Col(M1^M2,i) = Col(M1,i)^Col(M2,i)
proof
  let M1 be Matrix of n,k,D;
  let M2 be Matrix of m,k,D such that
A1: width M1 = width M2;
  let i such that
A2: i in Seg width M1;
A3: dom Col(M1^M2,i) = Seg len Col(M1^M2,i) by FINSEQ_1:def 3;
A4: len Col(M1^M2,i) = len (M1^M2) by MATRIX_1:def 8
    .= len M1 + len M2 by FINSEQ_1:22
    .= len M1 + len Col(M2,i) by MATRIX_1:def 8
    .= len Col(M1,i) + len Col(M2,i) by MATRIX_1:def 8
    .= len (Col(M1,i)^Col(M2,i)) by FINSEQ_1:22;
  now
    let j be Nat;
    assume
A5: j in dom Col(M1^M2,i);
    then j in Seg len (M1^M2) by A3,MATRIX_1:def 8;
    then
A6: j in dom (M1^M2) by FINSEQ_1:def 3;
    i in Seg width (M1^M2) by A1,A2,Th24;
    then [j,i] in [:dom(M1^M2),Seg width(M1^M2):] by A6,ZFMISC_1:87;
    then [j,i] in Indices (M1^M2) by MATRIX_1:def 4;
    then consider P be FinSequence of D such that
A7: P = (M1^M2).j and
A8: (M1^M2)*(j,i) = P.i by MATRIX_1:def 5;
A9: j in dom (Col(M1,i)^Col(M2,i)) by A4,A3,A5,FINSEQ_1:def 3;
    now
      per cases by A9,FINSEQ_1:25;
      suppose
A10:    j in dom Col(M1,i);
        then j in Seg len Col(M1,i) by FINSEQ_1:def 3;
        then j in Seg len M1 by MATRIX_1:def 8;
        then
A11:    j in dom M1 by FINSEQ_1:def 3;
        then [j,i] in [:dom M1,Seg width M1:] by A2,ZFMISC_1:87;
        then [j,i] in Indices M1 by MATRIX_1:def 4;
        then consider P1 be FinSequence of D such that
A12:    P1 = M1.j and
A13:    M1*(j,i) = P1.i by MATRIX_1:def 5;
        P = P1 by A7,A11,A12,FINSEQ_1:def 7;
        hence Col(M1^M2,i).j = M1*(j,i) by A6,A8,A13,MATRIX_1:def 8
          .= Col(M1,i).j by A11,MATRIX_1:def 8
          .= (Col(M1,i)^Col(M2,i)).j by A10,FINSEQ_1:def 7;
      end;
      suppose
        ex n be Nat st n in dom Col(M2,i) & j = len Col(M1,i) + n;
        then consider n be Nat such that
A14:    n in dom Col(M2,i) and
A15:    j = len Col(M1,i) + n;
        n in Seg len Col(M2,i) by A14,FINSEQ_1:def 3;
        then n in Seg len M2 by MATRIX_1:def 8;
        then
A16:    n in dom M2 by FINSEQ_1:def 3;
        then [n,i] in [:dom M2,Seg width M2:] by A1,A2,ZFMISC_1:87;
        then [n,i] in Indices M2 by MATRIX_1:def 4;
        then consider P2 be FinSequence of D such that
A17:    P2 = M2.n and
A18:    M2*(n,i) = P2.i by MATRIX_1:def 5;
        len Col(M2,i) = len M2 by MATRIX_1:def 8;
        then len Col(M1,i) = len M1 & dom Col(M2,i) = dom M2 by FINSEQ_3:29
,MATRIX_1:def 8;
        then P = P2 by A7,A14,A15,A17,FINSEQ_1:def 7;
        hence Col(M1^M2,i).j = M2*(n,i) by A6,A8,A18,MATRIX_1:def 8
          .= Col(M2,i).n by A16,MATRIX_1:def 8
          .= (Col(M1,i)^Col(M2,i)).j by A14,A15,FINSEQ_1:def 7;
      end;
    end;
    hence Col(M1^M2,i).j = (Col(M1,i)^Col(M2,i)).j;
  end;
  hence thesis by A4,FINSEQ_2:9;
end;

theorem Th27:
  for M1 be Matrix of n,k,the carrier of V, M2 be Matrix of m,k,
  the carrier of V holds Sum(M1^M2) = (Sum M1)^(Sum M2)
proof
  let M1 be Matrix of n,k,the carrier of V;
  let M2 be Matrix of m,k,the carrier of V;
A1: dom Sum(M1^M2) = Seg len Sum(M1^M2) by FINSEQ_1:def 3;
A2: now
    let i be Nat;
    assume
A3: i in dom Sum(M1^M2);
    then i in Seg len (M1^M2) by A1,Def6;
    then
A4: i in dom (M1^M2) by FINSEQ_1:def 3;
    now
      per cases by A4,FINSEQ_1:25;
      suppose
A5:     i in dom M1;
        len M1 = len Sum M1 by Def6;
        then
A6:     dom M1 = dom Sum M1 by FINSEQ_3:29;
        thus Sum(M1^M2).i = (Sum(M1^M2))/.i by A3,PARTFUN1:def 6
          .= Sum ((M1^M2)/.i) by A3,Def6
          .= Sum (M1/.i) by A5,FINSEQ_4:68
          .= (Sum M1)/.i by A5,A6,Def6
          .= (Sum M1).i by A5,A6,PARTFUN1:def 6
          .= ((Sum M1)^(Sum M2)).i by A5,A6,FINSEQ_1:def 7;
      end;
      suppose
A7:     ex n be Nat st n in dom M2 & i = len M1 + n;
A8:     len M1 = len Sum M1 by Def6;
        len M2 = len Sum M2 by Def6;
        then
A9:     dom M2 = dom Sum M2 by FINSEQ_3:29;
        consider n be Nat such that
A10:    n in dom M2 and
A11:    i = len M1 + n by A7;
        thus Sum(M1^M2).i = (Sum(M1^M2))/.i by A3,PARTFUN1:def 6
          .= Sum ((M1^M2)/.i) by A3,Def6
          .= Sum (M2/.n) by A10,A11,FINSEQ_4:69
          .= (Sum M2)/.n by A10,A9,Def6
          .= (Sum M2).n by A10,A9,PARTFUN1:def 6
          .= ((Sum M1)^(Sum M2)).i by A10,A11,A8,A9,FINSEQ_1:def 7;
      end;
    end;
    hence Sum(M1^M2).i = ((Sum M1)^(Sum M2)).i;
  end;
  len Sum(M1^M2) = len (M1^M2) by Def6
    .= len M1 + len M2 by FINSEQ_1:22
    .= len Sum M1 + len M2 by Def6
    .= len Sum M1 + len Sum M2 by Def6
    .= len ((Sum M1)^(Sum M2)) by FINSEQ_1:22;
  hence thesis by A2,FINSEQ_2:9;
end;

theorem Th28:
  for M1 be Matrix of n,k,D, M2 be Matrix of m,k,D st width M1 =
  width M2 holds (M1^M2)@ = M1@ ^^ M2@
proof
  let M1 be Matrix of n,k,D;
  let M2 be Matrix of m,k,D such that
A1: width M1 = width M2;
A2: Seg len (M1@ ^^ M2@) = dom (M1@ ^^ M2@) by FINSEQ_1:def 3
    .= dom (M1@) /\ dom (M2@) by PRE_POLY:def 4
    .= dom (M1@) /\ Seg len (M2@) by FINSEQ_1:def 3
    .= Seg len (M1@) /\ Seg len (M2@) by FINSEQ_1:def 3
    .= Seg width M1 /\ Seg len (M2@) by MATRIX_1:def 6
    .= Seg width M1 /\ Seg width M2 by MATRIX_1:def 6
    .= Seg width M1 by A1;
A3: dom ((M1^M2)@) = Seg len ((M1^M2)@) by FINSEQ_1:def 3;
A4: len ((M1^M2)@) = width (M1^M2) by MATRIX_1:def 6
    .= width M1 by A1,Th24
    .= len (M1@ ^^ M2@) by A2,FINSEQ_1:6;
  now
    let i be Nat;
    assume
A5: i in dom ((M1^M2)@);
    then
A6: i in Seg width (M1^M2) by A3,MATRIX_1:def 6;
A7: i in dom (M1@ ^^ M2@) by A4,A3,A5,FINSEQ_1:def 3;
    then
A8: i in dom (M1@) /\ dom (M2@) by PRE_POLY:def 4;
    then
A9: i in dom (M2@) by XBOOLE_0:def 4;
A10: i in dom (M1@) by A8,XBOOLE_0:def 4;
    reconsider m1 = M1@.i,m2 = M2@.i as FinSequence;
    i in Seg len (M1@) /\ dom (M2@) by A8,FINSEQ_1:def 3;
    then i in Seg len (M1@) /\ Seg len (M2@) by FINSEQ_1:def 3;
    then i in Seg width M1 /\ Seg len (M2@) by MATRIX_1:def 6;
    then
A11: i in Seg width M1 /\ Seg width M2 by MATRIX_1:def 6;
    thus (M1^M2)@.i = Line((M1^M2)@,i) by A5,MATRIX_2:16
      .= Col(M1^M2,i) by A6,MATRIX_2:15
      .= Col(M1,i)^Col(M2,i) by A1,A11,Th26
      .= Line(M1@,i)^Col(M2,i) by A1,A11,MATRIX_2:15
      .= Line(M1@,i)^Line(M2@,i) by A1,A11,MATRIX_2:15
      .= Line(M1@,i)^m2 by A9,MATRIX_2:16
      .= m1^m2 by A10,MATRIX_2:16
      .= (M1@ ^^ M2@).i by A7,PRE_POLY:def 4;
  end;
  hence thesis by A4,FINSEQ_2:9;
end;

theorem Th29:
  for M1,M2 be Matrix of the carrier of V1 holds Sum M1 + Sum M2 =
  Sum(M1 ^^ M2)
proof
  let M1,M2 be Matrix of the carrier of V1;
  reconsider m = min(len M1,len M2) as Element of NAT by FINSEQ_2:1;
A1: Seg m = Seg len M1 /\ Seg len M2 by FINSEQ_2:2
    .= Seg len M1 /\ dom M2 by FINSEQ_1:def 3
    .= dom M1 /\ dom M2 by FINSEQ_1:def 3
    .= dom (M1 ^^ M2) by PRE_POLY:def 4
    .= Seg len (M1 ^^ M2) by FINSEQ_1:def 3;
A2: len (Sum M1+Sum M2) = min(len Sum M1,len Sum M2) by FINSEQ_2:71
    .= min(len M1,len Sum M2) by Def6
    .= min(len M1,len M2) by Def6
    .= len (M1 ^^ M2) by A1,FINSEQ_1:6
    .= len Sum(M1 ^^ M2) by Def6;
A3: dom (Sum M1 + Sum M2) = Seg len(Sum M1 + Sum M2) by FINSEQ_1:def 3;
  now
    let i be Nat;
    assume
A4: i in dom (Sum M1+Sum M2);
    then
A5: i in dom Sum(M1 ^^ M2) by A2,A3,FINSEQ_1:def 3;
    i in Seg len (M1 ^^ M2) by A2,A3,A4,Def6;
    then
A6: i in dom (M1 ^^ M2) by FINSEQ_1:def 3;
    then
A7: i in dom M1 /\ dom M2 by PRE_POLY:def 4;
    then
A8: i in dom M1 by XBOOLE_0:def 4;
A9: i in dom M2 by A7,XBOOLE_0:def 4;
    reconsider m1 = M1.i,m2 = M2.i as FinSequence;
A10: ((M1/.i) ^ (M2/.i)) = m1 ^ (M2/.i) by A8,PARTFUN1:def 6
      .= m1 ^ m2 by A9,PARTFUN1:def 6
      .= (M1 ^^ M2).i by A6,PRE_POLY:def 4
      .= (M1 ^^ M2)/.i by A6,PARTFUN1:def 6;
    i in Seg len M2 by A9,FINSEQ_1:def 3;
    then i in Seg len (Sum M2) by Def6;
    then
A11: i in dom (Sum M2) by FINSEQ_1:def 3;
    then
A12: (Sum M2)/.i = (Sum M2).i by PARTFUN1:def 6;
    i in Seg len M1 by A8,FINSEQ_1:def 3;
    then i in Seg len (Sum M1) by Def6;
    then
A13: i in dom (Sum M1) by FINSEQ_1:def 3;
    then (Sum M1)/.i = (Sum M1).i by PARTFUN1:def 6;
    hence (Sum M1 + Sum M2).i = ((Sum M1)/.i) + ((Sum M2)/.i)
     by A4,A12,FUNCOP_1:22
      .= Sum (M1/.i) + (Sum M2/.i) by A13,Def6
      .= Sum (M1/.i) + Sum (M2/.i) by A11,Def6
      .= Sum ((M1 ^^ M2)/.i) by A10,RLVECT_1:41
      .= Sum(M1 ^^ M2)/.i by A5,Def6
      .= (Sum(M1 ^^ M2)).i by A5,PARTFUN1:def 6;
  end;
  hence thesis by A2,FINSEQ_2:9;
end;

theorem Th30:
  for P1,P2 be FinSequence of V1 st len P1 = len P2 holds
  Sum(P1 + P2) = (Sum P1) + (Sum P2)
proof
  let P1,P2 be FinSequence of V1;
  assume len P1 = len P2;
  then reconsider
  R1 = P1, R2 = P2 as Element of (len P1)-tuples_on (the carrier of
  V1) by FINSEQ_2:92;
  thus Sum(P1+P2) = Sum (R1 + R2) .= Sum P1 + Sum P2 by FVSUM_1:76;
end;

theorem Th31:
  for M1,M2 be Matrix of the carrier of V1 st len M1 = len M2
  holds Sum Sum M1 + Sum Sum M2 = Sum Sum(M1 ^^ M2)
proof
  let M1,M2 be Matrix of the carrier of V1 such that
A1: len M1 = len M2;
  len Sum M1 = len M1 by Def6
    .= len Sum M2 by A1,Def6;
  hence Sum Sum M1 + Sum Sum M2 = Sum (Sum M1 + Sum M2) by Th30
    .= Sum Sum(M1 ^^ M2) by Th29;
end;

theorem Th32:
  for M be Matrix of the carrier of V1 holds Sum Sum M = Sum Sum (M@)
proof
  defpred X[Nat] means for M be Matrix of the carrier of V1 st len M = $1
  holds Sum Sum M = Sum Sum (M@);
  let M be Matrix of the carrier of V1;
A1: for P be FinSequence of V1 holds Sum Sum <*P*> = Sum Sum (<*P*>@)
  proof
    defpred X[FinSequence of V1] means Sum Sum <*$1*> = Sum Sum(<*$1*>@);
    let P be FinSequence of V1;
    len <*<*>(the carrier of V1)*> = 1 by MATRIX_1:def 2;
    then width <*<*>(the carrier of V1)*> = 0 by MATRIX_1:20;
    then
A2: len (<*<*>(the carrier of V1)*>@) = 0 by MATRIX_1:def 6;
A3: for P being FinSequence of V1, x being Element of V1 st X[P] holds X[P
    ^<*x*>]
    proof
      let P be FinSequence of V1, x be Element of V1 such that
A4:   Sum Sum <*P*> = Sum Sum (<*P*>@);
      Seg len (<*P*> ^^ <*<*x*>*>) = dom (<*P*> ^^ <*<*x*>*>) by FINSEQ_1:def 3
        .= dom <*P*> /\ dom <*<*x*>*> by PRE_POLY:def 4
        .= Seg 1 /\ dom <*<*x*>*> by FINSEQ_1:38
        .= Seg 1 /\ Seg 1 by FINSEQ_1:38
        .= Seg 1;
      then
A5:   len (<*P*> ^^ <*<*x*>*>) = 1 by FINSEQ_1:6
        .= len <*P^<*x*>*> by FINSEQ_1:39;
      then
A6:   dom (<*P*> ^^ <*<*x*>*>) = Seg len <*P^<*x*>*> by FINSEQ_1:def 3;
A7:   now
        let i be Nat;
        assume
A8:     i in dom (<*P*> ^^ <*<*x*>*>);
        then i in { 1 } by A6,FINSEQ_1:2,40;
        then
A9:     i = 1 by TARSKI:def 1;
        reconsider m1 = <*P*>.i, m2 = <*<*x*>*>.i as FinSequence;
        thus (<*P*> ^^ <*<*x*>*>).i = m1 ^ m2 by A8,PRE_POLY:def 4
          .= P ^ m2 by A9,FINSEQ_1:40
          .= P ^ <*x*> by A9,FINSEQ_1:40
          .= <*P^<*x*>*>.i by A9,FINSEQ_1:40;
      end;
      per cases;
      suppose
        len P = 0;
        then
A10:    P = {};
        hence Sum Sum <*P^<*x*>*> = Sum Sum <*<*x*>*> by FINSEQ_1:34
          .= Sum Sum (<*<*x*>*>@) by Th15
          .= Sum Sum (<*P^<*x*>*>@) by A10,FINSEQ_1:34;
      end;
      suppose
A11:    len P <> 0;
A12:    len <*<*x*>*> = 1 by FINSEQ_1:40;
        then
A13:    width <*<*x*>*> = len <*x*> by MATRIX_1:20
          .= 1 by FINSEQ_1:40;
        then
A14:    len (<*<*x*>*>@) = 1 by MATRIX_1:def 6;
A15:    len <*P*> = 1 by FINSEQ_1:40;
        then
A16:    width <*P*> = len P by MATRIX_1:20;
        then
A17:    len (<*P*>@) = len P by MATRIX_1:def 6;
        width (<*P*>@) = 1 by A11,A15,A16,MATRIX_2:10;
        then reconsider
        d1 = <*P*>@ as Matrix of len P,1,the carrier of V1 by A11,A17,
MATRIX_1:20;
A18:    len <*P^<*x*>*> = 1 by FINSEQ_1:40;
        then
A19:    width <*P^<*x*>*> = len (P^<*x*>) by MATRIX_1:20
          .= len P + len <*x*> by FINSEQ_1:22
          .= len P + 1 by FINSEQ_1:40;
A20:    (<*<*x*>*>@)@ = <*<*x*>*> by A12,A13,MATRIX_2:13;
A21:    width (<*P*>@) = len <*P*> by A11,A16,MATRIX_2:10
          .= width (<*<*x*>*>@) by A15,A12,A13,MATRIX_2:10;
        then width (<*<*x*>*>@) = 1 by A11,A15,A16,MATRIX_2:10;
        then reconsider
        d2 = <*<*x*>*>@ as Matrix of 1,1,the carrier of V1 by A14,MATRIX_1:20;
A22:    (d1 ^ d2)@ = ((<*P*>@)@) ^^ ((<*<*x*>*>@)@) by A21,Th28
          .= <*P*> ^^ <*<*x*>*> by A11,A15,A16,A20,MATRIX_2:13
          .= <*P^<*x*>*> by A5,A7,FINSEQ_2:9
          .= (<*P^<*x*>*>@)@ by A18,A19,MATRIX_2:13;
A23:    len ((<*P*>@) ^ (<*<*x*>*>@)) = len (<*P*>@) + len (<*<*x*>*>@)
        by FINSEQ_1:22
          .= width <*P*> + len (<*<*x*>*>@) by MATRIX_1:def 6
          .= width <*P*> + width <*<*x*>*> by MATRIX_1:def 6
          .= len (<*P^<*x*>*>@) by A16,A13,A19,MATRIX_1:def 6;
        thus Sum Sum <*P^<*x*>*> = Sum Sum (<*P*> ^^ <*<*x*>*>) by A5,A7,
FINSEQ_2:9
          .= Sum Sum (<*P*>@) + Sum Sum <*<*x*>*> by A4,A15,A12,Th31
          .= Sum Sum (<*P*>@) + Sum Sum (<*<*x*>*>@) by Th15
          .= Sum (Sum d1 ^ Sum d2) by RLVECT_1:41
          .= Sum Sum (d1 ^ d2) by Th27
          .= Sum Sum (<*P^<*x*>*>@) by A23,A22,MATRIX_2:9;
      end;
    end;
    <*<*>(the carrier of V1)*> is Matrix of 0+1,0,the carrier of V1;
    then Sum Sum <*<*>(the carrier of V1)*> = 0.V1 by Th14
      .= Sum Sum (<*<*>(the carrier of V1)*>@) by A2,Th13;
    then
A24: X[<*>(the carrier of V1)];
    for P be FinSequence of V1 holds X[P] from FINSEQ_2:sch 2(A24,A3);
    hence thesis;
  end;
A25: for n st X[n] holds X[n+1]
  proof
    let n such that
A26: for M be Matrix of the carrier of V1 st len M = n holds Sum Sum M
    = Sum Sum (M@);
    thus for M be Matrix of the carrier of V1 st len M = n+1 holds Sum Sum M =
    Sum Sum (M@)
    proof
      let M be Matrix of the carrier of V1 such that
A27:  len M = n+1;
A28:  M <> {} by A27;
A29:  dom M = Seg len M by FINSEQ_1:def 3;
      per cases;
      suppose
A30:    n = 0;
        then M.1 = Line(M,1) by A27,A29,FINSEQ_1:4,MATRIX_2:16;
        then reconsider G = M.1 as FinSequence of V1;
        M = <*G*> by A27,A30,FINSEQ_1:40;
        hence thesis by A1;
      end;
      suppose
A31:    n > 0;
A32:    M.(n+1) = Line(M,n+1) by A27,A29,FINSEQ_1:4,MATRIX_2:16;
        then reconsider M1 = M.(n+1) as FinSequence of V1;
        reconsider R = <*M1*> as Matrix of 1,width M,the carrier of V1 by A32,
MATRIX_1:def 7;
        reconsider M9 = M as Matrix of n+1,width M,the carrier of V1 by A27,
MATRIX_1:20;
        reconsider W = Del(M9,n+1) as Matrix of n,width M,the carrier of V1
          by Th3;
A33:    width W = width M9 by A31,Th2
          .= width R by Th2;
A34:    len (W@) = width W by MATRIX_1:def 6
          .= len (R@) by A33,MATRIX_1:def 6;
A35:    len Del(M,n+1) = n by A27,Th1;
        thus Sum Sum M = Sum Sum (W ^ R) by A28,Th4,A27
          .= Sum (Sum W ^ Sum R) by Th27
          .= Sum Sum Del(M,n+1) + Sum Sum R by RLVECT_1:41
          .= Sum Sum (Del(M,n+1)@) + Sum Sum R by A26,A35
          .= Sum Sum (Del(M,n+1)@) + Sum Sum (R@) by A1
          .= Sum Sum ((W@) ^^ (R@)) by A34,Th31
          .= Sum Sum ((W ^ R)@) by A33,Th28
          .= Sum Sum (M@) by A28,Th4,A27;
      end;
    end;
  end;
A36: X[0]
  proof
    let M be Matrix of the carrier of V1;
    assume
A37: len M = 0;
    then width M = 0 by MATRIX_1:def 3;
    then
A38: len (M@) = 0 by MATRIX_1:def 6;
    thus Sum Sum M = 0.V1 by A37,Th13
      .= Sum Sum (M@) by A38,Th13;
  end;
  for n holds X[n] from NAT_1:sch 2(A36,A25);
  then X[len M];
  hence thesis;
end;

theorem Th33:
  for M being Matrix of n,m,the carrier of K st n > 0 & m > 0
  for p,d being FinSequence of K st len p = n & len d = m &
  for j st j in dom d holds d/.j = Sum mlt(p,Col(M,j))
  for b,c being FinSequence of V1 st len b = m & len c = n &
  for i st i in dom c holds c/.i = Sum lmlt(Line(M,i),b) holds
  Sum lmlt(p,c) = Sum lmlt(d,b)
proof
  let M be Matrix of n,m,the carrier of K such that
A1: n > 0 and
A2: m > 0;
A3: len M = n by A1,MATRIX_1:23;
  reconsider n1=n, m1=m as Element of NAT by ORDINAL1:def 12;
  let p,d be FinSequence of K such that
A4: len p = n and
A5: len d = m and
A6: for j st j in dom d holds d/.j = Sum mlt(p,Col(M,j));
  let b,c be FinSequence of V1 such that
A7: len b = m and
A8: len c = n and
A9: for i st i in dom c holds c/.i = Sum lmlt(Line(M,i),b);
  deffunc V(Nat,Nat) = (p/.$1) * (M*($1,$2)) * (b/.$2);
  consider M1 being Matrix of n1,m1,the carrier of V1 such that
A10: for i,j st [i,j] in Indices M1 holds M1*(i,j) = V(i,j) from MATRIX_1
  :sch 1;
A11: width M1 = len (M1@) by MATRIX_1:def 6
    .= len Sum (M1@) by Def6;
A12: dom d = dom b by A5,A7,FINSEQ_3:29;
  then
A13: dom lmlt(d,b) = dom b by Th12;
  then
A14: len lmlt(d,b) = len b by FINSEQ_3:29
    .= len Sum (M1@) by A1,A7,A11,MATRIX_1:23;
  then
A15: dom lmlt(d,b) = Seg len Sum(M1@) by FINSEQ_1:def 3;
A16: width M1 = m by A1,MATRIX_1:23;
A17: len M1 = n by A1,MATRIX_1:23;
A18: dom lmlt(d,b) = dom d by A12,Th12;
A19: now
A20: Seg len Sum(M1@) = dom Sum(M1@) by FINSEQ_1:def 3;
    let j be Nat such that
A21: j in dom lmlt(d,b);
A22: j in dom Sum(M1@) by A15,A21,FINSEQ_1:def 3;
A23: j in dom d by A12,A21,Th12;
A24: d/.j = d.j & b/.j = b.j by A18,A13,A21,PARTFUN1:def 6;
    len Sum(M1@) = len (M1@) by Def6;
    then
A25: dom Sum(M1@) = dom (M1@) by FINSEQ_3:29;
    then
A26: M1@/.j = M1@.j by A22,PARTFUN1:def 6
      .= Line(M1@,j) by A22,A25,MATRIX_2:16;
    reconsider H = mlt(p,Col(M,j)) as FinSequence of K;
    deffunc V(Nat) = (H/.$1) * (b/.j);
    consider G be FinSequence of V1 such that
A27: len G = len p & for i be Nat st i in dom G holds G.i = V(i) from
    FINSEQ_2:sch 1;
A28: len p = len Col(M,j) by A4,A3,MATRIX_1:def 8;
    then
A29: len ((the multF of K).:(p,Col(M,j))) = len p by FINSEQ_2:72;
    then
A30: dom H = dom G by A27,FINSEQ_3:29;
A31: dom p = dom G by A27,FINSEQ_3:29;
A32: len Line(M1@,j) = width (M1@) by MATRIX_1:def 7
      .= len ((M1@)@) by MATRIX_1:def 6
      .= len G by A1,A2,A4,A17,A16,A27,MATRIX_2:13;
    then
A33: dom Line(M1@,j) = Seg len G by FINSEQ_1:def 3;
A34: dom G = Seg len p by A27,FINSEQ_1:def 3;
A35: now
      let i be Nat;
A36:  dom M = Seg len M by FINSEQ_1:def 3;
      assume
A37:  i in dom Line(M1@,j);
      then
A38:  i in Seg len ((the multF of K).:(p,Col(M,j))) by A27,A28,A33,FINSEQ_2:72;
      then
A39:  i in dom H by FINSEQ_1:def 3;
A40:  i in dom ((the multF of K).:(p,Col(M,j))) by A38,FINSEQ_1:def 3;
A41:  Seg len G = dom G by FINSEQ_1:def 3;
      then
A42:  (p/.i) * (M*(i,j)) = (the multF of K).(p.i,M*(i,j)) by A31,A33,A37,
PARTFUN1:def 6
        .= (the multF of K).(p.i,Col(M,j).i) by A4,A3,A27,A33,A37,A36,
MATRIX_1:def 8
        .= ((the multF of K).:(p,Col(M,j))).i by A40,FUNCOP_1:22
        .= H/.i by A39,PARTFUN1:def 6;
      dom M1 = dom G by A4,A17,A27,FINSEQ_3:29;
      then [i,j] in [:dom M1,Seg width M1:] by A11,A15,A21,A33,A37,A41,
ZFMISC_1:87;
      then
A43:  [i,j] in Indices M1 by MATRIX_1:def 4;
      i in Seg width (M1@) by A32,A33,A37,MATRIX_1:def 7;
      hence Line(M1@,j).i = (M1@)*(j,i) by MATRIX_1:def 7
        .= M1*(i,j) by A43,MATRIX_1:def 6
        .= (H/.i) * (b/.j) by A10,A43,A42
        .= G.i by A27,A34,A33,A37;
    end;
    thus lmlt(d,b).j = (the lmult of V1).(d.j,b.j) by A21,FUNCOP_1:22
      .= (d/.j) * (b/.j) by A24,VECTSP_1:def 12
      .= Sum H * (b/.j) by A6,A23
      .= Sum G by A27,A29,A30,Th10
      .= Sum (M1@/.j) by A32,A35,A26,FINSEQ_2:9
      .= Sum (M1@)/.j by A22,Def6
      .= (Sum (M1@)).j by A15,A21,A20,PARTFUN1:def 6;
  end;
A44: dom p = dom c by A4,A8,FINSEQ_3:29;
  then
A45: dom lmlt(p,c) = dom p by Th12;
  then
A46: len lmlt(p,c) = len p by FINSEQ_3:29
    .= len M1 by A4,MATRIX_1:def 2
    .= len Sum M1 by Def6;
  now
    let i be Nat such that
A47: i in dom Sum M1;
A48: i in dom c by A44,A45,A46,A47,FINSEQ_3:29;
    then
A49: c.i = c/.i & p.i = p/.i by A44,PARTFUN1:def 6;
    i in Seg len Sum M1 by A47,FINSEQ_1:def 3;
    then i in Seg len M1 by Def6;
    then
A50: i in dom M1 by FINSEQ_1:def 3;
    then
A51: M1/.i = M1.i by PARTFUN1:def 6
      .= Line(M1,i) by A50,MATRIX_2:16;
    deffunc V(Nat) = (p/.i) * (lmlt(Line(M,i),b)/.$1);
    consider F be FinSequence of V1 such that
A52: len F = len b & for j be Nat st j in dom F holds F.j = V(j) from
    FINSEQ_2:sch 1;
A53: len F = width M by A1,A7,A52,MATRIX_1:23;
A54: dom Line(M,i) = Seg len Line(M,i) by FINSEQ_1:def 3
      .= Seg len F by A53,MATRIX_1:def 7
      .= dom b by A52,FINSEQ_1:def 3;
    then dom lmlt(Line(M,i),b) = dom b by Th12;
    then
A55: len F = len lmlt(Line(M,i),b) & dom F = dom lmlt(Line(M,i),b) by A52,
FINSEQ_3:29;
A56: len F = width M1 by A1,A7,A52,MATRIX_1:23;
    then
A57: len Line(M1,i) = len F by MATRIX_1:def 7;
    then
A58: dom (M1/.i) = Seg len F by A51,FINSEQ_1:def 3;
A59: dom F = Seg len b by A52,FINSEQ_1:def 3;
A60: now
      let j be Nat;
      assume
A61:  j in dom (M1/.i);
      then
A62:  Line(M,i).j = M*(i,j) by A53,A58,MATRIX_1:def 7;
      [i,j] in [:dom M1,Seg width M1:] by A56,A50,A58,A61,ZFMISC_1:87;
      then
A63:  [i,j] in Indices M1 by MATRIX_1:def 4;
A64:  j in dom b by A52,A58,A61,FINSEQ_1:def 3;
      then
A65:  b.j = b/.j by PARTFUN1:def 6;
A66:  j in dom (lmlt(Line(M,i),b)) by A54,A64,Th12;
      then
A67:  (lmlt(Line(M,i),b)/.j) = lmlt(Line(M,i),b).j by PARTFUN1:def 6
        .= (the lmult of V1).(Line(M,i).j,b.j) by A66,FUNCOP_1:22
        .= M*(i,j) * (b/.j) by A65,A62,VECTSP_1:def 12;
      thus (M1/.i).j = M1*(i,j) by A56,A51,A58,A61,MATRIX_1:def 7
        .= (p/.i) * (M*(i,j)) * (b/.j) by A10,A63
        .= (p/.i) * (lmlt(Line(M,i),b)/.j) by A67,VECTSP_1:def 16
        .= F.j by A52,A59,A58,A61;
    end;
A68: for j be Element of NAT st j in dom F holds F.j = (p/.i) * (lmlt(Line
    (M,i),b)/.j) by A52;
    i in dom ((the lmult of V1).:(p,c)) by A46,A47,FINSEQ_3:29;
    hence lmlt(p,c).i = (the lmult of V1).(p.i,c.i) by FUNCOP_1:22
      .= (p/.i) * (c/.i) by A49,VECTSP_1:def 12
      .= (p/.i) * Sum lmlt(Line(M,i),b) by A9,A48
      .= Sum F by A55,A68,RLVECT_2:67
      .= Sum (M1/.i) by A57,A51,A60,FINSEQ_2:9
      .= (Sum M1)/.i by A47,Def6
      .= (Sum M1).i by A47,PARTFUN1:def 6;
  end;
  hence Sum lmlt(p,c) = Sum Sum M1 by A46,FINSEQ_2:9
    .= Sum Sum (M1@) by Th32
    .= Sum lmlt(d,b) by A14,A19,FINSEQ_2:9;
end;

begin :: Decomposition of a Vector in Basis

definition
  let K be Field;
  let V be finite-dimensional VectSp of K;
  let b1 be OrdBasis of V;
  let W be Element of V;
  func W|--b1 -> FinSequence of K means
  :Def7:
  len it = len b1 & ex KL be
Linear_Combination of V st W = Sum(KL) & Carrier KL c= rng b1 & for k st 1<=k &
  k<=len it holds it/.k=KL.(b1/.k);
  existence
  proof
    reconsider b2 = rng b1 as Basis of V by Def2;
    consider KL be Linear_Combination of V such that
A1: W = Sum(KL) and
A2: Carrier KL c= b2 by Th8;
    deffunc V(Nat) = KL.(b1/.$1);
    consider A be FinSequence of K such that
A3: len A = len b1 and
A4: for k be Nat st k in dom A holds A.k = V(k) from FINSEQ_2:sch 1;
    take A;
    thus len A = len b1 by A3;
    take KL;
    thus W = Sum(KL) by A1;
    thus Carrier KL c= rng b1 by A2;
    let k;
A5: dom A = Seg len b1 by A3,FINSEQ_1:def 3;
    assume 1<=k & k<=len A;
    then
A6: k in Seg len b1 by A3,FINSEQ_1:1;
    then k in dom A by A3,FINSEQ_1:def 3;
    then A.k = A/.k by PARTFUN1:def 6;
    hence thesis by A4,A5,A6;
  end;
  uniqueness
  proof
    reconsider b = rng b1 as Basis of V by Def2;
    let F1,F2 be FinSequence of K;
    assume
A7: len F1 = len b1;
    given KL1 be Linear_Combination of V such that
A8: W = Sum(KL1) & Carrier(KL1) c= rng b1 and
A9: for k st 1<=k & k<=len F1 holds F1/.k=KL1.(b1/.k);
    assume
A10: len F2 = len b1;
    given KL2 be Linear_Combination of V such that
A11: W = Sum(KL2) & Carrier(KL2) c= rng b1 and
A12: for k st 1<=k & k<=len F2 holds F2/.k=KL2.(b1/.k);
A13: b is linearly-independent by VECTSP_7:def 3;
    for k be Nat st 1<=k & k<=len F1 holds F1.k = F2.k
    proof
      let k be Nat;
      assume
A14:  1<=k & k<=len F1;
      then
A15:  k in dom F2 by A7,A10,FINSEQ_3:25;
      k in dom F1 by A14,FINSEQ_3:25;
      hence F1.k = F1/.k by PARTFUN1:def 6
        .= KL1.(b1/.k) by A9,A14
        .= KL2.(b1/.k) by A8,A11,A13,Th5
        .= F2/.k by A7,A10,A12,A14
        .= F2.k by A15,PARTFUN1:def 6;
    end;
    hence thesis by A7,A10,FINSEQ_1:14;
  end;
end;

Lm1: for K being Field for V being finite-dimensional VectSp of K for b being
OrdBasis of V for W being Element of V holds dom (W|--b) = dom b
proof
  let K be Field, V be finite-dimensional VectSp of K, b be OrdBasis of V,
      W be Element of V;
  len (W|--b) = len b by Def7;
  hence thesis by FINSEQ_3:29;
end;

theorem Th34:
  v1|--b2 = v2|--b2 implies v1 = v2
proof
  consider KL1 be Linear_Combination of V2 such that
A1: v1 = Sum(KL1) and
A2: Carrier KL1 c= rng b2 and
A3: for t st 1<=t & t<=len (v1|--b2) holds (v1|--b2)/.t = KL1.(b2/.t) by Def7;
  consider KL2 be Linear_Combination of V2 such that
A4: v2 = Sum(KL2) and
A5: Carrier KL2 c= rng b2 and
A6: for t st 1<=t & t<=len (v2|--b2) holds (v2|--b2)/.t = KL2.(b2/.t) by Def7;
  assume
A7: v1|--b2 = v2|--b2;
A8: now
    let t be Nat;
    assume
A9: 1<=t & t<=len (v1|--b2);
    hence KL1.(b2/.t) = (v2|--b2)/.t by A7,A3
      .= KL2.(b2/.t) by A7,A6,A9;
  end;
A10: Carrier KL1 \/ Carrier KL2 c= rng b2 by A2,A5,XBOOLE_1:8;
  now
    let v be Vector of V2;
    per cases;
    suppose
A11:  not v in Carrier KL1 \/ Carrier KL2;
      then not v in Carrier KL2 by XBOOLE_0:def 3;
      then
A12:  KL2.v = 0.K by VECTSP_6:2;
      not v in Carrier KL1 by A11,XBOOLE_0:def 3;
      hence KL1.v = KL2.v by A12,VECTSP_6:2;
    end;
    suppose
      v in Carrier KL1 \/ Carrier KL2;
      then consider x such that
A13:  x in dom b2 and
A14:  v = b2.x by A10,FUNCT_1:def 3;
      reconsider x as Nat by A13,FINSEQ_3:23;
      x<=len b2 by A13,FINSEQ_3:25;
      then
A15:  x<=len (v1|--b2) by Def7;
      v = b2/.x & 1<=x by A13,A14,FINSEQ_3:25,PARTFUN1:def 6;
      hence KL1.v = KL2.v by A8,A15;
    end;
  end;
  hence thesis by A1,A4,VECTSP_6:def 7;
end;

theorem Th35:
  v = Sum lmlt(v|--b1,b1)
proof
  consider KL be Linear_Combination of V1 such that
A1: v = Sum KL & Carrier KL c= rng b1 and
A2: for k st 1<=k & k<=len (v|--b1) holds (v|--b1)/.k=KL.(b1/.k) by Def7;
  len (v|--b1) = len b1 by Def7;
  then
A3: dom (v|--b1) = dom b1 by FINSEQ_3:29;
  then
A4: dom b1 = dom lmlt(v|--b1,b1) by Th12;
 len (KL (#) b1) = len b1 by VECTSP_6:def 5
    .= len lmlt(v|--b1,b1) by A4,FINSEQ_3:29; then
A5: dom (KL (#) b1) = dom lmlt(v|--b1,b1) by FINSEQ_3:29;
A6: now
    let t be Nat;
    assume
A7: t in dom lmlt(v|--b1,b1);
    then
A8: b1/.t = b1.t by A4,PARTFUN1:def 6;
    t in dom (v|--b1) by A3,A7,Th12;
    then
A9: t<=len (v|--b1) by FINSEQ_3:25;
A10: 1<=t by A7,FINSEQ_3:25;
    then
A11: (v|--b1)/.t = (v|--b1).t by A9,FINSEQ_4:15;
    t in dom (KL (#) b1) by A5,A7;
    hence (KL (#) b1).t = KL.(b1/.t) * (b1/.t) by VECTSP_6:def 5
      .= ((v|--b1)/.t) * (b1/.t) by A2,A10,A9
      .= (the lmult of V1).((v|--b1).t,b1.t) by A8,A11,VECTSP_1:def 12
      .= lmlt(v|--b1,b1).t by A7,FUNCOP_1:22;
  end;
  b1 is one-to-one by Def2;
  hence v = Sum(KL (#) b1) by A1,Th20
    .= Sum lmlt(v|--b1,b1) by A5,A6,FINSEQ_1:13;
end;

theorem Th36:
  len d = len b1 implies d = Sum(lmlt(d,b1)) |-- b1
proof
  reconsider T = rng b1 as finite Subset of V1 by Def2;
  defpred X[Element of V1, Element of K] means ($1 in rng b1 implies (for k st
k in dom b1 & b1/.k = $1 holds $2 = d/.k)) & (not $1 in rng b1 implies $2 = 0.K
  );
A1: for v ex u being Element of K st X[v,u]
  proof
    let v be Element of V1;
    per cases;
    suppose
A2:   v in rng b1;
      then consider k be Element of NAT such that
A3:   k in dom b1 and
A4:   b1/.k = v by PARTFUN2:2;
      take u = d/.k;
      now
A5:     b1 is one-to-one by Def2;
        let i;
        assume that
A6:     i in dom b1 and
A7:     b1/.i = v;
        b1.i = b1/.k by A4,A6,A7,PARTFUN1:def 6
          .= b1.k by A3,PARTFUN1:def 6;
        hence u = d/.i by A3,A6,A5,FUNCT_1:def 4;
      end;
      hence thesis by A2;
    end;
    suppose
A8:   not v in rng b1;
      take 0.K;
      thus thesis by A8;
    end;
  end;
  consider KL be Function of V1, K such that
A9: for v holds X[v,KL.v] from FUNCT_2:sch 3(A1);
A10: now
    take T;
    let v be Element of V1;
    assume not v in T;
    hence KL.v = 0.K by A9;
  end;
  now
    take f = KL;
    thus KL = f & dom f = the carrier of V1 & rng f c= the carrier of K by
FUNCT_2:def 1,RELAT_1:def 19;
  end;
  then KL in Funcs(the carrier of V1, the carrier of K) by FUNCT_2:def 2;
  then reconsider KL1 = KL as Linear_Combination of V1 by A10,VECTSP_6:def 1;
  assume
A11: len d = len b1;
  now
    take KL1;
A12: b1 is one-to-one by Def2;
    thus
A13: for k st 1<=k & k<=len d holds d/.k=KL1.(b1/.k)
    proof
      let k;
      assume 1<=k & k<=len d;
      then
A14:  k in dom b1 by A11,FINSEQ_3:25;
      then b1.k = b1/.k by PARTFUN1:def 6;
      then b1/.k in rng b1 by A14,FUNCT_1:def 3;
      hence thesis by A9,A14;
    end;
    for x holds x in Carrier KL1 implies x in rng b1
    proof
      let x;
      assume x in Carrier KL1;
      then
A15:  ex v st x = v & KL1.v <> 0.K by VECTSP_6:1;
      assume not x in rng b1;
      hence contradiction by A9,A15;
    end;
    hence
A16: Carrier KL1 c= rng b1 by TARSKI:def 3;
A17: dom d = dom b1 by A11,FINSEQ_3:29;
    then
A18: dom lmlt(d,b1) = dom b1 by Th12;
    then
A19: len lmlt(d,b1) = len b1 by FINSEQ_3:29
      .= len (KL1 (#) b1) by VECTSP_6:def 5;
    now
      let k be Nat;
      assume
A20:  k in dom lmlt(d,b1);
      then
A21:  k in dom (KL1 (#) b1) by A19,FINSEQ_3:29;
A22:  1<=k & k<=len d by A11,A18,A20,FINSEQ_3:25;
A23:  d/.k = d.k & b1/.k = b1.k by A17,A18,A20,PARTFUN1:def 6;
      thus lmlt(d,b1).k = (the lmult of V1).(d.k,b1.k) by A20,FUNCOP_1:22
        .= (d/.k) * (b1/.k) by A23,VECTSP_1:def 12
        .= KL1.(b1/.k) * (b1/.k) by A13,A22
        .= (KL1 (#) b1).k by A21,VECTSP_6:def 5;
    end;
    hence Sum(lmlt(d,b1)) = Sum(KL1 (#) b1) by A19,FINSEQ_2:9
      .= Sum KL1 by A16,A12,Th20;
  end;
  hence thesis by A11,Def7;
end;

Lm2: for p be FinSequence, k be set st k in dom p holds len p > 0
proof
  let p be FinSequence, k be set;
  assume k in dom p;
  then p <> {};
  hence thesis;
end;

theorem Th37:
  for a,d be FinSequence of K st len a = len b1
  for j be Nat st j in dom b2 & len d = len b1 &
  for k st k in dom b1 holds d.k = (f.((b1/.k)) |-- b2)/.j holds
    len b1 > 0 implies (Sum(lmlt(a,f*b1)) |-- b2)/.j = Sum(mlt(a,d))
proof
  let a,d be FinSequence of K such that
A1: len a = len b1;
  reconsider B3 = f*b1 as FinSequence of V2;
  deffunc V(Nat,Nat) = ((B3/.$1) |-- b2)/.$2;
  consider M being Matrix of len b1,len b2,the carrier of K such that
A2: for i,j st [i,j] in Indices M holds M*(i,j) = V(i,j) from MATRIX_1:
  sch 1;
  deffunc W(Nat) = Sum mlt(a,Col(M,$1));
  consider dd being FinSequence of K such that
A3: len dd = len b2 & for j be Nat st j in dom dd holds dd/.j = W(j)
  from FINSEQ_4:sch 2;
  let j be Nat such that
A4: j in dom b2;
A5: j in dom dd by A4,A3,FINSEQ_3:29;
  assume that
A6: len d = len b1 and
A7: for k st k in dom b1 holds d.k = (f.(b1/.k) |-- b2)/.j;
A8: len Col(M,j) = len M by MATRIX_1:def 8
    .= len d by A6,MATRIX_1:def 2;
  len M = len b1 by MATRIX_1:def 2;
  then
A9: dom M = dom b1 by FINSEQ_3:29;
A10: len b1 = len B3 by FINSEQ_2:33;
  then
A11: dom b1 = dom B3 by FINSEQ_3:29;
  assume
A12: len b1 > 0;
  then
A13: width M = len b2 by MATRIX_1:23;
A14: now
    let i such that
A15: i in dom B3;
A16: now
      let j be Nat;
      assume
A17:  j in dom ((B3/.i) |-- b2);
      then j in Seg len ((B3/.i) |-- b2) by FINSEQ_1:def 3;
      then
A18:  j in Seg width M by A13,Def7;
      then [i,j] in [:dom M,Seg width M:] by A9,A11,A15,ZFMISC_1:87;
      then
A19:  [i,j] in Indices M by MATRIX_1:def 4;
      thus Line(M,i).j = M*(i,j) by A18,MATRIX_1:def 7
        .= ((B3/.i) |-- b2)/.j by A2,A19
        .= ((B3/.i) |-- b2).j by A17,PARTFUN1:def 6;
    end;
A20: len Line(M,i) = width M by MATRIX_1:def 7
      .= len ((B3/.i) |-- b2) by A13,Def7;
    thus B3/.i = Sum lmlt((B3/.i) |-- b2,b2) by Th35
      .= Sum lmlt(Line(M,i),b2) by A20,A16,FINSEQ_2:9;
  end;
  Seg len b2 = dom b2 by FINSEQ_1:def 3;
  then
A21: j in Seg width M by A4,A12,MATRIX_1:23;
A22: now
    let i be Nat;
    assume i in dom d;
    then
A23: i in dom b1 by A6,FINSEQ_3:29;
    then
A24: B3/.i = B3.i by A11,PARTFUN1:def 6
      .= f.(b1.i) by A23,FUNCT_1:13
      .= f.(b1/.i) by A23,PARTFUN1:def 6;
    [i,j] in [:dom M,Seg width M:] by A9,A21,A23,ZFMISC_1:87;
    then
A25: [i,j] in Indices M by MATRIX_1:def 4;
    thus Col(M,j).i = M*(i,j) by A9,A23,MATRIX_1:def 8
      .= (f.((b1/.i)) |-- b2)/.j by A2,A24,A25
      .= d.i by A7,A23;
  end;
  len b2 > 0 by A4,Lm2;
  hence (Sum(lmlt(a,f*b1)) |-- b2)/.j = (Sum(lmlt(dd,b2)) |-- b2)/.j
  by A1,A12,A3,A10,A14,Th33
    .= dd/.j by A3,Th36
    .= Sum(mlt(a,Col(M,j))) by A3,A5
    .= Sum(mlt(a,d)) by A8,A22,FINSEQ_2:9;
end;

begin :: Matrices of Linear Transformations

definition
  let K be Field;
  let V1,V2 be finite-dimensional VectSp of K;
  let f be Function of V1, V2;
  let b1 be FinSequence of V1;
  let b2 be OrdBasis of V2;
  func AutMt(f,b1,b2) -> Matrix of K means
  :Def8:
  len it = len b1 & for k st k in dom b1 holds it/.k = f.(b1/.k) |-- b2;
  existence
  proof
    deffunc V(Nat) = f.(b1/.$1) |-- b2;
    consider M be FinSequence such that
A1: len M = len b1 and
A2: for k be Nat st k in dom M holds M.k = V(k) from FINSEQ_1:sch 2;
A3: dom M = Seg len b1 by A1,FINSEQ_1:def 3;
    ex n being Nat st for x st x in rng M ex s st s=x & len s = n
    proof
      take n = len(f.(b1/.1) |-- b2);
      let x be set;
      assume x in rng M;
      then consider y such that
A4:   y in dom M and
A5:   x = M.y by FUNCT_1:def 3;
      reconsider y as Nat by A4,FINSEQ_3:23;
      M.y = f.(b1/.y) |-- b2 by A2,A4;
      then reconsider s = M.y as FinSequence;
      take s;
      thus s = x by A5;
      thus len s = len (f.(b1/.y) |-- b2) by A2,A4
        .= len b2 by Def7
        .= n by Def7;
    end;
    then reconsider M as tabular FinSequence by MATRIX_1:def 1;
    now
      let x;
      assume x in rng M;
      then consider y such that
A6:   y in dom M and
A7:   x = M.y by FUNCT_1:def 3;
      reconsider y as Nat by A6,FINSEQ_3:23;
      M.y = f.(b1/.y) |-- b2 by A2,A6;
      then reconsider s = M.y as FinSequence of K;
      s = x by A7;
      hence x in (the carrier of K)* by FINSEQ_1:def 11;
    end;
    then rng M c= (the carrier of K)* by TARSKI:def 3;
    then reconsider M as Matrix of K by FINSEQ_1:def 4;
    take M1 = M;
    for k st k in dom b1 holds M1/.k = f.(b1/.k) |-- b2
    proof
      let k be Nat;
      assume
A8:   k in dom b1;
      then
A9:   k in Seg len b1 by FINSEQ_1:def 3;
      dom M1 = dom b1 by A1,FINSEQ_3:29;
      hence M1/.k = M1.k by A8,PARTFUN1:def 6
        .= f.(b1/.k) |-- b2 by A2,A3,A9;
    end;
    hence thesis by A1;
  end;
  uniqueness
  proof
    let K1,K2 be Matrix of K such that
A10: len K1 = len b1 and
A11: for k st k in dom b1 holds K1/.k = f.(b1/.k) |-- b2 and
A12: len K2 = len b1 and
A13: for k st k in dom b1 holds K2/.k = f.(b1/.k) |-- b2;
    for k be Nat st 1 <= k & k <= len K1 holds K1.k = K2.k
    proof
      let k be Nat;
      assume
A14:  1 <= k & k <= len K1;
      then
A15:  k in dom b1 by A10,FINSEQ_3:25;
A16:  k in dom K2 by A10,A12,A14,FINSEQ_3:25;
      k in dom K1 by A14,FINSEQ_3:25;
      hence K1.k = K1/.k by PARTFUN1:def 6
        .= f.(b1/.k) |-- b2 by A11,A15
        .= K2/.k by A13,A15
        .=K2.k by A16,PARTFUN1:def 6;
    end;
    hence thesis by A10,A12,FINSEQ_1:14;
  end;
end;

Lm3: dom AutMt(f,b1,b2) = dom b1
proof
  len AutMt(f,b1,b2) = len b1 by Def8;
  hence thesis by FINSEQ_3:29;
end;

theorem Th38:
  len b1 = 0 implies AutMt(f,b1,b2) = {}
proof
  assume len b1 = 0;
  then len AutMt(f,b1,b2) = 0 by Def8;
  hence thesis;
end;

theorem Th39:
  len b1 > 0 implies width AutMt(f,b1,b2) = len b2
proof
  assume len b1 > 0;
  then len AutMt(f,b1,b2) > 0 by Def8;
  then consider s being FinSequence such that
A1: s in rng AutMt(f,b1,b2) and
A2: len s = width AutMt(f,b1,b2) by MATRIX_1:def 3;
  consider i be Nat such that
A3: i in dom AutMt(f,b1,b2) and
A4: AutMt(f,b1,b2).i = s by A1,FINSEQ_2:10;
  len AutMt(f,b1,b2) = len b1 by Def8;
  then
A5: i in dom b1 by A3,FINSEQ_3:29;
  s = (AutMt(f,b1,b2))/.i by A3,A4,PARTFUN1:def 6
    .= f.(b1/.i) |-- b2 by A5,Def8;
  hence thesis by A2,Def7;
end;

theorem
  f1 is additive homogeneous & f2 is additive homogeneous &
   AutMt(f1,b1,b2) = AutMt(f2,b1,b2) & len b1 > 0 implies f1 = f2
proof
  assume that
A1: f1 is additive homogeneous & f2 is additive homogeneous and
A2: AutMt(f1,b1,b2) = AutMt(f2,b1,b2) and
A3: len b1 > 0;
  rng b1 is Basis of V1 by Def2;
  then
A4: rng b1 c= the carrier of V1;
  then
A5: rng b1 c= dom f2 by FUNCT_2:def 1;
  rng b1 c= dom f1 by A4,FUNCT_2:def 1;
  then
A6: dom (f1*b1) = dom b1 by RELAT_1:27
    .= dom (f2*b1) by A5,RELAT_1:27;
  now
    let x be set;
    assume
A7: x in dom (f1*b1);
    then reconsider k=x as Nat by FINSEQ_3:23;
A8: dom (f1*b1) c= dom b1 by RELAT_1:25;
    then
A9: f1.(b1/.k) |-- b2 = (AutMt(f2,b1,b2))/.k by A2,A7,Def8
      .= f2.(b1/.k) |-- b2 by A7,A8,Def8;
    thus (f1*b1).x = f1.(b1.x) by A7,FUNCT_1:12
      .= f1.(b1/.x) by A7,A8,PARTFUN1:def 6
      .= f2.(b1/.x) by A9,Th34
      .= f2.(b1.x) by A7,A8,PARTFUN1:def 6
      .= (f2*b1).x by A6,A7,FUNCT_1:12;
  end;
  hence thesis by A1,A3,A6,Th22,FUNCT_1:2;
end;

theorem
  g is additive homogeneous & len b1 > 0 & len b2 > 0 implies
   AutMt(g*f,b1,b3) = AutMt(f,b1,b2) * AutMt(g,b2,b3)
proof
  assume
A1: g is additive homogeneous;
  assume that
A2: len b1 > 0 and
A3: len b2 > 0;
A4: width AutMt(f,b1,b2) = len b2 by A2,Th39
    .= len AutMt(g,b2,b3) by Def8;
A5: width AutMt(g*f,b1,b3) = len b3 by A2,Th39
    .= width AutMt(g,b2,b3) by A3,Th39;
  then
A6: width AutMt(g*f,b1,b3) = width (AutMt(f,b1,b2) * AutMt(g,b2,b3)) by A4,
MATRIX_3:def 4;
A7: len AutMt(g*f,b1,b3) = len b1 by Def8
    .= len AutMt(f,b1,b2) by Def8
    .= len (AutMt(f,b1,b2) * AutMt(g,b2,b3)) by A4,MATRIX_3:def 4;
  then
A8: dom AutMt(g*f,b1,b3) = dom (AutMt(f,b1,b2) * AutMt(g,b2,b3)) by FINSEQ_3:29
;
  for i,j st [i,j] in Indices AutMt(g*f,b1,b3) holds AutMt(g*f,b1,b3)*(i,j
  ) = (AutMt(f,b1,b2) * AutMt(g,b2,b3))*(i,j)
  proof
    let i,j;
    deffunc V(Nat) = (g.((b2/.$1)) |-- b3)/.j;
    consider d be FinSequence of K such that
A9: len d = len b2 & for k be Nat st k in dom d holds d.k = V(k) from
    FINSEQ_2:sch 1;
    assume
A10: [i,j] in Indices AutMt(g*f,b1,b3);
    then
A11: [i,j] in [:dom AutMt(g*f,b1,b3), Seg width AutMt(g*f,b1,b3):] by
MATRIX_1:def 4;
    then
A12: j in Seg width AutMt(g*f,b1,b3) by ZFMISC_1:87;
A13: len Col(AutMt(g,b2,b3),j) = len AutMt(g,b2,b3) by MATRIX_1:def 8
      .= len d by A9,Def8;
A14: dom d = Seg len b2 by A9,FINSEQ_1:def 3;
A15: [i,j] in Indices (AutMt(f,b1,b2) * AutMt(g,b2,b3)) by A8,A6,A11,
MATRIX_1:def 4;
A16: i in dom AutMt(g*f,b1,b3) by A11,ZFMISC_1:87;
A17:  width AutMt(g*f,b1,b3) <> {} by A12;
    len b1 = len AutMt(g*f,b1,b3) by Def8;
    then len b1 > 0 by A17,MATRIX_1:def 3;
    then
A18: j in Seg len b3 by A12,Th39;
    then
A19: j in dom b3 by FINSEQ_1:def 3;
A20: now
      let k be Nat;
      assume
A21:  1 <=k & k <= len d;
      then
A22:  k in dom d by FINSEQ_3:25;
A23:  k in dom b2 by A9,A21,FINSEQ_3:25;
A24:  len AutMt(g,b2,b3) = len b2 by Def8;
      then
A25:  k in dom AutMt(g,b2,b3) by A9,A21,FINSEQ_3:25;
      j in Seg width AutMt(g,b2,b3) by A5,A11,ZFMISC_1:87;
      then
[k,j] in [:dom AutMt(g,b2,b3),Seg width AutMt(g,b2,b3):] by A25,ZFMISC_1:87;
      then [k,j] in Indices AutMt(g,b2,b3) by MATRIX_1:def 4;
      then consider p2 be FinSequence of K such that
A26:  p2= AutMt(g,b2,b3).k and
A27:  AutMt(g,b2,b3)*(k,j) = p2.j by MATRIX_1:def 5;
A28:  p2 = (AutMt(g,b2,b3))/.k by A25,A26,PARTFUN1:def 6
        .= g.(b2/.k) |-- b3 by A23,Def8;
      then j in Seg len p2 by A18,Def7;
      then
A29:  j in dom p2 by FINSEQ_1:def 3;
      k in dom AutMt(g,b2,b3) by A9,A21,A24,FINSEQ_3:25;
      hence Col(AutMt(g,b2,b3),j).k = p2.j by A27,MATRIX_1:def 8
        .= (g.(b2/.k) |-- b3)/.j by A28,A29,PARTFUN1:def 6
        .= d.k by A9,A22;
    end;
    b1/.i in the carrier of V1;
    then
A30: b1/.i in dom f by FUNCT_2:def 1;
    consider p1 be FinSequence of K such that
A31: p1 = AutMt(g*f,b1,b3).i and
A32: AutMt(g*f,b1,b3)*(i,j) = p1.j by A10,MATRIX_1:def 5;
A33: len (f.(b1/.i) |-- b2) = len b2 by Def7;
A34: len AutMt(g*f,b1,b3) = len b1 by Def8;
    then
A35: i in dom b1 by A16,FINSEQ_3:29;
A36: p1 = (AutMt(g*f,b1,b3))/.i by A16,A31,PARTFUN1:def 6
      .= (g*f).(b1/.i) |-- b3 by A35,Def8;
    len AutMt(f,b1,b2) = len b1 by Def8;
    then
A37: i in dom AutMt(f,b1,b2) by A16,A34,FINSEQ_3:29;
    then
A38: Line(AutMt(f,b1,b2),i) = AutMt(f,b1,b2).i by MATRIX_2:16
      .= (AutMt(f,b1,b2))/.i by A37,PARTFUN1:def 6
      .= f.(b1/.i) |-- b2 by A35,Def8;
A39: Seg len b2 = dom b2 by FINSEQ_1:def 3;
    j in Seg len ((g*f).(b1/.i) |-- b3) by A18,Def7;
    then j in dom p1 by A36,FINSEQ_1:def 3;
    hence AutMt(g*f,b1,b3)*(i,j) = ((g*f).(b1/.i) |-- b3)/.j by A32,A36,
PARTFUN1:def 6
      .= (g.(f.(b1/.i)) |-- b3)/.j by A30,FUNCT_1:13
      .= (g.Sum(lmlt(f.(b1/.i) |-- b2,b2)) |-- b3)/.j by Th35
      .= (Sum(lmlt(f.(b1/.i) |-- b2,g*b2)) |-- b3)/.j by A1,A33,Th18
      .= Sum(mlt(f.(b1/.i) |-- b2,d)) by A3,A19,A9,A14,A39,A33,Th37
      .= Line(AutMt(f,b1,b2),i) "*" Col(AutMt(g,b2,b3),j) by A38,A13,A20,
FINSEQ_1:14
      .= (AutMt(f,b1,b2) * AutMt(g,b2,b3))*(i,j) by A4,A15,MATRIX_3:def 4;
  end;
  hence thesis by A7,A6,MATRIX_1:21;
end;

theorem
  AutMt(f1+f2,b1,b2) = AutMt(f1,b1,b2) + AutMt(f2,b1,b2)
proof
A1: len AutMt(f1+f2,b1,b2) = len b1 by Def8
    .= len AutMt(f1,b1,b2) by Def8;
  then
A2: dom AutMt(f1+f2,b1,b2) = dom AutMt(f1,b1,b2) by FINSEQ_3:29;
A3: width AutMt(f1,b1,b2) = width AutMt(f2,b1,b2)
  proof
    per cases;
    suppose
A4:   len b1 = 0;
      then AutMt(f1,b1,b2) = {} by Th38
        .= AutMt(f2,b1,b2) by A4,Th38;
      hence thesis;
    end;
    suppose
A5:   len b1 > 0;
      hence width AutMt(f1,b1,b2) = len b2 by Th39
        .= width AutMt(f2,b1,b2) by A5,Th39;
    end;
  end;
A6: width AutMt(f1+f2,b1,b2) = width AutMt(f1,b1,b2)
  proof
    per cases;
    suppose
A7:   len b1 = 0;
      then AutMt(f1+f2,b1,b2) = {} by Th38
        .= AutMt(f1,b1,b2) by A7,Th38;
      hence thesis;
    end;
    suppose
A8:   len b1 > 0;
      hence width AutMt(f1+f2,b1,b2) = len b2 by Th39
        .= width AutMt(f1,b1,b2) by A8,Th39;
    end;
  end;
  then
A9: width AutMt(f1+f2,b1,b2) = width (AutMt(f1,b1,b2) + AutMt(f2,b1,b2) )
  by MATRIX_3:def 3;
  len AutMt(f1,b1,b2) = len b1 by Def8
    .= len AutMt(f2,b1,b2) by Def8;
  then
A10: dom AutMt(f1,b1,b2) = dom AutMt(f2,b1,b2) by FINSEQ_3:29;
A11: for i,j st [i,j] in Indices AutMt(f1+f2,b1,b2) holds AutMt(f1+f2,b1,b2)
  *(i,j) = (AutMt(f1,b1,b2) + AutMt(f2,b1,b2))*(i,j)
  proof
    let i,j;
    assume
A12: [i,j] in Indices AutMt(f1+f2,b1,b2);
    then
A13: [i,j] in [:dom AutMt(f1+f2,b1,b2), Seg width AutMt(f1+f2,b1,b2):] by
MATRIX_1:def 4;
    then
A14: [i,j] in Indices AutMt(f1,b1,b2) by A2,A6,MATRIX_1:def 4;
A15: [i,j] in Indices AutMt(f2,b1,b2) by A10,A3,A2,A6,A13,MATRIX_1:def 4;
    AutMt(f1+f2,b1,b2)*(i,j) = AutMt(f1,b1,b2)*(i,j)+AutMt(f2,b1,b2)*(i,j )
    proof
      consider KL3 be Linear_Combination of V2 such that
A16:  f2.(b1/.i) = Sum(KL3) & Carrier KL3 c= rng b2 and
A17:  for t st 1<=t & t<=len (f2.(b1/.i) |-- b2) holds (f2.(b1/.i) |-- b2
      )/.t=KL3.(b2/.t) by Def7;
      consider KL2 be Linear_Combination of V2 such that
A18:  f1.(b1/.i) = Sum(KL2) & Carrier KL2 c= rng b2 and
A19:  for t st 1<=t & t<=len (f1.(b1/.i) |-- b2) holds (f1.(b1/.i) |-- b2
      )/.t=KL2.(b2/.t) by Def7;
A20:  i in dom AutMt(f1+f2,b1,b2) by A13,ZFMISC_1:87;
      then
A21:  i in dom b1 by Lm3;
      reconsider b4 = rng b2 as Basis of V2 by Def2;
      consider p1 be FinSequence of K such that
A22:  p1 = AutMt(f1+f2,b1,b2).i and
A23:  AutMt(f1+f2,b1,b2)*(i,j) = p1.j by A12,MATRIX_1:def 5;
      consider KL1 be Linear_Combination of V2 such that
A24:  (f1+f2).(b1/.i) = Sum(KL1) & Carrier KL1 c= rng b2 and
A25:  for t st 1<=t & t<=len ((f1+f2).(b1/.i) |-- b2) holds ((f1+f2).(
      b1/.i) |-- b2)/.t=KL1.(b2/.t) by Def7;
      b4 is linearly-independent & (f1+f2).(b1/.i) = f1.(b1/.i) + f2.(b1
      /.i) by Def3,VECTSP_7:def 3;
      then
A26:  KL1.(b2/.j) = (KL2 + KL3).(b2/.j) by A24,A18,A16,Th6
        .= KL2.(b2/.j) + KL3.(b2/.j) by VECTSP_6:22;
A27:  p1 = (AutMt(f1+f2,b1,b2))/.i by A22,A20,PARTFUN1:def 6
        .= (f1+f2).(b1/.i) |-- b2 by A21,Def8;
      consider p3 be FinSequence of K such that
A28:  p3 = (AutMt(f2,b1,b2)).i and
A29:  AutMt(f2,b1,b2)*(i,j) = p3.j by A15,MATRIX_1:def 5;
      consider p2 be FinSequence of K such that
A30:  p2 = (AutMt(f1,b1,b2)).i and
A31:  AutMt(f1,b1,b2)*(i,j) = p2.j by A14,MATRIX_1:def 5;
A32:  j in Seg width AutMt(f1+f2,b1,b2) by A13,ZFMISC_1:87;
then A33:  1<=j by FINSEQ_1:1;
      len b1 = len AutMt(f1+f2,b1,b2) by Def8;
      then dom b1 = dom AutMt(f1+f2,b1,b2) by FINSEQ_3:29;
      then dom b1 <> {} by A13,ZFMISC_1:87;
      then Seg len b1 <> {} by FINSEQ_1:def 3;
      then len b1 > 0;
      then
A34:  j in Seg len b2 by A32,Th39;
      then
A35:  j<=len b2 by FINSEQ_1:1;
      then j<=len ((f1+f2).(b1/.i) |-- b2) by Def7;
      then
A36:  p1/.j = KL1.(b2/.j) by A33,A27,A25;
A37:  j in dom b2 by A34,FINSEQ_1:def 3;
      i in dom AutMt(f2,b1,b2) by A21,Lm3;
      then
A38:  p3 = AutMt(f2,b1,b2)/.i by A28,PARTFUN1:def 6
        .= f2.(b1/.i) |-- b2 by A21,Def8;
      then j in dom p3 by A37,Lm1;
      then
A39:  AutMt(f2,b1,b2)*(i,j) = p3/.j by A29,PARTFUN1:def 6;
      i in dom AutMt(f1,b1,b2) by A21,Lm3;
      then
A40:  p2 = (AutMt(f1,b1,b2))/.i by A30,PARTFUN1:def 6
        .= f1.(b1/.i) |-- b2 by A21,Def8;
      then j in dom p2 by A37,Lm1;
      then
A41:  AutMt(f1,b1,b2)*(i,j) = p2/.j by A31,PARTFUN1:def 6;
      j<=len (f2.(b1/.i) |-- b2) by A35,Def7;
      then
A42:  p3/.j = KL3.(b2/.j) by A33,A38,A17;
      j<=len (f1.(b1/.i) |-- b2) by A35,Def7;
      then
A43:  p2/.j = KL2.(b2/.j) by A33,A40,A19;
      j in dom p1 by A37,A27,Lm1;
      hence thesis by A23,A41,A39,A36,A43,A42,A26,PARTFUN1:def 6;
    end;
    hence thesis by A14,MATRIX_3:def 3;
  end;
  len AutMt(f1+f2,b1,b2) = len (AutMt(f1,b1,b2) + AutMt(f2,b1,b2)) by A1,
MATRIX_3:def 3;
  hence thesis by A9,A11,MATRIX_1:21;
end;

theorem
  a <> 0.K implies AutMt(a*f,b1,b2) = a * AutMt(f,b1,b2)
proof
  assume
A1: a <> 0.K;
A2: width AutMt(a*f,b1,b2) = width AutMt(f,b1,b2)
  proof
    per cases;
    suppose
A3:   len b1 = 0;
      then AutMt(a*f,b1,b2) = {} by Th38
        .= AutMt(f,b1,b2) by A3,Th38;
      hence thesis;
    end;
    suppose
A4:   len b1 > 0;
      hence width AutMt(a*f,b1,b2) = len b2 by Th39
        .= width AutMt(f,b1,b2) by A4,Th39;
    end;
  end;
  then
A5: width AutMt(a*f,b1,b2) = width (a * AutMt(f,b1,b2)) by MATRIX_3:def 5;
A6: len AutMt(a*f,b1,b2) = len b1 by Def8
    .= len AutMt(f,b1,b2) by Def8;
  then
A7: dom AutMt(a*f,b1,b2) = dom AutMt(f,b1,b2) by FINSEQ_3:29;
A8: for i,j st [i,j] in Indices AutMt(a*f,b1,b2) holds AutMt(a*f,b1,b2)*(i,
  j) = (a * AutMt(f,b1,b2))*(i,j)
  proof
    let i,j;
    assume
A9: [i,j] in Indices AutMt(a*f,b1,b2);
    then
A10: [i,j] in [:dom AutMt(a*f,b1,b2),Seg width AutMt(a*f,b1,b2):] by
MATRIX_1:def 4;
    then
A11: [i,j] in Indices AutMt(f,b1,b2) by A7,A2,MATRIX_1:def 4;
    AutMt(a*f,b1,b2)*(i,j) = a * (AutMt(f,b1,b2)*(i,j))
    proof
      consider p2 be FinSequence of K such that
A12:  p2 = (AutMt(f,b1,b2)).i and
A13:  AutMt(f,b1,b2)*(i,j) = p2.j by A11,MATRIX_1:def 5;
A14:  i in dom AutMt(a*f,b1,b2) by A10,ZFMISC_1:87;
      then
A15:  i in dom b1 by Lm3;
      then i in dom AutMt(f,b1,b2) by Lm3;
      then
A16:  p2 = (AutMt(f,b1,b2))/.i by A12,PARTFUN1:def 6
        .= f.(b1/.i) |-- b2 by A15,Def8;
      reconsider b4 = rng b2 as Basis of V2 by Def2;
      consider p1 be FinSequence of K such that
A17:  p1 = AutMt(a*f,b1,b2).i and
A18:  AutMt(a*f,b1,b2)*(i,j) = p1.j by A9,MATRIX_1:def 5;
      consider KL1 be Linear_Combination of V2 such that
A19:  (a*f).(b1/.i) = Sum(KL1) & Carrier KL1 c= rng b2 and
A20:  for t st 1<=t & t<=len ((a*f).(b1/.i) |-- b2) holds ((a*f).(b1/.i)
      |-- b2)/.t=KL1.(b2/.t) by Def7;
      consider KL2 be Linear_Combination of V2 such that
A21:  f.(b1/.i) = Sum(KL2) & Carrier KL2 c= rng b2 and
A22:  for t st 1<=t & t<=len (f.(b1/.i) |-- b2) holds (f.(b1/.i) |-- b2)
      /.t= KL2.(b2/.t) by Def7;
      b4 is linearly-independent & (a*f).(b1/.i) = a * (f.(b1/.i)) by Def4,
VECTSP_7:def 3;
      then
A23:  KL1.(b2/.j) = (a * KL2).(b2/.j) by A1,A19,A21,Th7
        .= a * KL2.(b2/.j) by VECTSP_6:def 9;
A24:  j in Seg width AutMt(a*f,b1,b2) by A10,ZFMISC_1:87;
      then
A25:  1<=j by FINSEQ_1:1;
      len b1 = len AutMt(a*f,b1,b2) by Def8;
      then dom b1 = dom AutMt(a*f,b1,b2) by FINSEQ_3:29;
      then dom b1 <> {} by A10,ZFMISC_1:87;
      then Seg len b1 <> {} by FINSEQ_1:def 3;
      then len b1 > 0;
      then
A26:  j in Seg len b2 by A24,Th39;
      then
A27:  j<=len b2 by FINSEQ_1:1;
      then j<=len (f.(b1/.i) |-- b2) by Def7;
      then
A28:  p2/.j = KL2.(b2/.j) by A25,A16,A22;
A29:  j in dom b2 by A26,FINSEQ_1:def 3;
      then j in dom (f.(b1/.i) |-- b2) by Lm1;
      then
A30:  AutMt(f,b1,b2)*(i,j) = p2/.j by A13,A16,PARTFUN1:def 6;
A31:  p1 = (AutMt(a*f,b1,b2))/.i by A17,A14,PARTFUN1:def 6
        .= (a*f).(b1/.i) |-- b2 by A15,Def8;
      then
A32:  j in dom p1 by A29,Lm1;
      j<=len ((a*f).(b1/.i) |-- b2) by A27,Def7;
      then p1/.j = KL1.(b2/.j) by A25,A31,A20;
      hence thesis by A18,A32,A30,A28,A23,PARTFUN1:def 6;
    end;
    hence thesis by A11,MATRIX_3:def 5;
  end;
  len AutMt(a*f,b1,b2) = len (a * AutMt(f,b1,b2)) by A6,MATRIX_3:def 5;
  hence thesis by A5,A8,MATRIX_1:21;
end;