:: The Rank+Nullity Theorem
::  by Jesse Alama
::
:: Received July 31, 2007
:: Copyright (c) 2007-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies FUNCT_1, RELAT_1, TARSKI, STRUCT_0, SUBSET_1, XBOOLE_0, VECTSP_1,
      RLVECT_5, FINSET_1, RLVECT_3, LOPBAN_1, ARYTM_3, SUPINF_2, CARD_1,
      RLSUB_1, FUNCT_2, ARYTM_1, MESFUNC1, VECTSP10, RLVECT_2, FUNCT_4,
      REALSET1, FUNCOP_1, QC_LANG1, CARD_3, RLSUB_2, FINSEQ_1, VALUED_1, NAT_1,
      XXREAL_0, PARTFUN1, NUMBERS, PBOOLE, RANKNULL, MSSUBFAM, UNIALG_1;
 notations TARSKI, XBOOLE_0, SUBSET_1, DOMAIN_1, RELAT_1, RELSET_1, FUNCT_1,
      ORDINAL1, NAT_1, NUMBERS, FUNCOP_1, PARTFUN1, FUNCT_2, FUNCT_4, XCMPLX_0,
      XXREAL_0, CARD_1, FINSET_1, FINSEQ_1, FINSEQOP, STRUCT_0, RLVECT_1,
      RLVECT_2, VECTSP_1, FUNCT_7, VECTSP_4, VECTSP_5, VECTSP_6, VECTSP_7,
      MOD_2, MATRLIN, VECTSP_9, LOPBAN_1;
 constructors NAT_1, FINSEQOP, HAHNBAN, VECTSP_6, VECTSP_7, MOD_2, VECTSP_9,
      REALSET1, RLVECT_2, WELLORD2, LOPBAN_1, VECTSP_5, FUNCT_7, FUNCT_4,
      XXREAL_0, MATRLIN, RELSET_1;
 registrations RELAT_1, FUNCT_1, STRUCT_0, CARD_1, FINSET_1, VECTSP_9,
      XBOOLE_0, MATRLIN, FUNCOP_1, ORDINAL1, XREAL_0, SUBSET_1, FINSEQ_1,
      MOD_2, GRCAT_1, RELSET_1;
 requirements BOOLE, SUBSET, NUMERALS, ARITHM;
 definitions TARSKI, RELAT_1, FUNCT_1, FINSEQ_1, VECTSP_4, VECTSP_6, XBOOLE_0,
      RLVECT_1, STRUCT_0, MOD_2, MATRLIN, FUNCOP_1, LOPBAN_1, FUNCT_2;
 theorems TARSKI, ZFMISC_1, RELAT_1, FINSET_1, FINSEQ_1, FUNCT_1, VECTSP_7,
      VECTSP_9, CARD_2, XBOOLE_1, FUNCT_2, SUBSET_1, XBOOLE_0, VECTSP_1,
      RLVECT_1, VECTSP_4, VECTSP_6, STRUCT_0, RLVECT_2, MOD_2, MATRLIN, CARD_1,
      FUNCOP_1, VECTSP_5, FUNCT_7, FINSEQ_2, FUNCT_4, ENUMSET1, ORDINAL1,
      PARTFUN1;
 schemes CLASSES1;

begin

theorem Th1:
  for f,g being Function st g is one-to-one & f|(rng g) is
  one-to-one & rng g c= dom f holds f*g is one-to-one
proof
  let f,g be Function such that
A1: g is one-to-one and
A2: f|(rng g) is one-to-one and
A3: rng g c= dom f;
  set h = f*g;
A4: dom h c= dom g
  proof
    let x be set;
    assume x in dom h;
    hence thesis by FUNCT_1:11;
  end;
  dom g c= dom h
  proof
    let x be set such that
A5: x in dom g;
    g.x in rng g by A5,FUNCT_1:3;
    hence thesis by A3,A5,FUNCT_1:11;
  end;
  then
A6: dom h = dom g by A4,XBOOLE_0:def 10;
  for x1,x2 being set st x1 in dom h & x2 in dom h & h.x1 = h.x2 holds x1 = x2
  proof
    let x1,x2 be set such that
A7: x1 in dom h and
A8: x2 in dom h and
A9: h.x1 = h.x2;
A10: h.x1 = f.(g.x1) & h.x2 = f.(g.x2) by A7,A8,FUNCT_1:12;
    dom (f|(rng g)) = rng g by A3,RELAT_1:62;
    then
A11: g.x1 in dom (f|(rng g)) by A4,A7,FUNCT_1:3;
    g.x2 in rng g by A4,A8,FUNCT_1:3;
    then
A12: g.x2 in dom (f|(rng g)) by A3,RELAT_1:62;
    f.(g.x1) = (f|(rng g)).(g.x1) & f.(g.x2) = (f|(rng g)).(g.x2) by A6,A7,A8,
FUNCT_1:3,49;
    then g.x1 = g.x2 by A2,A9,A10,A11,A12,FUNCT_1:def 4;
    hence thesis by A1,A4,A7,A8,FUNCT_1:def 4;
  end;
  hence thesis by FUNCT_1:def 4;
end;

:: If a function is one-to-one on a set X, then it is one-to-one on
:: any subset of X.

theorem Th2:
  for f being Function, X,Y being set st X c= Y & f|Y is one-to-one
  holds f|X is one-to-one
proof
  let f be Function, X,Y be set such that
A1: X c= Y and
A2: f|Y is one-to-one;
  f|X = (f|Y)|X by A1,RELAT_1:74;
  hence thesis by A2,FUNCT_1:52;
end;

theorem Th3:
  for V being 1-sorted, X,Y being Subset of V holds X meets Y iff
  ex v being Element of V st v in X & v in Y
proof
  let V be 1-sorted, X,Y be Subset of V;
  X meets Y implies ex v being Element of V st v in X & v in Y
  proof
    assume X meets Y;
    then consider z being set such that
A1: z in X and
A2: z in Y by XBOOLE_0:3;
    reconsider v = z as Element of V by A1;
    take v;
    thus thesis by A1,A2;
  end;
  hence thesis by XBOOLE_0:3;
end;

reserve F for Field,
  V,W for VectSp of F;

registration
  let F be Field, V be finite-dimensional VectSp of F;
  cluster finite for Basis of V;
  existence
  proof
    consider A being finite Subset of V such that
A1: A is Basis of V by MATRLIN:def 1;
    reconsider A as Basis of V by A1;
    take A;
    thus thesis;
  end;
end;

registration
  let F be Field, V,W be VectSp of F;
  cluster additive homogeneous for Function of V,W;
  existence
  proof
    set f = FuncZero ([#]V,W);
    reconsider f as Function of V,W;
A1: for x,y being Vector of V holds f.(x+y) = (f.x)+(f.y)
    proof
      let x,y be Vector of V;
A2:   f.y = 0.W by FUNCOP_1:7;
      f.(x+y) = 0.W & f.x = 0.W by FUNCOP_1:7;
      hence thesis by A2,RLVECT_1:def 4;
    end;
    take f;
    for a being Element of F, x being Element of V holds f.(a*x) = a*(f.x)
    proof
      let a be Element of F, x be Element of V;
      f.(a*x) = 0.W & f.x = 0.W by FUNCOP_1:7;
      hence thesis by VECTSP_1:14;
    end;
    hence f is additive homogeneous by A1,VECTSP_1:def 20,MOD_2:def 2;
  end;
end;

theorem Th4:
  [#]V is finite implies V is finite-dimensional
proof
  set B = the Basis of V;
  assume [#]V is finite;
  then reconsider B as finite Subset of V;
  take B;
  thus thesis;
end;

theorem
  for V being finite-dimensional VectSp of F st card ([#]V) = 1 holds dim V = 0
proof
  let V be finite-dimensional VectSp of F such that
A1: card ([#]V) = 1;
  [#]V = {0.V}
  proof
    ex y being set st [#]V = {y} by A1,CARD_2:42;
    hence thesis by TARSKI:def 1;
  end;
  then (Omega).V = (0).V by VECTSP_4:def 3;
  hence thesis by VECTSP_9:29;
end;

theorem
  card ([#]V) = 2 implies dim V = 1
proof
  assume
A1: card ([#]V) = 2;
  then
A2: [#]V is finite;
  reconsider C = [#]V as finite set by A1;
  reconsider V as finite-dimensional VectSp of F by A2,Th4;
  ex v being Vector of V st v <> 0.V & (Omega).V = Lin ({v})
  proof
    consider x,y being set such that
A3: x <> y and
A4: [#]V = {x,y} by A1,CARD_2:60;
    per cases by A4,TARSKI:def 2;
    suppose
A5:   x = 0.V;
      then reconsider x as Element of V;
      reconsider y as Element of V by A4,TARSKI:def 2;
      set L = Lin ({y});
      take y;
      for v being Element of V holds v in (Omega).V iff v in L
      proof
        let v be Element of V;
        v in (Omega).V implies v in L
        proof
          assume v in (Omega).V;
A6:       y in {y} by TARSKI:def 1;
A7:       0.L in L by STRUCT_0:def 5;
          per cases by A4,TARSKI:def 2;
          suppose
            v = x;
            hence thesis by A5,A7,VECTSP_4:def 2;
          end;
          suppose
            v = y;
            hence thesis by A6,VECTSP_7:8;
          end;
        end;
        hence thesis by STRUCT_0:def 5;
      end;
      hence thesis by A3,A5,VECTSP_4:30;
    end;
    suppose
A8:   y = 0.V;
      reconsider x as Element of V by A4,TARSKI:def 2;
      reconsider y as Element of V by A8;
      set L = Lin ({x});
      take x;
      for v being Element of V holds v in (Omega).V iff v in L
      proof
        let v be Element of V;
        v in (Omega).V implies v in L
        proof
          assume v in (Omega).V;
A9:      x in {x} by TARSKI:def 1;
A10:      0.L in L by STRUCT_0:def 5;
          per cases by A4,TARSKI:def 2;
          suppose
            v = y;
            hence thesis by A8,A10,VECTSP_4:def 2;
          end;
          suppose
            v = x;
            hence thesis by A9,VECTSP_7:8;
          end;
        end;
        hence thesis by STRUCT_0:def 5;
      end;
      hence thesis by A3,A8,VECTSP_4:30;
    end;
  end;
  hence thesis by VECTSP_9:30;
end;

begin :: Basic facts of linear transformations

definition
  let F be Field, V,W be VectSp of F;
  mode linear-transformation of V,W is additive homogeneous Function of V,W;
end;

reserve T for linear-transformation of V,W;

theorem Th7:
  for V, W being non empty 1-sorted, T being Function of V,W holds
  dom T = [#]V & rng T c= [#]W
proof
  let V, W be non empty 1-sorted, T be Function of V,W;
  T is Element of Funcs([#]V,[#]W) by FUNCT_2:8;
  hence thesis by FUNCT_2:92;
end;

theorem Th8:
  for x,y being Element of V holds T.x - T.y = T.(x - y)
proof
  let x,y be Element of V;
A1: T.((-1.F)*y) = (-1.F)*(T.y) by MOD_2:def 2;
  T.(x - y) = T.x + T.(-y) & -y = (-1.F)*y by VECTSP_1:def 20,VECTSP_1:14;
  hence thesis by A1,VECTSP_1:14;
end;

theorem Th9:
  T.(0.V) = 0.W
proof
  0.V = (0.F)*(0.V) by VECTSP_1:14;
  then T.(0.V) = (0.F)*T.(0.V) by MOD_2:def 2
    .= 0.W by VECTSP_1:14;
  hence thesis;
end;

definition
  let F be Field, V,W be VectSp of F, T be linear-transformation of V,W;
  func ker T -> strict Subspace of V means
  :Def1:
  [#]it = { u where u is Element of V : T.u = 0.W };
  existence
  proof
    set K = { u where u is Element of V : T.u = 0.W };
    K c= [#]V
    proof
      let x be set;
      assume x in K;
      then ex u being Element of V st u = x & T.u = 0.W;
      hence thesis;
    end;
    then reconsider K as Subset of V;
A1: for v being Element of V st v in K holds T.v = 0.W
    proof
      let v be Element of V;
      assume v in K;
      then ex u being Element of V st u = v & T.u = 0.W;
      hence thesis;
    end;
    now
      let u be Element of V, a be Element of F;
      assume u in K;
      then T.u = 0.W by A1;
      then T.(a*u) = a*(0.W) by MOD_2:def 2
        .= 0.W by VECTSP_1:14;
      hence a*u in K;
    end;
    then
A2: for a being Element of F, u being Element of V st u in K holds a*u in K;
    T.(0.V) = 0.W by Th9;
    then
A3: 0.V in K;
    now
      let u,v be Element of V;
      assume u in K & v in K;
      then T.u = 0.W & T.v = 0.W by A1;
      then T.(u+v) = 0.W + 0.W by VECTSP_1:def 20
        .= 0.W by RLVECT_1:def 4;
      hence u+v in K;
    end;
    then K is linearly-closed by A2,VECTSP_4:def 1;
    then consider W being strict Subspace of V such that
A4: K = the carrier of W by A3,VECTSP_4:34;
    take W;
    thus thesis by A4;
  end;
  uniqueness by VECTSP_4:29;
end;

theorem Th10:
  for x being Element of V holds x in ker T iff T.x = 0.W
proof
  let x be Element of V;
  thus x in ker T implies T.x = 0.W
  proof
    assume x in ker T;
    then
A1: x in [#]ker T by STRUCT_0:def 5;
    [#]ker T = { u where u is Element of V : T.u = 0.W } by Def1;
    then ex u being Element of V st u = x & T.u = 0.W by A1;
    hence thesis;
  end;
  assume T.x = 0.W;
  then x in { u where u is Element of V : T.u = 0.W };
  then x in [#]ker T by Def1;
  hence thesis by STRUCT_0:def 5;
end;

definition
  let V,W be non empty 1-sorted, T be Function of V,W, X be Subset of V;
  redefine func T .: X -> Subset of W;
  coherence
  proof
    rng T c= [#]W & T .: X c= rng T by Th7,RELAT_1:111;
    hence thesis by XBOOLE_1:1;
  end;
end;

definition
  let F be Field, V,W be VectSp of F, T be linear-transformation of V,W;
  func im T -> strict Subspace of W means
  :Def2:
  [#]it = T .: [#]V;
  existence
  proof
    reconsider U = T .: [#]V as Subset of W;
A1: for u being Element of W holds u in U iff ex v being Element of V st T
    .v = u
    proof
      let u be Element of W;
      thus u in U implies ex v being Element of V st T.v = u
      proof
        assume u in U;
        then consider x being set such that
        x in dom T and
A2:     x in [#]V and
A3:     u = T.x by FUNCT_1:def 6;
        reconsider x as Element of V by A2;
        take x;
        thus thesis by A3;
      end;
      thus (ex v being Element of V st T.v = u) implies u in U
      proof
        given v being Element of V such that
A4:     T.v = u;
        v in [#]V;
        then v in dom T by Th7;
        hence thesis by A4,FUNCT_1:def 6;
      end;
    end;
A5: now
      let u,v be Element of W such that
A6:   u in U and
A7:   v in U;
      consider x being Element of V such that
A8:   T.x = u by A1,A6;
      consider y being Element of V such that
A9:   T.y = v by A1,A7;
      u+v = T.(x+y) by A8,A9,VECTSP_1:def 20;
      hence u+v in U by A1;
    end;
    now
      let a be Element of F, w be Element of W;
      assume w in U;
      then consider v being Element of V such that
A10:  T.v = w by A1;
      T.(a*v) = a*w by A10,MOD_2:def 2;
      hence a*w in U by A1;
    end;
    then
A11: U is linearly-closed by A5,VECTSP_4:def 1;
    T.(0.V) = 0.W by Th9;
    then U <> {} by A1;
    then consider A being strict Subspace of W such that
A12: U = the carrier of A by A11,VECTSP_4:34;
    take A;
    thus thesis by A12;
  end;
  uniqueness by VECTSP_4:29;
end;

theorem
  0.V in ker T
proof
  0.V = (0.F)*(0.V) by VECTSP_1:14;
  then T.(0.V) = (0.F)*T.(0.V) by MOD_2:def 2
    .= 0.W by VECTSP_1:14;
  hence thesis by Th10;
end;

theorem Th12:
  for X being Subset of V holds T .: X is Subset of im T
proof
  let X be Subset of V;
  [#](im T) = T .: [#]V by Def2;
  hence thesis by RELAT_1:123;
end;

theorem Th13:
  for y being Element of W holds y in im T iff ex x being Element
  of V st y = T.x
proof
  let y be Element of W;
A1: y in im T implies ex x being Element of V st y = T.x
  proof
    assume y in im T;
    then reconsider y as Element of im T by STRUCT_0:def 5;
    [#](im T) = T .: [#]V by Def2;
    then consider x being set such that
    x in dom T and
A2: x in [#]V and
A3: y = T.x by FUNCT_1:def 6;
    reconsider x as Element of V by A2;
    take x;
    thus thesis by A3;
  end;
  (ex x being Element of V st y = T.x) implies y in im T
  proof
    assume
A4: ex x being Element of V st y = T.x;
    dom T = [#]V by Th7;
    then y in T .: [#]V by A4,FUNCT_1:def 6;
    then y in [#](im T) by Def2;
    hence thesis by STRUCT_0:def 5;
  end;
  hence thesis by A1;
end;

theorem
  for x being Element of ker T holds T.x = 0.W
proof
  let x be Element of ker T;
  reconsider y = x as Element of V by VECTSP_4:10;
  y in ker T by STRUCT_0:def 5;
  hence thesis by Th10;
end;

theorem Th15:
  T is one-to-one implies ker T = (0).V
proof
  reconsider Z = (0).V as Subspace of ker T by VECTSP_4:39;
  assume
A1: T is one-to-one;
  for v being Element of ker T holds v in Z
  proof
    let v be Element of ker T;
A2: v in ker T by STRUCT_0:def 5;
    assume not v in Z;
    then
A3: not v = 0.V by VECTSP_4:35;
A4: T.(0.V) = 0.W & dom T = [#]V by Th7,Th9;
    reconsider v as Element of V by VECTSP_4:10;
    T.v = 0.W by A2,Th10;
    hence thesis by A1,A3,A4,FUNCT_1:def 4;
  end;
  hence thesis by VECTSP_4:32;
end;

theorem Th16:
  for V being finite-dimensional VectSp of F holds dim ((0).V) = 0
proof
  let V be finite-dimensional VectSp of F;
  (Omega).((0).V) = (0).((0).V) by VECTSP_4:36;
  hence thesis by VECTSP_9:29;
end;

theorem Th17:
  for x,y being Element of V st T.x = T.y holds x - y in ker T
proof
  let x,y be Element of V such that
A1: T.x = T.y;
  T.(x - y) = T.x - T.y by Th8
    .= 0.W by A1,VECTSP_1:19;
  hence thesis by Th10;
end;

theorem Th18:
  for A being Subset of V, x,y being Element of V st x - y in Lin
  A holds x in Lin (A \/ {y})
proof
  let A be Subset of V, x,y be Element of V such that
A1: x - y in Lin A;
A2: Lin (A \/ {y}) = (Lin A) + (Lin {y}) by VECTSP_7:15;
  y in {y} by TARSKI:def 1;
  then
A3: y in Lin ({y}) by VECTSP_7:8;
  (x - y) + y = x - (y - y) by RLVECT_1:29
    .= x - 0.V by VECTSP_1:19
    .= x by RLVECT_1:13;
  hence thesis by A1,A3,A2,VECTSP_5:1;
end;

begin :: Some basic facts about linearly independent subsets and linear
:: combinations

theorem Th19:
  for X being Subset of V st V is Subspace of W holds X is Subset of W
proof
  let X be Subset of V;
  assume V is Subspace of W;
  then
A1: [#]V c= [#]W by VECTSP_4:def 2;
  X c= [#]W
  proof
    let x be set;
    assume x in X;
    then x in [#]V;
    hence thesis by A1;
  end;
  hence thesis;
end;

:: A linearly independent set is a basis of its linear span.

theorem Th20:
  for A being Subset of V st A is linearly-independent holds A is
  Basis of Lin A
proof
  let A be Subset of V such that
A1: A is linearly-independent;
  A c= [#](Lin A)
  proof
    let x be set such that
A2: x in A;
    reconsider x as Element of V by A2;
    x in Lin A by A2,VECTSP_7:8;
    hence thesis by STRUCT_0:def 5;
  end;
  then reconsider B = A as Subset of Lin A;
A3: Lin B = Lin A by VECTSP_9:17;
  B is linearly-independent by A1,VECTSP_9:12;
  hence thesis by A3,VECTSP_7:def 3;
end;

:: Adjoining an element x to A that is already in its linear span
:: results in a linearly dependent set.

theorem Th21:
  for A being Subset of V, x being Element of V st x in Lin A &
  not x in A holds A \/ {x} is linearly-dependent
proof
  let A be Subset of V, x be Element of V such that
A1: x in Lin A and
A2: not x in A;
  per cases;
  suppose
A3: A is linearly-independent;
    x in [#](Lin A) by A1,STRUCT_0:def 5;
    then reconsider X = {x} as Subset of Lin A by SUBSET_1:41;
    reconsider A9 = A as Basis of Lin A by A3,Th20;
    reconsider B = A9 \/ X as Subset of Lin A;
    X misses A9
    proof
      assume X meets A9;
      then ex y being set st y in X & y in A9 by XBOOLE_0:3;
      hence contradiction by A2,TARSKI:def 1;
    end;
    then B is linearly-dependent by VECTSP_9:15;
    hence thesis by VECTSP_9:12;
  end;
  suppose
    A is linearly-dependent;
    hence thesis by VECTSP_7:1,XBOOLE_1:7;
  end;
end;

theorem Th22:
  for A being Subset of V, B being Basis of V st A is Basis of ker
  T & A c= B holds T|(B \ A) is one-to-one
proof
  let A be Subset of V, B be Basis of V such that
A1: A is Basis of ker T and
A2: A c= B;
  reconsider A9 = A as Subset of V;
  set f = T|(B \ A);
  let x1,x2 be set such that
A3: x1 in dom f and
A4: x2 in dom f and
A5: f.x1 = f.x2 and
A6: x1 <> x2;
  x2 in dom T by A4,RELAT_1:57;
  then reconsider x2 as Element of V;
  x1 in dom T by A3,RELAT_1:57;
  then reconsider x1 as Element of V;
A7: x1 in B \ A by A3;
A8: not x1 in (A9 \/ {x2})
  proof
    assume
A9: x1 in A9 \/ {x2};
    per cases by A9,XBOOLE_0:def 3;
    suppose
      x1 in A9;
      hence contradiction by A7,XBOOLE_0:def 5;
    end;
    suppose
      x1 in {x2};
      hence contradiction by A6,TARSKI:def 1;
    end;
  end;
A10: x2 in B \ A by A4;
  then
A11: f.x2 = T.x2 by FUNCT_1:49;
  reconsider A as Basis of ker T by A1;
A12: ker T = Lin A by VECTSP_7:def 3;
  f.x1 = T.x1 by A7,FUNCT_1:49;
  then x1 - x2 in ker T by A5,A11,Th17;
  then x1 - x2 in Lin A9 by A12,VECTSP_9:17;
  then
A13: x1 in Lin (A9 \/ {x2}) by Th18;
  {x2} \/ {x1} = {x1,x2} by ENUMSET1:1;
  then
A14: (A9 \/ {x2}) \/ {x1} = A9 \/ {x1,x2} by XBOOLE_1:4;
  {x1,x2} c= B
  proof
    let z be set such that
A15: z in {x1,x2};
    per cases by A15,TARSKI:def 2;
    suppose
      z = x1;
      hence thesis by A7,XBOOLE_0:def 5;
    end;
    suppose
      z = x2;
      hence thesis by A10,XBOOLE_0:def 5;
    end;
  end;
  then
A16: A9 \/ {x1,x2} c= B by A2,XBOOLE_1:8;
  B is linearly-independent by VECTSP_7:def 3;
  hence thesis by A13,A14,A8,A16,Th21,VECTSP_7:1;
end;

theorem
  for A being Subset of V, l being Linear_Combination of A, x being
Element of V, a being Element of F holds l +* (x,a) is Linear_Combination of A
  \/ {x}
proof
  let A be Subset of V, l be Linear_Combination of A, x be Element of V, a be
  Element of F;
  set m = l +* (x,a);
A1: dom m = [#]V by FUNCT_2:def 1;
  rng m c= [#]F
  proof
    let y be set;
    assume y in rng m;
    then consider x9 being set such that
A2: x9 in dom m and
A3: m.x9 = y by FUNCT_1:def 3;
A4: x9 in dom l by A1,A2,FUNCT_2:92;
    per cases;
    suppose
      x9 = x;
      then m.x9 = a by A4,FUNCT_7:31;
      hence thesis by A3;
    end;
    suppose
A5:   x9 <> x;
A6:   l.x9 in rng l & rng l c= [#]F by A4,FUNCT_1:3,FUNCT_2:92;
      m.x9 = l.x9 by A5,FUNCT_7:32;
      hence thesis by A3,A6;
    end;
  end;
  then reconsider m as Element of Funcs ([#]V,[#]F) by A1,FUNCT_2:def 2;
  set T = Carrier l \/ {x};
  for v being Element of V st not v in T holds m.v = 0.F
  proof
    let v be Element of V such that
A7: not v in T;
    not v in {x} by A7,XBOOLE_0:def 3;
    then v <> x by TARSKI:def 1;
    then
A8: m.v = l.v by FUNCT_7:32;
    not v in Carrier l by A7,XBOOLE_0:def 3;
    hence thesis by A8;
  end;
  then reconsider m as Linear_Combination of V by VECTSP_6:def 1;
A9: Carrier m c= T
  proof
    let y be set;
    assume y in Carrier m;
    then consider z being Element of V such that
A10: y = z and
A11: m.z <> 0.F;
    per cases;
    suppose
A12:  z = x;
      x in {x} & {x} c= T by TARSKI:def 1,XBOOLE_1:7;
      hence thesis by A10,A12;
    end;
    suppose
      z <> x;
      then m.z = l.z by FUNCT_7:32;
      then
A13:  z in Carrier l by A11;
      Carrier l c= T by XBOOLE_1:7;
      hence thesis by A10,A13;
    end;
  end;
  Carrier l c= A by VECTSP_6:def 4;
  then T c= A \/ {x} by XBOOLE_1:9;
  then Carrier m c= A \/ {x} by A9,XBOOLE_1:1;
  hence thesis by VECTSP_6:def 4;
end;

definition
  let V be 1-sorted, X be Subset of V;
  func V \ X -> Subset of V equals
  [#]V \ X;
  coherence;
end;

definition
  let F be Field, V be VectSp of F, l be Linear_Combination of V, X be Subset
  of V;
  redefine func l .: X -> Subset of F;
  coherence
  proof
    l .: X c= [#]F;
    hence thesis;
  end;
end;

reserve l for Linear_Combination of V;

registration
  let F be Field, V be VectSp of F;
  cluster linearly-dependent for Subset of V;
  existence
  proof
    reconsider S = {0.V} as Subset of V;
    take S;
    0.V in S by TARSKI:def 1;
    hence thesis by VECTSP_7:2;
  end;
end;

:: Restricting a linear combination to a given set

definition
  let F be Field, V be VectSp of F, l be Linear_Combination of V, A be Subset
  of V;
  func l!A -> Linear_Combination of A equals
  (l|A) +* ((V \ A) --> 0.F);
  coherence
  proof
    set f = (l|A) +* ((V \ A) --> 0.F);
A1: dom f = dom (l|A) \/ dom ((V \ A) --> 0.F) by FUNCT_4:def 1;
A2: dom ((V \ A) --> 0.F) = V \ A by FUNCOP_1:13;
    dom l = [#]V by FUNCT_2:92;
    then
A3: dom (l|A) = A by RELAT_1:62;
    then
A4: dom f = [#]V by A1,A2,XBOOLE_1:45;
A5: A \/ ([#]V \ A) = [#]V by XBOOLE_1:45;
    rng f c= [#]F
    proof
      let y be set;
      assume y in rng f;
      then consider x being set such that
A6:   x in dom f and
A7:   y = f.x by FUNCT_1:def 3;
      reconsider x as Element of V by A1,A3,A2,A6,XBOOLE_1:45;
      per cases by A5,XBOOLE_0:def 3;
      suppose
A8:     x in A;
        then not x in dom ((V \ A) --> 0.F) by XBOOLE_0:def 5;
        then
A9:     f.x = (l|A).x by FUNCT_4:11;
        (l|A).x = l.x by A8,FUNCT_1:49;
        hence thesis by A7,A9;
      end;
      suppose
A10:    x in V \ A;
        then x in dom ((V \ A) --> 0.F) by FUNCOP_1:13;
        then f.x = ((V \ A) --> 0.F).x by FUNCT_4:13
          .= 0.F by A10,FUNCOP_1:7;
        hence thesis by A7;
      end;
    end;
    then reconsider f as Element of Funcs([#]V,[#]F) by A4,FUNCT_2:def 2;
    ex T being finite Subset of V st for v being Element of V st not v in
    T holds f.v = 0.F
    proof
      set D = { v where v is Element of V : f.v <> 0.F };
      D c= [#]V
      proof
        let x be set;
        assume x in D;
        then ex v being Element of V st x = v & f.v <> 0.F;
        hence thesis;
      end;
      then reconsider D as Subset of V;
      set C = Carrier l;
      D c= C
      proof
        let x be set;
        assume x in D;
        then consider v being Element of V such that
A11:    x = v and
A12:    f.v <> 0.F;
A13:    dom ((V \ A) --> 0.F) = V \ A by FUNCOP_1:13;
A14:    now
          assume
A15:      v in V \ A;
          then f.v = ((V \ A) --> 0.F).v by A1,A4,A13,FUNCT_4:def 1
            .= 0.F by A15,FUNCOP_1:7;
          hence contradiction by A12;
        end;
        then v in A by XBOOLE_0:def 5;
        then
A16:    (l|A).v = l.v by FUNCT_1:49;
        not v in dom ((V \ A) --> 0.F) by A14;
        then f.v = (l|A).v by FUNCT_4:11;
        hence thesis by A11,A12,A16;
      end;
      then reconsider D as finite Subset of V;
      take D;
      thus thesis;
    end;
    then reconsider f as Linear_Combination of V by VECTSP_6:def 1;
    Carrier f c= A
    proof
      let x be set such that
A17:  x in Carrier f;
      reconsider x as Element of V by A17;
A18:  f.x <> 0.F by A17,VECTSP_6:2;
      now
        assume not x in A;
        then
A19:    x in V \ A by XBOOLE_0:def 5;
        then x in dom (l|A) \/ (dom ((V \ A) --> 0.F)) by A2,XBOOLE_0:def 3;
        then f.x = ((V \ A) --> 0.F).x by A2,A19,FUNCT_4:def 1;
        hence contradiction by A18,A19,FUNCOP_1:7;
      end;
      hence thesis;
    end;
    hence thesis by VECTSP_6:def 4;
  end;
end;

theorem Th24:
  l = l!Carrier l
proof
  set f = l|(Carrier l);
  set g = (V \ Carrier l) --> 0.F;
  set m = f +* g;
A1: dom g = V \ (Carrier l) by FUNCOP_1:13;
A2: dom l = [#]V by FUNCT_2:92;
  then dom f = Carrier l by RELAT_1:62;
  then
A3: (dom f) \/ (dom g) = [#]V by A1,XBOOLE_1:45;
A4: for x being set st x in dom l holds l.x = m.x
  proof
    let x be set;
    assume x in dom l;
    then reconsider x as Element of V;
    per cases;
    suppose
A5:   x in Carrier l;
      then not x in dom g by XBOOLE_0:def 5;
      then m.x = f.x by A3,FUNCT_4:def 1;
      hence thesis by A5,FUNCT_1:49;
    end;
    suppose
A6:   not x in Carrier l;
      then x in V \ (Carrier l) by XBOOLE_0:def 5;
      then m.x = g.x & g.x = 0.F by A1,A3,FUNCOP_1:7,FUNCT_4:def 1;
      hence thesis by A6;
    end;
  end;
  dom l = dom m by A2,A3,FUNCT_4:def 1;
  hence thesis by A4,FUNCT_1:def 11;
end;

Lm1: for X being Subset of V holds l .: X is finite
proof
  let X be Subset of V;
A1: l = l!(Carrier l) by Th24;
  (rng (l|Carrier l)) \/ rng ((V \ (Carrier l)) --> 0.F) is finite;
  then rng l is finite by A1,FINSET_1:1,FUNCT_4:17;
  hence thesis by FINSET_1:1,RELAT_1:111;
end;

theorem Th25:
  for A being Subset of V, v being Element of V st v in A holds (l !A).v = l.v
proof
  let A be Subset of V, v be Element of V such that
A1: v in A;
  dom (l!A) = [#]V by FUNCT_2:92;
  then
A2: (dom (l|A)) \/ (dom ((V \ A) --> 0.F)) = [#]V by FUNCT_4:def 1;
  not v in dom ((V \ A) --> 0.F) by A1,XBOOLE_0:def 5;
  then (l!A).v = (l|A).v by A2,FUNCT_4:def 1
    .= l.v by A1,FUNCT_1:49;
  hence thesis;
end;

theorem Th26:
  for A being Subset of V, v being Element of V st not v in A
  holds (l!A).v = 0.F
proof
  let A be Subset of V, v be Element of V;
  assume not v in A;
  then
A1: v in V \ A by XBOOLE_0:def 5;
A2: dom (l!A) = [#]V by FUNCT_2:92;
  dom ((V \ A) --> 0.F) = V \ A & dom (l!A) = (dom (l|A)) \/ (dom ((V \ A)
  --> 0.F)) by FUNCOP_1:13,FUNCT_4:def 1;
  then (l!A).v = ((V \ A) --> 0.F).v by A2,A1,FUNCT_4:def 1
    .= 0.F by A1,FUNCOP_1:7;
  hence thesis;
end;

theorem Th27:
  for A,B being Subset of V, l being Linear_Combination of B st A
  c= B holds l = (l!A) + (l!(B\A))
proof
  let A,B be Subset of V, l be Linear_Combination of B such that
A1: A c= B;
  set r = (l!A) + (l!(B\A));
  let v be Element of V;
A2: v in B implies (v in A or v in B \ A)
  proof
    assume
A3: v in B;
    B = A \/ (B \ A) by A1,XBOOLE_1:45;
    hence thesis by A3,XBOOLE_0:def 3;
  end;
  per cases by A2;
  suppose
A4: v in A;
    then not v in B \ A by XBOOLE_0:def 5;
    then
A5: (l!(B\A)).v = 0.F by Th26;
    (l!A).v = l.v by A4,Th25;
    then r.v = l.v + 0.F by A5,VECTSP_6:22
      .= l.v by RLVECT_1:4;
    hence l.v = r.v;
  end;
  suppose
A6: v in B\A;
    then not v in A by XBOOLE_0:def 5;
    then
A7: (l!A).v = 0.F by Th26;
    (l!(B\A)).v = l.v by A6,Th25;
    then r.v = 0.F + l.v by A7,VECTSP_6:22
      .= l.v by RLVECT_1:4;
    hence l.v = r.v;
  end;
  suppose
A8: not v in B;
    Carrier l c= B by VECTSP_6:def 4;
    then
A9: not v in Carrier l by A8;
    not v in B\A by A8,XBOOLE_0:def 5;
    then
A10: (l!(B\A)).v = 0.F by Th26;
    not v in A by A1,A8;
    then (l!A).v = 0.F by Th26;
    then r.v = 0.F + 0.F by A10,VECTSP_6:22
      .= 0.F by RLVECT_1:4;
    hence l.v = r.v by A9;
  end;
end;

registration
  let F be Field, V be VectSp of F, l be Linear_Combination of V, X be Subset
  of V;
  cluster l .: X -> finite;
  coherence by Lm1;
end;

definition
  let V,W be non empty 1-sorted, T be Function of V,W, X be Subset of W;
  redefine func T"X -> Subset of V;
  coherence
  proof
    dom T = [#]V by Th7;
    hence thesis by RELAT_1:132;
  end;
end;

theorem Th28:
  for X being Subset of V st X misses Carrier l holds l .: X c= { 0.F}
proof
  let X be Subset of V such that
A1: X misses Carrier l;
  set M = l .: X;
  let y be set;
  assume y in M;
  then consider x being set such that
A2: x in dom l and
A3: x in X and
A4: y = l.x by FUNCT_1:def 6;
  reconsider x as Element of V by A2;
  now
    assume l.x <> 0.F;
    then x in Carrier l;
    then x in (Carrier l) /\ X by A3,XBOOLE_0:def 4;
    hence contradiction by A1,XBOOLE_0:def 7;
  end;
  hence thesis by A4,TARSKI:def 1;
end;

:: The image of a linear combination under a linear transformation:
::
::   T(a1*v1 + a2*v2 + ... + an*vn)
::     =  a1*T(v1) + a2*T(v2) + ... + an*T(vn).
::
:: Linear combinations are represented as functions from the space to
:: the underlying field having finite support, so to define a new
:: linear combination it is enough to say what its values are for the
:: elements of W and to prove that its support is finite.
::
:: The only difficulty is that some values T(vi) and T(vj) may be
:: equal.  In this case, the new linear combination should be the sum
:: of the coefficients ai and aj, i.e., l(vi) and l(vj).

definition
  let F be Field, V,W be VectSp of F, l be Linear_Combination of V, T be
  linear-transformation of V,W;
  func T@l -> Linear_Combination of W means
  :Def5:
  for w being Element of W holds it.w = Sum (l .: (T"{w}));
  existence
  proof
    defpred P[set,set] means ex w being Element of W st $1 = w & $2 = Sum (l
    .: (T"{w}));
A1: for x being set st x in [#]W holds ex y being set st P[x,y]
    proof
      let x be set;
      assume x in [#]W;
      then reconsider x as Element of W;
      take Sum (l .: (T"{x}));
      thus thesis;
    end;
    consider f being Function such that
A2: dom f = [#]W and
A3: for x being set st x in [#]W holds P[x,f.x] from CLASSES1:sch 1(A1
    );
A4: rng f c= [#]F
    proof
      let y be set;
      assume y in rng f;
      then consider x being set such that
A5:   x in dom f and
A6:   f.x = y by FUNCT_1:def 3;
      ex w being Element of W st x = w & f.x = Sum (l .: (T"{w} )) by A2,A3,A5;
      hence thesis by A6;
    end;
A7: for w being Element of W holds f.w = Sum (l .: (T"{w}))
    proof
      let w be Element of W;
      ex w9 being Element of W st w = w9 & f.w = Sum (l .: (T"{ w9})) by A3;
      hence thesis;
    end;
    reconsider f as Element of Funcs([#]W,[#]F) by A2,A4,FUNCT_2:def 2;
    ex T being finite Subset of W st for w being Element of W st not w in
    T holds f.w = 0.F
    proof
      set X = { w where w is Element of W : f.w <> 0.F };
      X c= [#]W
      proof
        let x be set;
        assume x in X;
        then ex w being Element of W st x = w & f.w <> 0.F;
        hence thesis;
      end;
      then reconsider X as Subset of W;
      set C = Carrier l;
      reconsider TC = T .: C as Subset of W;
      X c= TC
      proof
        let x be set;
        assume x in X;
        then consider w being Element of W such that
A8:     x = w and
A9:     f.w <> 0.F;
        T"{w} meets Carrier l
        proof
          assume
A10:      T"{w} misses Carrier l;
          then
A11:      l .: T"{w} c= {0.F} by Th28;
          Sum (l .: T"{w}) = 0.F
          proof
            per cases;
            suppose
              l .: T"{w} = {}F;
              hence thesis by RLVECT_2:8;
            end;
            suppose
A12:          l .: T"{w} <> {}F;
A13:          {0.F} c= l .: T"{w}
              proof
                let y be set;
                assume y in {0.F};
                then
A14:            y = 0.F by TARSKI:def 1;
                ex z being set st z in l .: T"{w} by A12,XBOOLE_0:def 1;
                hence thesis by A11,A14,TARSKI:def 1;
              end;
              l .: T"{w} c= {0.F} by A10,Th28;
              then l .: T"{w} = {0.F} by A13,XBOOLE_0:def 10;
              hence thesis by RLVECT_2:9;
            end;
          end;
          hence contradiction by A7,A9;
        end;
        then consider y being set such that
A15:    y in T"{w} and
A16:    y in Carrier l by XBOOLE_0:3;
A17:    dom T = [#]V by Th7;
        reconsider y as Element of V by A16;
        T.y in {w} by A15,FUNCT_1:def 7;
        then T.y = w by TARSKI:def 1;
        hence thesis by A8,A16,A17,FUNCT_1:def 6;
      end;
      then reconsider X as finite Subset of W;
      take X;
      thus thesis;
    end;
    then reconsider f as Linear_Combination of W by VECTSP_6:def 1;
    take f;
    for w being Element of W holds f.w = Sum (l .: (T"{w}))
    proof
      let w be Element of W;
      ex w9 being Element of W st w = w9 & f.w = Sum (l .: (T"{ w9})) by A3;
      hence thesis;
    end;
    hence thesis;
  end;
  uniqueness
  proof
    let f,g be Linear_Combination of W such that
A18: for w being Element of W holds f.w = Sum (l .: (T"{w})) and
A19: for w being Element of W holds g.w = Sum (l .: (T"{w}));
A20: for x being set st x in dom f holds f.x = g.x
    proof
      let x be set;
      assume x in dom f;
      then reconsider x as Element of W;
      f.x = Sum (l .: (T"{x})) by A18;
      hence thesis by A19;
    end;
    dom f = [#]W & dom g = [#]W by FUNCT_2:92;
    hence thesis by A20,FUNCT_1:def 11;
  end;
end;

theorem Th29:
  T@l is Linear_Combination of T .: (Carrier l)
proof
  Carrier (T@l) c= T .: (Carrier l)
  proof
    let w be set such that
A1: w in Carrier (T@l);
    reconsider w as Element of W by A1;
A2: (T@l).w <> 0.F by A1,VECTSP_6:2;
    now
      assume
A3:   T"{w} misses Carrier l;
      then
A4:   l .: T"{w} c= {0.F} by Th28;
      Sum (l .: T"{w}) = 0.F
      proof
        per cases;
        suppose
          l .: T"{w} = {}F;
          hence thesis by RLVECT_2:8;
        end;
        suppose
A5:       l .: T"{w} <> {}F;
A6:       {0.F} c= l .: T"{w}
          proof
            let y be set;
            assume y in {0.F};
            then
A7:         y = 0.F by TARSKI:def 1;
            ex z being set st z in l .: T"{w} by A5,XBOOLE_0:def 1;
            hence thesis by A4,A7,TARSKI:def 1;
          end;
          l .: T"{w} c= {0.F} by A3,Th28;
          then l .: T"{w} = {0.F} by A6,XBOOLE_0:def 10;
          hence thesis by RLVECT_2:9;
        end;
      end;
      hence contradiction by A2,Def5;
    end;
    then consider x being set such that
A8: x in T"{w} and
A9: x in Carrier l by XBOOLE_0:3;
A10: x in dom T by A8,FUNCT_1:def 7;
A11: T.x in {w} by A8,FUNCT_1:def 7;
    reconsider x as Element of V by A8;
    T.x = w by A11,TARSKI:def 1;
    hence thesis by A9,A10,FUNCT_1:def 6;
  end;
  hence thesis by VECTSP_6:def 4;
end;

theorem Th30:
  Carrier (T@l) c= T .: (Carrier l)
proof
  T@l is Linear_Combination of T .: (Carrier l) by Th29;
  hence thesis by VECTSP_6:def 4;
end;

theorem Th31:
  for l,m being Linear_Combination of V st (Carrier l) misses (
  Carrier m) holds Carrier (l + m) = (Carrier l) \/ (Carrier m)
proof
  let l,m be Linear_Combination of V such that
A1: (Carrier l) misses (Carrier m);
  thus Carrier (l+m) c= (Carrier l) \/ (Carrier m) by VECTSP_6:23;
  thus (Carrier l) \/ (Carrier m) c= Carrier (l+m)
  proof
    let v be set such that
A2: v in (Carrier l) \/ (Carrier m);
    per cases by A2,XBOOLE_0:def 3;
    suppose
A3:   v in Carrier l;
      then reconsider v as Element of V;
      not v in Carrier m by A1,A2,A3,XBOOLE_0:5;
      then (l+m).v = (l.v) + (m.v) & m.v = 0.F by VECTSP_6:22;
      then
A4:   (l+m).v = l.v by RLVECT_1:4;
      l.v <> 0.F by A3,VECTSP_6:2;
      hence thesis by A4;
    end;
    suppose
A5:   v in Carrier m;
      then reconsider v as Element of V;
      not v in Carrier l by A1,A2,A5,XBOOLE_0:5;
      then (l+m).v = (l.v) + (m.v) & l.v = 0.F by VECTSP_6:22;
      then
A6:   (l+m).v = m.v by RLVECT_1:4;
      m.v <> 0.F by A5,VECTSP_6:2;
      hence thesis by A6;
    end;
  end;
end;

theorem Th32:
  for l,m being Linear_Combination of V st (Carrier l) misses (
  Carrier m) holds Carrier (l - m) = (Carrier l) \/ (Carrier m)
proof
  let l,m be Linear_Combination of V such that
A1: (Carrier l) misses (Carrier m);
  Carrier (-m) = Carrier m by VECTSP_6:38;
  hence thesis by A1,Th31;
end;

theorem Th33:
  for A,B being Subset of V st A c= B & B is Basis of V holds V
  is_the_direct_sum_of Lin A, Lin (B \ A)
proof
  let A,B be Subset of V such that
A1: A c= B and
A2: B is Basis of V;
A3: (Lin A) /\ (Lin (B \ A)) = (0).V
  proof
    set U = (Lin A) /\ (Lin (B \ A));
    reconsider W = (0).V as strict Subspace of U by VECTSP_4:39;
    for v being Element of U holds v in W
    proof
      let v be Element of U;
A4:   B is linearly-independent by A2,VECTSP_7:def 3;
A5:   v in U by STRUCT_0:def 5;
      then v in Lin A by VECTSP_5:3;
      then consider l being Linear_Combination of A such that
A6:   v = Sum l by VECTSP_7:7;
      v in Lin (B \ A) by A5,VECTSP_5:3;
      then consider m being Linear_Combination of B \ A such that
A7:   v = Sum m by VECTSP_7:7;
A8:   0.V = (Sum l) - (Sum m) by A6,A7,VECTSP_1:19
        .= Sum (l - m) by VECTSP_6:47;
A9:   Carrier (l - m) c= (Carrier l) \/ (Carrier m) & A \/ (B \ A) = B by A1,
VECTSP_6:41,XBOOLE_1:45;
A10:  Carrier l c= A & Carrier m c= B \ A by VECTSP_6:def 4;
      then (Carrier l) \/ (Carrier m) c= A \/ (B \ A) by XBOOLE_1:13;
      then Carrier (l - m) c= B by A9,XBOOLE_1:1;
      then reconsider n = l - m as Linear_Combination of B by VECTSP_6:def 4;
      A misses (B \ A) by XBOOLE_1:79;
      then Carrier n = (Carrier l) \/ (Carrier m) by A10,Th32,XBOOLE_1:64;
      then Carrier l = {} by A8,A4,VECTSP_7:def 1;
      then l = ZeroLC(V) by VECTSP_6:def 3;
      then Sum l = 0.V by VECTSP_6:15;
      hence thesis by A6,VECTSP_4:35;
    end;
    hence thesis by VECTSP_4:32;
  end;
  (Omega).V = (Lin A) + (Lin (B \ A))
  proof
    set U = (Lin A) + (Lin (B \ A));
A11: [#]V c= [#]U
    proof
      let v be set;
      assume v in [#]V;
      then reconsider v as Element of V;
      v in Lin B by A2,VECTSP_9:10;
      then consider l being Linear_Combination of B such that
A12:  v = Sum l by VECTSP_7:7;
      set n = l!(B\A);
      set m = l!A;
A13:  l = m + n by A1,Th27;
      ex v1,v2 being Element of V st v1 in Lin A & v2 in Lin (B \ A) & v
      = v1 + v2
      proof
        take Sum m, Sum n;
        thus thesis by A12,A13,VECTSP_6:44,VECTSP_7:7;
      end;
      then v in (Lin A) + (Lin (B \ A)) by VECTSP_5:1;
      hence thesis by STRUCT_0:def 5;
    end;
    [#]U c= [#]V by VECTSP_4:def 2;
    then [#]U = [#]V by A11,XBOOLE_0:def 10;
    hence thesis by VECTSP_4:29;
  end;
  hence thesis by A3,VECTSP_5:def 4;
end;

theorem Th34:
  for A being Subset of V, l being Linear_Combination of A, v
  being Element of V st T|A is one-to-one & v in A holds ex X being Subset of V
  st X misses A & T"{T.v} = {v} \/ X
proof
  let A be Subset of V, l be Linear_Combination of A, v be Element of V such
  that
A1: T|A is one-to-one and
A2: v in A;
  set X = T"{T.v} \ {v};
A3: X misses A
  proof
    dom T = [#]V by Th7;
    then
A4: dom (T|A) = A by RELAT_1:62;
    assume X meets A;
    then consider x being set such that
A5: x in X and
A6: x in A by XBOOLE_0:3;
    not x in {v} by A5,XBOOLE_0:def 5;
    then
A7: x <> v by TARSKI:def 1;
    x in T"{T.v} by A5,XBOOLE_0:def 5;
    then T.x in {T.v} by FUNCT_1:def 7;
    then
A8: T.x = T.v by TARSKI:def 1;
    T.x = (T|A).x by A6,FUNCT_1:49;
    then (T|A).v = (T|A).x by A2,A8,FUNCT_1:49;
    hence thesis by A1,A2,A6,A7,A4,FUNCT_1:def 4;
  end;
  take X;
  {v} c= T"{T.v}
  proof
    let x be set;
    assume x in {v};
    then
A9: x = v by TARSKI:def 1;
    dom T = [#]V & T.v in {T.v} by Th7,TARSKI:def 1;
    hence thesis by A9,FUNCT_1:def 7;
  end;
  hence thesis by A3,XBOOLE_1:45;
end;

theorem Th35:
  for X being Subset of V st X misses Carrier l & X <> {} holds l .: X = {0.F}
proof
  let X be Subset of V such that
A1: X misses Carrier l and
A2: X <> {};
  dom l = [#]V by FUNCT_2:92;
  then
A3: l .: X <> {} by A2,RELAT_1:119;
  l .: X c= {0.F} by A1,Th28;
  hence thesis by A3,ZFMISC_1:33;
end;

theorem Th36:
  for w being Element of W st w in Carrier (T@l) holds T"{w} meets Carrier l
proof
  let w be Element of W;
  assume w in Carrier (T@l);
  then
A1: (T@l).w <> 0.F by VECTSP_6:2;
  assume
A2: T"{w} misses Carrier l;
  per cases;
  suppose
    T"{w} = {};
    then Sum (l .: T"{w}) = Sum ({}F)
      .= 0.F by RLVECT_2:8;
    hence thesis by A1,Def5;
  end;
  suppose
    T"{w} <> {};
    then l .: T"{w} = {0.F} by A2,Th35;
    then Sum (l .: T"{w}) = 0.F by RLVECT_2:9;
    hence thesis by A1,Def5;
  end;
end;

theorem Th37:
  for v being Element of V st T|(Carrier l) is one-to-one & v in
  Carrier l holds (T@l).(T.v) = l.v
proof
  let v be Element of V such that
A1: T|(Carrier l) is one-to-one and
A2: v in Carrier l;
  consider X being Subset of V such that
A3: X misses Carrier l and
A4: T"{T.v} = {v} \/ X by A1,A2,Th34;
  per cases;
  suppose
A5: X = {};
A6: dom l = [#]V by FUNCT_2:92;
    l .: {v} = Im (l,v) .= {l.v} by A6,FUNCT_1:59;
    then Sum (l .: T"{T.v}) = l.v by A4,A5,RLVECT_2:9;
    hence thesis by Def5;
  end;
  suppose
A7: X <> {};
A8: l .: X c= {0.F}
    proof
      let y be set;
      assume y in l .: X;
      then consider x being set such that
A9:   x in dom l and
A10:  x in X and
A11:  y = l.x by FUNCT_1:def 6;
A12:  now
        assume x in Carrier l;
        then x in (Carrier l) /\ X by A10,XBOOLE_0:def 4;
        hence contradiction by A3,XBOOLE_0:def 7;
      end;
      reconsider x as Element of V by A9;
      l.x = 0.F by A12;
      hence thesis by A11,TARSKI:def 1;
    end;
A13: l .: X misses l .: {v}
    proof
      assume l .: X meets l .: {v};
      then consider x being set such that
A14:  x in l .: X and
A15:  x in l .: {v} by XBOOLE_0:3;
A16:  dom l = [#]V by FUNCT_2:92;
      l .: {v} = Im (l,v) .= {l.v} by A16,FUNCT_1:59;
      then
A17:  x = l.v by A15,TARSKI:def 1;
      x = 0.F by A8,A14,TARSKI:def 1;
      hence thesis by A2,A17,VECTSP_6:2;
    end;
A18: dom l = [#]V by FUNCT_2:92;
    {0.F} c= l .: X
    proof
      consider y being set such that
A19:  y in X by A7,XBOOLE_0:def 1;
A20:  now
        assume y in Carrier l;
        then y in (Carrier l) /\ X by A19,XBOOLE_0:def 4;
        hence contradiction by A3,XBOOLE_0:def 7;
      end;
      reconsider y as Element of V by A19;
      let x be set;
      assume x in {0.F};
      then x = 0.F by TARSKI:def 1;
      then l.y = x by A20;
      hence thesis by A18,A19,FUNCT_1:def 6;
    end;
    then
A21: l .: X = {0.F} by A8,XBOOLE_0:def 10;
A22: l .: {v} = Im (l,v) .= {l.v} by A18,FUNCT_1:59;
    l .: T"{T.v} = (l .: {v}) \/ (l .: X) by A4,RELAT_1:120;
    then Sum (l .: T"{T.v}) = (Sum (l .: {v})) + (Sum (l .: X)) by A13,
RLVECT_2:12
      .= l.v + (Sum ({0.F})) by A22,A21,RLVECT_2:9
      .= l.v + 0.F by RLVECT_2:9
      .= l.v by RLVECT_1:4;
    hence thesis by Def5;
  end;
end;

theorem Th38:
  for G being FinSequence of V st rng G = Carrier l & T|(Carrier l
  ) is one-to-one holds T*(l (#) G) = (T@l) (#) (T*G)
proof
  let G be FinSequence of V such that
A1: rng G = Carrier l and
A2: T|(Carrier l) is one-to-one;
  reconsider R = (T@l) (#) (T*G) as FinSequence of W;
  reconsider L = T*(l (#) G) as FinSequence of W;
A3: len R = len (T*G) by VECTSP_6:def 5
    .= len G by FINSEQ_2:33;
A4: len L = len (l (#) G) by FINSEQ_2:33
    .= len G by VECTSP_6:def 5;
  for k being Nat st 1 <= k & k <= len L holds L.k = R.k
  proof
A5: dom R = Seg len G by A3,FINSEQ_1:def 3;
    let k be Nat such that
A6: 1 <= k & k <= len L;
    reconsider gk = G/.k as Element of V;
    len (l (#) G) = len G by VECTSP_6:def 5;
    then
A7: dom (l (#) G) = Seg len G by FINSEQ_1:def 3;
    k in NAT by ORDINAL1:def 12;
    then
A8: k in dom (l (#) G) by A4,A6,A7;
    then
A9: k in dom G by A7,FINSEQ_1:def 3;
    then
A10: G.k = G/.k by PARTFUN1:def 6;
    then reconsider Gk = G.k as Element of V;
    (T*G).k = T.Gk by A9,FUNCT_1:13;
    then reconsider TGk = (T*G).k as Element of W;
    (l (#) G).k = (l.gk)*gk by A8,VECTSP_6:def 5;
    then
A11: L.k = T.((l.gk)*gk) by A8,FUNCT_1:13
      .= (l.gk)*(T.gk) by MOD_2:def 2
      .= (l.Gk)*TGk by A9,A10,FUNCT_1:13;
    G.k in rng G & (T*G).k = T.(G.k) by A9,FUNCT_1:3,13;
    then
A12: (T@l).((T*G).k) = l.(G.k) by A1,A2,Th37;
    dom T = [#]V by Th7;
    then dom (T*G) = dom G by A1,RELAT_1:27;
    then (T*G)/.k = (T*G).k by A9,PARTFUN1:def 6;
    hence thesis by A7,A8,A11,A5,A12,VECTSP_6:def 5;
  end;
  hence thesis by A4,A3,FINSEQ_1:14;
end;

theorem Th39:
  T|(Carrier l) is one-to-one implies T .: (Carrier l) = Carrier ( T@l)
proof
  assume
A1: T|(Carrier l) is one-to-one;
A2: T .: (Carrier l) c= Carrier (T@l)
  proof
    let w be set;
    assume w in T .: (Carrier l);
    then consider v being set such that
A3: v in dom T and
A4: v in Carrier l and
A5: T.v = w by FUNCT_1:def 6;
    reconsider v as Element of V by A3;
    (T@l).(T.v) = l.v & l.v <> 0.F by A1,A4,Th37,VECTSP_6:2;
    hence thesis by A5;
  end;
  Carrier (T@l) c= T .: (Carrier l) by Th30;
  hence thesis by A2,XBOOLE_0:def 10;
end;

theorem Th40:
  for A being Subset of V, B being Basis of V, l being
  Linear_Combination of B \ A st A is Basis of ker T & A c= B holds T.(Sum l) =
  Sum (T@l)
proof
  let A be Subset of V, B be Basis of V, l be Linear_Combination of B \ A;
  assume A is Basis of ker T & A c= B;
  then
A1: T|(B \ A) is one-to-one by Th22;
  Carrier l c= B \ A by VECTSP_6:def 4;
  then
A2: (T|(B \ A))|(Carrier l) = T|(Carrier l) by RELAT_1:74;
  then
A3: T|(Carrier l) is one-to-one by A1,FUNCT_1:52;
  consider G being FinSequence of V such that
A4: G is one-to-one and
A5: rng G = Carrier l and
A6: Sum l = Sum (l (#) G) by VECTSP_6:def 6;
  set H = T*G;
  reconsider H as FinSequence of W;
A7: rng H = T .: (Carrier l) by A5,RELAT_1:127
    .= Carrier (T@l) by A3,Th39;
  dom T = [#]V by Th7;
  then H is one-to-one by A4,A5,A1,A2,Th1,FUNCT_1:52;
  then
A8: Sum (T@l) = Sum ((T@l) (#) H) by A7,VECTSP_6:def 6;
  T*(l (#) G) = (T@l) (#) H by A5,A3,Th38;
  hence thesis by A6,A8,MATRLIN:16;
end;

theorem Th41:
  for X being Subset of V st X is linearly-dependent holds ex l
  being Linear_Combination of X st Carrier l <> {} & Sum l = 0.V
proof
  let X be Subset of V;
  assume X is linearly-dependent;
  then
  not (for l being Linear_Combination of X st Sum l = 0.V holds Carrier l
  = {}) by VECTSP_7:def 1;
  hence thesis;
end;

:: "Pulling back" a linear combination from the image space of a
:: linear transformation to the base space.

definition
  let F be Field, V,W be VectSp of F, X be Subset of V, T be
  linear-transformation of V,W, l be Linear_Combination of T .: X;
  assume
A1: T|X is one-to-one;
  func T#l -> Linear_Combination of X equals
  :Def6:
  (l*T) +* ((V \ X) --> 0.F);
  coherence
  proof
    rng (l*T) c= rng l & rng l c= [#]F by FUNCT_2:92,RELAT_1:26;
    then
A2: rng (l*T) c= [#]F by XBOOLE_1:1;
    dom l = [#]W by FUNCT_2:92;
    then rng T c= dom l by Th7;
    then
A3: dom (l*T) = dom T by RELAT_1:27;
    set f = (l*T) +* ((V \ X) --> 0.F);
A4: dom ((V \ X) --> 0.F) = [#]V \ X by FUNCOP_1:13;
    rng ((V \ X) --> 0.F) c= {0.F} by FUNCOP_1:13;
    then rng ((V \ X) --> 0.F) c= [#]F by XBOOLE_1:1;
    then rng f c= rng (l*T) \/ rng ((V \ X) --> 0.F) & rng (l*T) \/ rng ((V \
    X) --> 0.F) c= [#]F by A2,FUNCT_4:17,XBOOLE_1:8;
    then
A5: rng f c= [#]F by XBOOLE_1:1;
    dom T = [#]V & [#]V \/ ([#]V \ X) = [#]V by Th7,XBOOLE_1:12;
    then dom f = [#]V by A3,A4,FUNCT_4:def 1;
    then reconsider f as Element of Funcs ([#]V,[#]F) by A5,FUNCT_2:def 2;
    ex T being finite Subset of V st for v being Element of V st not v in
    T holds f.v = 0.F
    proof
      set C = { v where v is Element of V : f.v <> 0.F };
      C c= [#]V
      proof
        let x be set;
        assume x in C;
        then ex v being Element of V st v = x & f.v <> 0.F;
        hence thesis;
      end;
      then reconsider C as Subset of V;
      ex g being Function st g is one-to-one & dom g = C & rng g c= Carrier l
      proof
        set S = (T"(Carrier l)) /\ X;
        set g = T|S;
        take g;
A6:     C c= S
        proof
          let x be set such that
A7:       x in C;
A8:       ex v being Element of V st v = x & f.v <> 0.F by A7;
          reconsider x as Element of V by A7;
A9:       now
            assume not x in X;
            then
A10:        x in V \ X by XBOOLE_0:def 5;
            then x in dom ((V \ X) --> 0.F) by FUNCOP_1:13;
            then f.x = ((V \ X) --> 0.F).x by FUNCT_4:13;
            hence contradiction by A8,A10,FUNCOP_1:7;
          end;
          then not x in V \ X by XBOOLE_0:def 5;
          then
A11:      f.x = (l*T).x by A4,FUNCT_4:11;
A12:      dom T = [#]V by Th7;
          then (l*T).x = l.(T.x) by FUNCT_1:13;
          then T.x in Carrier l by A8,A11;
          then x in T"(Carrier l) by A12,FUNCT_1:def 7;
          hence thesis by A9,XBOOLE_0:def 4;
        end;
A13:    dom T = [#]V by Th7;
A14:    rng g c= Carrier l
        proof
          let y be set;
          assume y in rng g;
          then consider x being set such that
A15:      x in dom g and
A16:      y = g.x by FUNCT_1:def 3;
          x in T"(Carrier l) by A15,XBOOLE_0:def 4;
          then T.x in Carrier l by FUNCT_1:def 7;
          hence thesis by A15,A16,FUNCT_1:49;
        end;
        S c= C
        proof
          let x be set such that
A17:      x in S;
A18:      x in X by A17,XBOOLE_0:def 4;
A19:      x in T"(Carrier l) by A17,XBOOLE_0:def 4;
          then
A20:      x in dom T by FUNCT_1:def 7;
A21:      T.x in Carrier l by A19,FUNCT_1:def 7;
          reconsider x as Element of V by A17;
A22:      l.(T.x) <> 0.F by A21,VECTSP_6:2;
          not x in dom ((V \ X) --> 0.F) by A18,XBOOLE_0:def 5;
          then
A23:      f.x = (l*T).x by FUNCT_4:11;
          (l*T).x = l.(T.x) by A20,FUNCT_1:13;
          hence thesis by A23,A22;
        end;
        then S = C by A6,XBOOLE_0:def 10;
        hence thesis by A1,A13,A14,Th2,RELAT_1:62,XBOOLE_1:17;
      end;
      then card C c= card Carrier l by CARD_1:10;
      then reconsider C as finite Subset of V;
      take C;
      thus thesis;
    end;
    then reconsider f as Linear_Combination of V by VECTSP_6:def 1;
    Carrier f c= X
    proof
      let x be set such that
A24:  x in Carrier f;
      reconsider x as Element of V by A24;
      now
        assume not x in X;
        then
A25:    x in V \ X by XBOOLE_0:def 5;
        then f.x = ((V \ X) --> 0.F).x by A4,FUNCT_4:13
          .= 0.F by A25,FUNCOP_1:7;
        hence contradiction by A24,VECTSP_6:2;
      end;
      hence thesis;
    end;
    hence thesis by VECTSP_6:def 4;
  end;
end;

theorem Th42:
  for X being Subset of V, l being Linear_Combination of T .: X, v
  being Element of V st v in X & T|X is one-to-one holds (T#l).v = l.(T.v)
proof
  let X be Subset of V, l be Linear_Combination of T .: X, v be Element of V;
  assume v in X & T|X is one-to-one;
  then ( not v in dom ((V \ X) --> 0.F))& T#l = (l*T) +* ((V \ X) --> 0.F) by
Def6,XBOOLE_0:def 5;
  then
A1: (T#l).v = (l*T).v by FUNCT_4:11;
  dom T = [#]V by Th7;
  hence thesis by A1,FUNCT_1:13;
end;

:: # is a right inverse of @

theorem Th43:
  for X being Subset of V, l being Linear_Combination of T .: X st
  T|X is one-to-one holds T@(T#l) = l
proof
  let X be Subset of V, l be Linear_Combination of T .: X such that
A1: T|X is one-to-one;
  let w be Element of W;
  set m = T@(T#l);
  per cases;
  suppose
A2: w in Carrier l;
    then
A3: l.w <> 0.F by VECTSP_6:2;
A4: dom (T#l) = [#]V by FUNCT_2:92;
    Carrier l c= T .: X by VECTSP_6:def 4;
    then consider v being set such that
A5: v in dom T and
A6: v in X and
A7: w = T.v by A2,FUNCT_1:def 6;
    reconsider v as Element of V by A5;
    consider B being Subset of V such that
A8: B misses X and
A9: T"{T.v} = {v} \/ B by A1,A6,Th34;
A10: (T#l).v = l.(T.v) by A1,A6,Th42;
A11: (T#l) .: {v} = Im (T#l,v) .= {(T#l).v} by A4,FUNCT_1:59;
A12: m.w = Sum ((T#l) .: T"{T.v}) by A7,Def5
      .= Sum ({l.(T.v)} \/ ((T#l) .: B)) by A9,A10,A11,RELAT_1:120;
    per cases;
    suppose
      B = {};
      then m.w = Sum ({l.(T.v)} \/ {}F) by A12
        .= l.w by A7,RLVECT_2:9;
      hence thesis;
    end;
    suppose
A13:  B <> {};
      Carrier (T#l) c= X by VECTSP_6:def 4;
      then B misses Carrier (T#l) by A8,XBOOLE_1:63;
      then m.w = Sum ({l.(T.v)} \/ {0.F}) by A12,A13,Th35
        .= Sum ({l.(T.v)}) + Sum ({0.F}) by A3,A7,RLVECT_2:12,ZFMISC_1:11
        .= l.(T.v) + Sum ({0.F}) by RLVECT_2:9
        .= l.(T.v) + 0.F by RLVECT_2:9
        .= l.w by A7,RLVECT_1:4;
      hence thesis;
    end;
  end;
  suppose
A14: not w in Carrier l;
    then
A15: l.w = 0.F;
    now
      assume
A16:  m.w <> 0.F;
      then w in Carrier m;
      then T"{w} meets Carrier (T#l) by Th36;
      then consider v being Element of V such that
A17:  v in T"{w} and
A18:  v in Carrier (T#l) by Th3;
      T.v in {w} by A17,FUNCT_1:def 7;
      then
A19:  T.v = w by TARSKI:def 1;
A20:  Carrier (T#l) c= X by VECTSP_6:def 4;
      then T|(Carrier (T#l)) is one-to-one by A1,Th2;
      then m.w = (T#l).v by A18,A19,Th37
        .= 0.F by A1,A15,A18,A19,A20,Th42;
      hence contradiction by A16;
    end;
    hence thesis by A14;
  end;
end;

begin :: The rank+nullity theorem

definition
  let F be Field, V,W be finite-dimensional VectSp of F, T be
  linear-transformation of V,W;
  func rank(T) -> Nat equals
  dim (im T);
  coherence;
  func nullity(T) -> Nat equals
  dim (ker T);
  coherence;
end;

::$N Rank-nullity theorem
theorem Th44:
  for V,W being finite-dimensional VectSp of F, T being
  linear-transformation of V,W holds dim V = rank(T) + nullity(T)
proof
  let V,W be finite-dimensional VectSp of F, T be linear-transformation of V,W;
  set A = the finite Basis of ker T;
  reconsider A9 = A as Subset of V by Th19;
  consider B being Basis of V such that
A1: A c= B by VECTSP_9:13;
  reconsider B as finite Subset of V by VECTSP_9:20;
  reconsider X = B \ A9 as finite Subset of B by XBOOLE_1:36;
  reconsider X as finite Subset of V;
A2: B = A \/ X by A1,XBOOLE_1:45;
  reconsider B as finite Basis of V;
  reconsider A as finite Basis of ker T;
  reconsider C = T .: X as finite Subset of W;
A3: T|X is one-to-one by A1,Th22;
A4: C is linearly-independent
  proof
    assume C is linearly-dependent;
    then consider l being Linear_Combination of C such that
A5: Carrier l <> {} and
A6: Sum l = 0.W by Th41;
    ex m being Linear_Combination of X st l = T@m
    proof
      reconsider l9 = l as Linear_Combination of T .: X;
      set m = T#(l9);
      take m;
      thus thesis by A3,Th43;
    end;
    then consider m being Linear_Combination of B \ A9 such that
A7: l = T@m;
    T.(Sum m) = 0.W by A1,A6,A7,Th40;
    then Sum m in ker T by Th10;
    then Sum m in Lin A by VECTSP_7:def 3;
    then Sum m in Lin A9 by VECTSP_9:17;
    then consider n being Linear_Combination of A9 such that
A8: Sum m = Sum n by VECTSP_7:7;
A9: Carrier (m - n) c= (Carrier m) \/ (Carrier n) & (B \ A9) \/ A9 = B by A1,
VECTSP_6:41,XBOOLE_1:45;
A10: Carrier m c= B \ A9 & Carrier n c= A by VECTSP_6:def 4;
    then (Carrier m) \/ (Carrier n) c= (B \ A9) \/ A by XBOOLE_1:13;
    then Carrier (m - n) c= B by A9,XBOOLE_1:1;
    then reconsider o = m - n as Linear_Combination of B by VECTSP_6:def 4;
A11: B is linearly-independent by VECTSP_7:def 3;
    (Sum m) - (Sum n) = 0.V by A8,VECTSP_1:19;
    then Sum (m - n) = 0.V by VECTSP_6:47;
    then
A12: Carrier o = {} by A11,VECTSP_7:def 1;
    A9 misses B \ A9 by XBOOLE_1:79;
    then Carrier (m - n) = (Carrier m) \/ (Carrier n) by A10,Th32,XBOOLE_1:64;
    then Carrier m = {} by A12;
    then T .: (Carrier m) = {};
    hence thesis by A5,A7,Th30,XBOOLE_1:3;
  end;
  dom T = [#]V by Th7;
  then X c= dom (T|X) by RELAT_1:62;
  then X,(T|X) .: X are_equipotent by A3,CARD_1:33;
  then X,C are_equipotent by RELAT_1:129;
  then
A13: card C = card X by CARD_1:5;
  reconsider C as finite Subset of im T by Th12;
  reconsider L = Lin C as strict Subspace of im T;
  for v being Element of im T holds v in L
  proof
    reconsider A9 = A as Subset of V by Th19;
    let v be Element of im T;
    reconsider v9 = v as Element of W by VECTSP_4:10;
    reconsider C9 = C as Subset of W;
    v in im T by STRUCT_0:def 5;
    then consider u being Element of V such that
A14: T.u = v9 by Th13;
    V is_the_direct_sum_of Lin A9, Lin (B \ A9) by A1,Th33;
    then
A15: (Omega).V = (Lin A9) + (Lin (B \ A9)) by VECTSP_5:def 4;
    u in (Omega).V by STRUCT_0:def 5;
    then consider u1, u2 being Element of V such that
A16: u1 in Lin A9 and
A17: u2 in Lin (B \ A9) and
A18: u = u1 + u2 by A15,VECTSP_5:1;
    consider l being Linear_Combination of B \ A9 such that
A19: u2 = Sum l by A17,VECTSP_7:7;
    Lin A = ker T by VECTSP_7:def 3;
    then u1 in ker T by A16,VECTSP_9:17;
    then
A20: T.u1 = 0.W by Th10;
    T@l is Linear_Combination of T .: (Carrier l) & Carrier l c= B \ A9
    by Th29,VECTSP_6:def 4;
    then reconsider m = T@l as Linear_Combination of C9 by RELAT_1:123
,VECTSP_6:4;
    T.u = T.u1 + T.u2 by A18,VECTSP_1:def 20;
    then
A21: T.u = T.u2 by A20,RLVECT_1:4;
    ex m being Linear_Combination of C9 st v = Sum m
    proof
      take m;
      thus thesis by A1,A14,A21,A19,Th40;
    end;
    then v in Lin C9 by VECTSP_7:7;
    hence thesis by VECTSP_9:17;
  end;
  then
A22: Lin C = im T by VECTSP_4:32;
  reconsider C as linearly-independent Subset of im T by A4,VECTSP_9:12;
  reconsider C as finite Basis of im T by A22,VECTSP_7:def 3;
A23: nullity T = card A & rank T = card C by VECTSP_9:def 1;
  dim V = card B by VECTSP_9:def 1
    .= rank T + nullity T by A2,A13,A23,CARD_2:40,XBOOLE_1:79;
  hence thesis;
end;

theorem
  for V,W being finite-dimensional VectSp of F, T being
  linear-transformation of V,W st T is one-to-one holds dim V = rank T
proof
  let V,W be finite-dimensional VectSp of F, T be linear-transformation of V,W;
  assume T is one-to-one;
  then ker T = (0).V by Th15;
  then
A1: nullity(T) = 0 by Th16;
  dim V = rank(T) + nullity(T) by Th44
    .= rank(T) by A1;
  hence thesis;
end;