:: RANKNULL semantic presentation

begin

theorem Th1: :: RANKNULL:1
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; ::_thesis: ( g is one-to-one & f | (rng g) is one-to-one & rng g c= dom f implies f * g is one-to-one )
assume that
A1: g is one-to-one and
A2: f | (rng g) is one-to-one and
A3: rng g c= dom f ; ::_thesis: f * g is one-to-one
set h = f * g;
A4: dom (f * g) c= dom g
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom (f * g) or x in dom g )
assume  x in dom (f * g) ; ::_thesis: x in dom g
hence  x in dom g by FUNCT_1:11; ::_thesis: verum
end;
 dom g c= dom (f * g)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom g or x in dom (f * g) )
assume A5: x in dom g ; ::_thesis: x in dom (f * g)
 g . x in rng g by A5, FUNCT_1:3;
hence  x in dom (f * g) by A3, A5, FUNCT_1:11; ::_thesis: verum
end;
then A6: dom (f * g) = dom g by A4, XBOOLE_0:def_10;
 for x1, x2 being set st x1 in dom (f * g) & x2 in dom (f * g) & (f * g) . x1 = (f * g) . x2 holds
x1 = x2
proof
let x1, x2 be set ; ::_thesis: ( x1 in dom (f * g) & x2 in dom (f * g) & (f * g) . x1 = (f * g) . x2 implies x1 = x2 )
assume that
A7: x1 in dom (f * g) and
A8: x2 in dom (f * g) and
A9: (f * g) . x1 = (f * g) . x2 ; ::_thesis: x1 = x2
A10: ( (f * g) . x1 = f . (g . x1) & (f * g) . 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, FUNCT_1:49;
then  g . x1 = g . x2 by A2, A9, A10, A11, A12, FUNCT_1:def_4;
hence  x1 = x2 by A1, A4, A7, A8, FUNCT_1:def_4; ::_thesis: verum
end;
hence  f * g is one-to-one by FUNCT_1:def_4; ::_thesis: verum
end;

theorem Th2: :: RANKNULL:2
for f being Function
for 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; ::_thesis: for X, Y being set st X c= Y & f | Y is one-to-one holds
f | X is one-to-one
let X, Y be set ; ::_thesis: ( X c= Y & f | Y is one-to-one implies f | X is one-to-one )
assume that
A1: X c= Y and
A2: f | Y is one-to-one ; ::_thesis: f | X is one-to-one
 f | X = (f | Y) | X by A1, RELAT_1:74;
hence  f | X is one-to-one by A2, FUNCT_1:52; ::_thesis: verum
end;

theorem Th3: :: RANKNULL:3
for V being 1-sorted
for 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 ; ::_thesis: for X, Y being Subset of V holds
( X meets Y iff ex v being Element of V st
( v in X & v in Y ) )
let X, Y be Subset of V; ::_thesis: ( X meets Y iff ex v being Element of V st
( v in X & v in Y ) )
 ( X meets Y implies ex v being Element of V st
( v in X & v in Y ) )
proof
assume  X meets Y ; ::_thesis: ex v being Element of V st
( v in X & v in 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 ; ::_thesis: ( v in X & v in Y )
thus  ( v in X & v in Y ) by A1, A2; ::_thesis: verum
end;
hence  ( X meets Y iff ex v being Element of V st
( v in X & v in Y ) ) by XBOOLE_0:3; ::_thesis: verum
end;


registration
let F be Field;
let V be finite-dimensional VectSp of F;
cluster finite for Basis of V;
existence
 ex b1 being Basis of V st b1 is finite
proof
consider A being finite Subset of V such that
A1: A is Basis of V by MATRLIN:def_1;
reconsider A = A as Basis of V by A1;
take  A ; ::_thesis: A is finite
thus  A is finite ; ::_thesis: verum
end;
end;

registration
let F be Field;
let V, W be VectSp of F;
cluster Relation-like the carrier of V -defined the carrier of W -valued Function-like quasi_total additive homogeneous for Element of K6(K7( the carrier of V, the carrier of W));
existence
 ex b1 being Function of V,W st
( b1 is additive & b1 is homogeneous )
proof
set f = FuncZero (([#] V),W);
reconsider f = FuncZero (([#] V),W) 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; ::_thesis: f . (x + y) = (f . x) + (f . y)
A2: f . y = 0. W by FUNCOP_1:7;
 ( f . (x + y) = 0. W & f . x = 0. W ) by FUNCOP_1:7;
hence  f . (x + y) = (f . x) + (f . y) by A2, RLVECT_1:def_4; ::_thesis: verum
end;
take  f ; ::_thesis: ( f is additive & f is homogeneous )
 for a being Element of F
for x being Element of V holds f . (a * x) = a * (f . x)
proof
let a be Element of F; ::_thesis: for x being Element of V holds f . (a * x) = a * (f . x)
let x be Element of V; ::_thesis: f . (a * x) = a * (f . x)
 ( f . (a * x) = 0. W & f . x = 0. W ) by FUNCOP_1:7;
hence  f . (a * x) = a * (f . x) by VECTSP_1:14; ::_thesis: verum
end;
hence  ( f is additive & f is homogeneous ) by A1, VECTSP_1:def_20, MOD_2:def_2; ::_thesis: verum
end;
end;

theorem Th4: :: RANKNULL:4
for F being Field
for V being VectSp of F st [#] V is finite holds
V is finite-dimensional
proof
let F be Field; ::_thesis: for V being VectSp of F st [#] V is finite holds
V is finite-dimensional
let V be VectSp of F; ::_thesis: ( [#] V is finite implies V is finite-dimensional )
set B = the Basis of V;
assume  [#] V is finite ; ::_thesis: V is finite-dimensional
then reconsider B = the Basis of V as finite Subset of V ;
take  B ; :: according to MATRLIN:def_1 ::_thesis: B is Basis of V
thus  B is Basis of V ; ::_thesis: verum
end;

theorem :: RANKNULL:5
for F being Field
for V being finite-dimensional VectSp of F st card ([#] V) = 1 holds
dim V = 0
proof
let F be Field; ::_thesis: for V being finite-dimensional VectSp of F st card ([#] V) = 1 holds
dim V = 0
let V be finite-dimensional VectSp of F; ::_thesis: ( card ([#] V) = 1 implies dim V = 0 )
assume A1: card ([#] V) = 1 ; ::_thesis: dim V = 0
 [#] V = {(0. V)}
proof
 ex y being set st [#] V = {y} by A1, CARD_2:42;
hence  [#] V = {(0. V)} by TARSKI:def_1; ::_thesis: verum
end;
then  (Omega). V = (0). V by VECTSP_4:def_3;
hence  dim V = 0 by VECTSP_9:29; ::_thesis: verum
end;

theorem :: RANKNULL:6
for F being Field
for V being VectSp of F st card ([#] V) = 2 holds
dim V = 1
proof
let F be Field; ::_thesis: for V being VectSp of F st card ([#] V) = 2 holds
dim V = 1
let V be VectSp of F; ::_thesis: ( card ([#] V) = 2 implies dim V = 1 )
assume A1: card ([#] V) = 2 ; ::_thesis: dim V = 1
then A2: [#] V is finite ;
reconsider C = [#] V as finite set by A1;
reconsider V = 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;
percases ( x = 0. V or y = 0. V ) by A4, TARSKI:def_2;
supposeA5: x = 0. V ; ::_thesis: ex v being Vector of V st
( v <> 0. V & (Omega). V = Lin {v} )
then reconsider x = x as Element of V ;
reconsider y = y as Element of V by A4, TARSKI:def_2;
set L = Lin {y};
take  y ; ::_thesis: ( y <> 0. V & (Omega). V = Lin {y} )
 for v being Element of V holds
( v in (Omega). V iff v in Lin {y} )
proof
let v be Element of V; ::_thesis: ( v in (Omega). V iff v in Lin {y} )
 ( v in (Omega). V implies v in Lin {y} )
proof
assume  v in (Omega). V ; ::_thesis: v in Lin {y}
A6: y in {y} by TARSKI:def_1;
A7: 0. (Lin {y}) in Lin {y} by STRUCT_0:def_5;
percases ( v = x or v = y ) by A4, TARSKI:def_2;
suppose v = x ; ::_thesis: v in Lin {y}
hence  v in Lin {y} by A5, A7, VECTSP_4:def_2; ::_thesis: verum
end;
suppose v = y ; ::_thesis: v in Lin {y}
hence  v in Lin {y} by A6, VECTSP_7:8; ::_thesis: verum
end;
end;
end;
hence  ( v in (Omega). V iff v in Lin {y} ) by STRUCT_0:def_5; ::_thesis: verum
end;
hence  ( y <> 0. V & (Omega). V = Lin {y} ) by A3, A5, VECTSP_4:30; ::_thesis: verum
end;
supposeA8: y = 0. V ; ::_thesis: ex v being Vector of V st
( v <> 0. V & (Omega). V = Lin {v} )
reconsider x = x as Element of V by A4, TARSKI:def_2;
reconsider y = y as Element of V by A8;
set L = Lin {x};
take  x ; ::_thesis: ( x <> 0. V & (Omega). V = Lin {x} )
 for v being Element of V holds
( v in (Omega). V iff v in Lin {x} )
proof
let v be Element of V; ::_thesis: ( v in (Omega). V iff v in Lin {x} )
 ( v in (Omega). V implies v in Lin {x} )
proof
assume  v in (Omega). V ; ::_thesis: v in Lin {x}
A9: x in {x} by TARSKI:def_1;
A10: 0. (Lin {x}) in Lin {x} by STRUCT_0:def_5;
percases ( v = y or v = x ) by A4, TARSKI:def_2;
suppose v = y ; ::_thesis: v in Lin {x}
hence  v in Lin {x} by A8, A10, VECTSP_4:def_2; ::_thesis: verum
end;
suppose v = x ; ::_thesis: v in Lin {x}
hence  v in Lin {x} by A9, VECTSP_7:8; ::_thesis: verum
end;
end;
end;
hence  ( v in (Omega). V iff v in Lin {x} ) by STRUCT_0:def_5; ::_thesis: verum
end;
hence  ( x <> 0. V & (Omega). V = Lin {x} ) by A3, A8, VECTSP_4:30; ::_thesis: verum
end;
end;
end;
hence  dim V = 1 by VECTSP_9:30; ::_thesis: verum
end;

begin

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

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

theorem Th8: :: RANKNULL:8
for F being Field
for W, V being VectSp of F
for T being linear-transformation of V,W
for x, y being Element of V holds (T . x) - (T . y) = T . (x - y)
proof
let F be Field; ::_thesis: for W, V being VectSp of F
for T being linear-transformation of V,W
for x, y being Element of V holds (T . x) - (T . y) = T . (x - y)
let W, V be VectSp of F; ::_thesis: for T being linear-transformation of V,W
for x, y being Element of V holds (T . x) - (T . y) = T . (x - y)
let T be linear-transformation of V,W; ::_thesis: for x, y being Element of V holds (T . x) - (T . y) = T . (x - y)
let x, y be Element of V; ::_thesis: (T . x) - (T . y) = T . (x - y)
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  (T . x) - (T . y) = T . (x - y) by A1, VECTSP_1:14; ::_thesis: verum
end;

theorem Th9: :: RANKNULL:9
for F being Field
for V, W being VectSp of F
for T being linear-transformation of V,W holds T . (0. V) = 0. W
proof
let F be Field; ::_thesis: for V, W being VectSp of F
for T being linear-transformation of V,W holds T . (0. V) = 0. W
let V, W be VectSp of F; ::_thesis: for T being linear-transformation of V,W holds T . (0. V) = 0. W
let T be linear-transformation of V,W; ::_thesis: T . (0. V) = 0. W
 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  T . (0. V) = 0. W ; ::_thesis: verum
end;

definition
let F be Field;
let V, W be VectSp of F;
let T be linear-transformation of V,W;
func ker T ->  strict Subspace of V means :Def1: :: RANKNULL:def 1
 [#] it =  {  u where u is Element of V : T . u = 0. W  }  ;
existence
 ex b1 being strict Subspace of V st [#] b1 =  {  u where u is Element of V : T . u = 0. W  }
proof
set K =  {  u where u is Element of V : T . u = 0. W  }  ;
  {  u where u is Element of V : T . u = 0. W  }  c= [#] V
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  u where u is Element of V : T . u = 0. W  }  or x in [#] V )
assume  x in  {  u where u is Element of V : T . u = 0. W  }  ; ::_thesis: x in [#] V
then  ex u being Element of V st
( u = x & T . u = 0. W ) ;
hence  x in [#] V ; ::_thesis: verum
end;
then reconsider K =  {  u where u is Element of V : T . u = 0. W  }  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; ::_thesis: ( v in K implies T . v = 0. W )
assume  v in K ; ::_thesis: T . v = 0. W
then  ex u being Element of V st
( u = v & T . u = 0. W ) ;
hence  T . v = 0. W ; ::_thesis: verum
end;
now__::_thesis:_for_u_being_Element_of_V
for_a_being_Element_of_F_st_u_in_K_holds_
a_*_u_in_K
let u be Element of V; ::_thesis: for a being Element of F st u in K holds
a * u in K
let a be Element of F; ::_thesis: ( u in K implies a * u in K )
assume  u in K ; ::_thesis: a * 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 ; ::_thesis: verum
end;
then A2: for a being Element of F
for 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__::_thesis:_for_u,_v_being_Element_of_V_st_u_in_K_&_v_in_K_holds_
u_+_v_in_K
let u, v be Element of V; ::_thesis: ( u in K & v in K implies u + v in K )
assume  ( u in K & v in K ) ; ::_thesis: u + 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 ; ::_thesis: verum
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 ; ::_thesis: [#] W =  {  u where u is Element of V : T . u = 0. W  }
thus  [#] W =  {  u where u is Element of V : T . u = 0. W  }  by A4; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict Subspace of V st [#] b1 =  {  u where u is Element of V : T . u = 0. W  }  & [#] b2 =  {  u where u is Element of V : T . u = 0. W  }  holds
b1 = b2 by VECTSP_4:29;
end;

:: deftheorem Def1 defines ker RANKNULL:def_1_:_
 for F being Field
for V, W being VectSp of F
for T being linear-transformation of V,W
for b5 being strict Subspace of V holds
( b5 = ker T iff [#] b5 =  {  u where u is Element of V : T . u = 0. W  }  );

theorem Th10: :: RANKNULL:10
for F being Field
for V, W being VectSp of F
for T being linear-transformation of V,W
for x being Element of V holds
( x in ker T iff T . x = 0. W )
proof
let F be Field; ::_thesis: for V, W being VectSp of F
for T being linear-transformation of V,W
for x being Element of V holds
( x in ker T iff T . x = 0. W )
let V, W be VectSp of F; ::_thesis: for T being linear-transformation of V,W
for x being Element of V holds
( x in ker T iff T . x = 0. W )
let T be linear-transformation of V,W; ::_thesis: for x being Element of V holds
( x in ker T iff T . x = 0. W )
let x be Element of V; ::_thesis: ( x in ker T iff T . x = 0. W )
thus  ( x in ker T implies T . x = 0. W ) ::_thesis: ( T . x = 0. W implies x in ker T )
proof
assume  x in ker T ; ::_thesis: T . x = 0. W
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  T . x = 0. W ; ::_thesis: verum
end;
assume  T . x = 0. W ; ::_thesis: x in ker T
then  x in  {  u where u is Element of V : T . u = 0. W  }  ;
then  x in [#] (ker T) by Def1;
hence  x in ker T by STRUCT_0:def_5; ::_thesis: verum
end;

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

definition
let F be Field;
let V, W be VectSp of F;
let T be linear-transformation of V,W;
func im T ->  strict Subspace of W means :Def2: :: RANKNULL:def 2
 [#] it = T .: ([#] V);
existence
 ex b1 being strict Subspace of W st [#] b1 = T .: ([#] V)
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; ::_thesis: ( u in U iff ex v being Element of V st T . v = u )
thus  ( u in U implies ex v being Element of V st T . v = u ) ::_thesis: ( ex v being Element of V st T . v = u implies u in U )
proof
assume  u in U ; ::_thesis: ex v being Element of V st T . v = 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 = x as Element of V by A2;
take  x ; ::_thesis: T . x = u
thus  T . x = u by A3; ::_thesis: verum
end;
thus  ( ex v being Element of V st T . v = u implies u in U ) ::_thesis: verum
proof
given v being Element of V such that A4: T . v = u ; ::_thesis: u in U
 v in [#] V ;
then  v in dom T by Th7;
hence  u in U by A4, FUNCT_1:def_6; ::_thesis: verum
end;
end;
A5: now__::_thesis:_for_u,_v_being_Element_of_W_st_u_in_U_&_v_in_U_holds_
u_+_v_in_U
let u, v be Element of W; ::_thesis: ( u in U & v in U implies u + v in U )
assume that
A6: u in U and
A7: v in U ; ::_thesis: u + 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; ::_thesis: verum
end;
now__::_thesis:_for_a_being_Element_of_F
for_w_being_Element_of_W_st_w_in_U_holds_
a_*_w_in_U
let a be Element of F; ::_thesis: for w being Element of W st w in U holds
a * w in U
let w be Element of W; ::_thesis: ( w in U implies a * w in U )
assume  w in U ; ::_thesis: a * 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; ::_thesis: verum
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 ; ::_thesis: [#] A = T .: ([#] V)
thus  [#] A = T .: ([#] V) by A12; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict Subspace of W st [#] b1 = T .: ([#] V) & [#] b2 = T .: ([#] V) holds
b1 = b2 by VECTSP_4:29;
end;

:: deftheorem Def2 defines im RANKNULL:def_2_:_
 for F being Field
for V, W being VectSp of F
for T being linear-transformation of V,W
for b5 being strict Subspace of W holds
( b5 = im T iff [#] b5 = T .: ([#] V) );

theorem :: RANKNULL:11
for F being Field
for W, V being VectSp of F
for T being linear-transformation of V,W holds 0. V in ker T
proof
let F be Field; ::_thesis: for W, V being VectSp of F
for T being linear-transformation of V,W holds 0. V in ker T
let W, V be VectSp of F; ::_thesis: for T being linear-transformation of V,W holds 0. V in ker T
let T be linear-transformation of V,W; ::_thesis: 0. V in ker T
 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  0. V in ker T by Th10; ::_thesis: verum
end;

theorem Th12: :: RANKNULL:12
for F being Field
for W, V being VectSp of F
for T being linear-transformation of V,W
for X being Subset of V holds T .: X is Subset of (im T)
proof
let F be Field; ::_thesis: for W, V being VectSp of F
for T being linear-transformation of V,W
for X being Subset of V holds T .: X is Subset of (im T)
let W, V be VectSp of F; ::_thesis: for T being linear-transformation of V,W
for X being Subset of V holds T .: X is Subset of (im T)
let T be linear-transformation of V,W; ::_thesis: for X being Subset of V holds T .: X is Subset of (im T)
let X be Subset of V; ::_thesis: T .: X is Subset of (im T)
 [#] (im T) = T .: ([#] V) by Def2;
hence  T .: X is Subset of (im T) by RELAT_1:123; ::_thesis: verum
end;

theorem Th13: :: RANKNULL:13
for F being Field
for W, V being VectSp of F
for T being linear-transformation of V,W
for y being Element of W holds
( y in im T iff ex x being Element of V st y = T . x )
proof
let F be Field; ::_thesis: for W, V being VectSp of F
for T being linear-transformation of V,W
for y being Element of W holds
( y in im T iff ex x being Element of V st y = T . x )
let W, V be VectSp of F; ::_thesis: for T being linear-transformation of V,W
for y being Element of W holds
( y in im T iff ex x being Element of V st y = T . x )
let T be linear-transformation of V,W; ::_thesis: for y being Element of W holds
( y in im T iff ex x being Element of V st y = T . x )
let y be Element of W; ::_thesis: ( y in im T iff ex x being Element of V st y = T . x )
A1: ( y in im T implies ex x being Element of V st y = T . x )
proof
assume  y in im T ; ::_thesis: ex x being Element of V st y = T . x
then reconsider y = 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 = x as Element of V by A2;
take  x ; ::_thesis: y = T . x
thus  y = T . x by A3; ::_thesis: verum
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 ; ::_thesis: y in im T
 dom T = [#] V by Th7;
then  y in T .: ([#] V) by A4, FUNCT_1:def_6;
then  y in [#] (im T) by Def2;
hence  y in im T by STRUCT_0:def_5; ::_thesis: verum
end;
hence  ( y in im T iff ex x being Element of V st y = T . x ) by A1; ::_thesis: verum
end;

theorem :: RANKNULL:14
for F being Field
for V, W being VectSp of F
for T being linear-transformation of V,W
for x being Element of (ker T) holds T . x = 0. W
proof
let F be Field; ::_thesis: for V, W being VectSp of F
for T being linear-transformation of V,W
for x being Element of (ker T) holds T . x = 0. W
let V, W be VectSp of F; ::_thesis: for T being linear-transformation of V,W
for x being Element of (ker T) holds T . x = 0. W
let T be linear-transformation of V,W; ::_thesis: for x being Element of (ker T) holds T . x = 0. W
let x be Element of (ker T); ::_thesis: T . x = 0. W
reconsider y = x as Element of V by VECTSP_4:10;
 y in ker T by STRUCT_0:def_5;
hence  T . x = 0. W by Th10; ::_thesis: verum
end;

theorem Th15: :: RANKNULL:15
for F being Field
for W, V being VectSp of F
for T being linear-transformation of V,W st T is one-to-one holds
ker T = (0). V
proof
let F be Field; ::_thesis: for W, V being VectSp of F
for T being linear-transformation of V,W st T is one-to-one holds
ker T = (0). V
let W, V be VectSp of F; ::_thesis: for T being linear-transformation of V,W st T is one-to-one holds
ker T = (0). V
let T be linear-transformation of V,W; ::_thesis: ( T is one-to-one implies ker T = (0). V )
reconsider Z = (0). V as Subspace of ker T by VECTSP_4:39;
assume A1: T is one-to-one ; ::_thesis: ker T = (0). V
 for v being Element of (ker T) holds v in Z
proof
let v be Element of (ker T); ::_thesis: v in Z
A2: v in ker T by STRUCT_0:def_5;
assume  not v in Z ; ::_thesis: contradiction
then A3: not v = 0. V by VECTSP_4:35;
A4: ( T . (0. V) = 0. W & dom T = [#] V ) by Th7, Th9;
reconsider v = v as Element of V by VECTSP_4:10;
 T . v = 0. W by A2, Th10;
hence  contradiction by A1, A3, A4, FUNCT_1:def_4; ::_thesis: verum
end;
hence  ker T = (0). V by VECTSP_4:32; ::_thesis: verum
end;

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

theorem Th17: :: RANKNULL:17
for F being Field
for W, V being VectSp of F
for T being linear-transformation of V,W
for x, y being Element of V st T . x = T . y holds
x - y in ker T
proof
let F be Field; ::_thesis: for W, V being VectSp of F
for T being linear-transformation of V,W
for x, y being Element of V st T . x = T . y holds
x - y in ker T
let W, V be VectSp of F; ::_thesis: for T being linear-transformation of V,W
for x, y being Element of V st T . x = T . y holds
x - y in ker T
let T be linear-transformation of V,W; ::_thesis: for x, y being Element of V st T . x = T . y holds
x - y in ker T
let x, y be Element of V; ::_thesis: ( T . x = T . y implies x - y in ker T )
assume A1: T . x = T . y ; ::_thesis: x - y in ker T
T . (x - y) = (T . x) - (T . y) by Th8
.= 0. W by A1, VECTSP_1:19 ;
hence  x - y in ker T by Th10; ::_thesis: verum
end;

theorem Th18: :: RANKNULL:18
for F being Field
for V being VectSp of F
for A being Subset of V
for x, y being Element of V st x - y in Lin A holds
x in Lin (A \/ {y})
proof
let F be Field; ::_thesis: for V being VectSp of F
for A being Subset of V
for x, y being Element of V st x - y in Lin A holds
x in Lin (A \/ {y})
let V be VectSp of F; ::_thesis: for A being Subset of V
for x, y being Element of V st x - y in Lin A holds
x in Lin (A \/ {y})
let A be Subset of V; ::_thesis: for x, y being Element of V st x - y in Lin A holds
x in Lin (A \/ {y})
let x, y be Element of V; ::_thesis: ( x - y in Lin A implies x in Lin (A \/ {y}) )
assume A1: x - y in Lin A ; ::_thesis: x in Lin (A \/ {y})
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  x in Lin (A \/ {y}) by A1, A3, A2, VECTSP_5:1; ::_thesis: verum
end;

begin

theorem Th19: :: RANKNULL:19
for F being Field
for V, W being VectSp of F
for X being Subset of V st V is Subspace of W holds
X is Subset of W
proof
let F be Field; ::_thesis: for V, W being VectSp of F
for X being Subset of V st V is Subspace of W holds
X is Subset of W
let V, W be VectSp of F; ::_thesis: for X being Subset of V st V is Subspace of W holds
X is Subset of W
let X be Subset of V; ::_thesis: ( V is Subspace of W implies X is Subset of W )
assume  V is Subspace of W ; ::_thesis: X is Subset of W
then A1: [#] V c= [#] W by VECTSP_4:def_2;
 X c= [#] W
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in [#] W )
assume  x in X ; ::_thesis: x in [#] W
then  x in [#] V ;
hence  x in [#] W by A1; ::_thesis: verum
end;
hence  X is Subset of W ; ::_thesis: verum
end;

theorem Th20: :: RANKNULL:20
for F being Field
for V being VectSp of F
for A being Subset of V st A is linearly-independent holds
A is Basis of Lin A
proof
let F be Field; ::_thesis: for V being VectSp of F
for A being Subset of V st A is linearly-independent holds
A is Basis of Lin A
let V be VectSp of F; ::_thesis: for A being Subset of V st A is linearly-independent holds
A is Basis of Lin A
let A be Subset of V; ::_thesis: ( A is linearly-independent implies A is Basis of Lin A )
assume A1: A is linearly-independent ; ::_thesis: A is Basis of Lin A
 A c= [#] (Lin A)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in [#] (Lin A) )
assume A2: x in A ; ::_thesis: x in [#] (Lin A)
reconsider x = x as Element of V by A2;
 x in Lin A by A2, VECTSP_7:8;
hence  x in [#] (Lin A) by STRUCT_0:def_5; ::_thesis: verum
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  A is Basis of Lin A by A3, VECTSP_7:def_3; ::_thesis: verum
end;

theorem Th21: :: RANKNULL:21
for F being Field
for V being VectSp of F
for A being Subset of V
for x being Element of V st x in Lin A & not x in A holds
A \/ {x} is linearly-dependent
proof
let F be Field; ::_thesis: for V being VectSp of F
for A being Subset of V
for x being Element of V st x in Lin A & not x in A holds
A \/ {x} is linearly-dependent
let V be VectSp of F; ::_thesis: for A being Subset of V
for x being Element of V st x in Lin A & not x in A holds
A \/ {x} is linearly-dependent
let A be Subset of V; ::_thesis: for x being Element of V st x in Lin A & not x in A holds
A \/ {x} is linearly-dependent
let x be Element of V; ::_thesis: ( x in Lin A & not x in A implies A \/ {x} is linearly-dependent )
assume that
A1: x in Lin A and
A2: not x in A ; ::_thesis: A \/ {x} is linearly-dependent
percases ( A is linearly-independent or A is linearly-dependent ) ;
supposeA3: A is linearly-independent ; ::_thesis: A \/ {x} is linearly-dependent
 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 ; ::_thesis: contradiction
then  ex y being set st
( y in X & y in A9 ) by XBOOLE_0:3;
hence  contradiction by A2, TARSKI:def_1; ::_thesis: verum
end;
then  B is linearly-dependent by VECTSP_9:15;
hence  A \/ {x} is linearly-dependent by VECTSP_9:12; ::_thesis: verum
end;
suppose A is linearly-dependent ; ::_thesis: A \/ {x} is linearly-dependent
hence  A \/ {x} is linearly-dependent by VECTSP_7:1, XBOOLE_1:7; ::_thesis: verum
end;
end;
end;

theorem Th22: :: RANKNULL:22
for F being Field
for W, V being VectSp of F
for T being linear-transformation of V,W
for A being Subset of V
for 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 F be Field; ::_thesis: for W, V being VectSp of F
for T being linear-transformation of V,W
for A being Subset of V
for B being Basis of V st A is Basis of ker T & A c= B holds
T | (B \ A) is one-to-one
let W, V be VectSp of F; ::_thesis: for T being linear-transformation of V,W
for A being Subset of V
for B being Basis of V st A is Basis of ker T & A c= B holds
T | (B \ A) is one-to-one
let T be linear-transformation of V,W; ::_thesis: for A being Subset of V
for B being Basis of V st A is Basis of ker T & A c= B holds
T | (B \ A) is one-to-one
let A be Subset of V; ::_thesis: for B being Basis of V st A is Basis of ker T & A c= B holds
T | (B \ A) is one-to-one
let B be Basis of V; ::_thesis: ( A is Basis of ker T & A c= B implies T | (B \ A) is one-to-one )
assume that
A1: A is Basis of ker T and
A2: A c= B ; ::_thesis: T | (B \ A) is one-to-one
reconsider A9 = A as Subset of V ;
set f = T | (B \ A);
let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom (T | (B \ A)) or not x2 in dom (T | (B \ A)) or not (T | (B \ A)) . x1 = (T | (B \ A)) . x2 or x1 = x2 )
assume that
A3: x1 in dom (T | (B \ A)) and
A4: x2 in dom (T | (B \ A)) and
A5: (T | (B \ A)) . x1 = (T | (B \ A)) . x2 and
A6: x1 <> x2 ; ::_thesis: contradiction
 x2 in dom T by A4, RELAT_1:57;
then reconsider x2 = x2 as Element of V ;
 x1 in dom T by A3, RELAT_1:57;
then reconsider x1 = 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} ; ::_thesis: contradiction
percases ( x1 in A9 or x1 in {x2} ) by A9, XBOOLE_0:def_3;
suppose x1 in A9 ; ::_thesis: contradiction
hence  contradiction by A7, XBOOLE_0:def_5; ::_thesis: verum
end;
suppose x1 in {x2} ; ::_thesis: contradiction
hence  contradiction by A6, TARSKI:def_1; ::_thesis: verum
end;
end;
end;
A10: x2 in B \ A by A4;
then A11: (T | (B \ A)) . x2 = T . x2 by FUNCT_1:49;
reconsider A = A as Basis of ker T by A1;
A12: ker T = Lin A by VECTSP_7:def_3;
 (T | (B \ A)) . 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 ; :: according to TARSKI:def_3 ::_thesis: ( not z in {x1,x2} or z in B )
assume A15: z in {x1,x2} ; ::_thesis: z in B
percases ( z = x1 or z = x2 ) by A15, TARSKI:def_2;
suppose z = x1 ; ::_thesis: z in B
hence  z in B by A7, XBOOLE_0:def_5; ::_thesis: verum
end;
suppose z = x2 ; ::_thesis: z in B
hence  z in B by A10, XBOOLE_0:def_5; ::_thesis: verum
end;
end;
end;
then A16: A9 \/ {x1,x2} c= B by A2, XBOOLE_1:8;
 B is linearly-independent by VECTSP_7:def_3;
hence  contradiction by A13, A14, A8, A16, Th21, VECTSP_7:1; ::_thesis: verum
end;

theorem :: RANKNULL:23
for F being Field
for V being VectSp of F
for A being Subset of V
for l being Linear_Combination of A
for x being Element of V
for a being Element of F holds l +* (x,a) is Linear_Combination of A \/ {x}
proof
let F be Field; ::_thesis: for V being VectSp of F
for A being Subset of V
for l being Linear_Combination of A
for x being Element of V
for a being Element of F holds l +* (x,a) is Linear_Combination of A \/ {x}
let V be VectSp of F; ::_thesis: for A being Subset of V
for l being Linear_Combination of A
for x being Element of V
for a being Element of F holds l +* (x,a) is Linear_Combination of A \/ {x}
let A be Subset of V; ::_thesis: for l being Linear_Combination of A
for x being Element of V
for a being Element of F holds l +* (x,a) is Linear_Combination of A \/ {x}
let l be Linear_Combination of A; ::_thesis: for x being Element of V
for a being Element of F holds l +* (x,a) is Linear_Combination of A \/ {x}
let x be Element of V; ::_thesis: for a being Element of F holds l +* (x,a) is Linear_Combination of A \/ {x}
let a be Element of F; ::_thesis: l +* (x,a) is Linear_Combination of A \/ {x}
set m = l +* (x,a);
A1: dom (l +* (x,a)) = [#] V by FUNCT_2:def_1;
 rng (l +* (x,a)) c= [#] F
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (l +* (x,a)) or y in [#] F )
assume  y in rng (l +* (x,a)) ; ::_thesis: y in [#] F
then consider x9 being set  such that
A2: x9 in dom (l +* (x,a)) and
A3: (l +* (x,a)) . x9 = y by FUNCT_1:def_3;
A4: x9 in dom l by A1, A2, FUNCT_2:92;
percases ( x9 = x or x9 <> x ) ;
suppose x9 = x ; ::_thesis: y in [#] F
then  (l +* (x,a)) . x9 = a by A4, FUNCT_7:31;
hence  y in [#] F by A3; ::_thesis: verum
end;
supposeA5: x9 <> x ; ::_thesis: y in [#] F
A6: ( l . x9 in rng l & rng l c= [#] F ) by A4, FUNCT_1:3, FUNCT_2:92;
 (l +* (x,a)) . x9 = l . x9 by A5, FUNCT_7:32;
hence  y in [#] F by A3, A6; ::_thesis: verum
end;
end;
end;
then reconsider m = l +* (x,a) 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 (Carrier l) \/ {x} holds
m . v = 0. F
proof
let v be Element of V; ::_thesis: ( not v in (Carrier l) \/ {x} implies m . v = 0. F )
assume A7: not v in (Carrier l) \/ {x} ; ::_thesis: m . v = 0. F
 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  m . v = 0. F by A8; ::_thesis: verum
end;
then reconsider m = m as Linear_Combination of V by VECTSP_6:def_1;
A9: Carrier m c= (Carrier l) \/ {x}
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Carrier m or y in (Carrier l) \/ {x} )
assume  y in Carrier m ; ::_thesis: y in (Carrier l) \/ {x}
then consider z being Element of V such that
A10: y = z and
A11: m . z <> 0. F ;
percases ( z = x or z <> x ) ;
supposeA12: z = x ; ::_thesis: y in (Carrier l) \/ {x}
 ( x in {x} & {x} c= (Carrier l) \/ {x} ) by TARSKI:def_1, XBOOLE_1:7;
hence  y in (Carrier l) \/ {x} by A10, A12; ::_thesis: verum
end;
suppose z <> x ; ::_thesis: y in (Carrier l) \/ {x}
then  m . z = l . z by FUNCT_7:32;
then A13: z in Carrier l by A11;
 Carrier l c= (Carrier l) \/ {x} by XBOOLE_1:7;
hence  y in (Carrier l) \/ {x} by A10, A13; ::_thesis: verum
end;
end;
end;
 Carrier l c= A by VECTSP_6:def_4;
then  (Carrier l) \/ {x} c= A \/ {x} by XBOOLE_1:9;
then  Carrier m c= A \/ {x} by A9, XBOOLE_1:1;
hence  l +* (x,a) is Linear_Combination of A \/ {x} by VECTSP_6:def_4; ::_thesis: verum
end;

definition
let V be 1-sorted ;
let X be Subset of V;
funcV \ X ->  Subset of V equals :: RANKNULL:def 3
([#] V) \ X;
coherence
 ([#] V) \ X is Subset of V ;
end;

:: deftheorem  defines \ RANKNULL:def_3_:_
 for V being 1-sorted
for X being Subset of V holds V \ X = ([#] V) \ X;

definition
let F be Field;
let V be VectSp of F;
let l be Linear_Combination of V;
let X be Subset of V;
:: original: .:
redefine funcl .: X ->  Subset of F;
coherence
 l .: X is Subset of F
proof
 l .: X c= [#] F ;
hence  l .: X is Subset of F ; ::_thesis: verum
end;
end;

registration
let F be Field;
let V be VectSp of F;
cluster linearly-dependent for Element of K6( the carrier of V);
existence
 ex b1 being Subset of V st b1 is linearly-dependent
proof
reconsider S = {(0. V)} as Subset of V ;
take  S ; ::_thesis: S is linearly-dependent
 0. V in S by TARSKI:def_1;
hence  S is linearly-dependent by VECTSP_7:2; ::_thesis: verum
end;
end;

definition
let F be Field;
let V be VectSp of F;
let l be Linear_Combination of V;
let A be Subset of V;
funcl ! A ->  Linear_Combination of A equals :: RANKNULL:def 4
(l | A) +* ((V \ A) --> (0. F));
coherence
 (l | A) +* ((V \ A) --> (0. F)) is Linear_Combination of A
proof
set f = (l | A) +* ((V \ A) --> (0. F));
A1: dom ((l | A) +* ((V \ A) --> (0. 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 ((l | A) +* ((V \ A) --> (0. F))) = [#] V by A1, A2, XBOOLE_1:45;
A5: A \/ (([#] V) \ A) = [#] V by XBOOLE_1:45;
 rng ((l | A) +* ((V \ A) --> (0. F))) c= [#] F
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng ((l | A) +* ((V \ A) --> (0. F))) or y in [#] F )
assume  y in rng ((l | A) +* ((V \ A) --> (0. F))) ; ::_thesis: y in [#] F
then consider x being set  such that
A6: x in dom ((l | A) +* ((V \ A) --> (0. F))) and
A7: y = ((l | A) +* ((V \ A) --> (0. F))) . x by FUNCT_1:def_3;
reconsider x = x as Element of V by A1, A3, A2, A6, XBOOLE_1:45;
percases ( x in A or x in V \ A ) by A5, XBOOLE_0:def_3;
supposeA8: x in A ; ::_thesis: y in [#] F
then  not x in dom ((V \ A) --> (0. F)) by XBOOLE_0:def_5;
then A9: ((l | A) +* ((V \ A) --> (0. F))) . x = (l | A) . x by FUNCT_4:11;
 (l | A) . x = l . x by A8, FUNCT_1:49;
hence  y in [#] F by A7, A9; ::_thesis: verum
end;
supposeA10: x in V \ A ; ::_thesis: y in [#] F
then  x in dom ((V \ A) --> (0. F)) by FUNCOP_1:13;
then ((l | A) +* ((V \ A) --> (0. F))) . x = ((V \ A) --> (0. F)) . x by FUNCT_4:13
.= 0. F by A10, FUNCOP_1:7 ;
hence  y in [#] F by A7; ::_thesis: verum
end;
end;
end;
then reconsider f = (l | A) +* ((V \ A) --> (0. 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  }  ;
  {  v where v is Element of V : f . v <> 0. F  }  c= [#] V
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  v where v is Element of V : f . v <> 0. F  }  or x in [#] V )
assume  x in  {  v where v is Element of V : f . v <> 0. F  }  ; ::_thesis: x in [#] V
then  ex v being Element of V st
( x = v & f . v <> 0. F ) ;
hence  x in [#] V ; ::_thesis: verum
end;
then reconsider D =  {  v where v is Element of V : f . v <> 0. F  }  as Subset of V ;
set C = Carrier l;
 D c= Carrier l
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D or x in Carrier l )
assume  x in D ; ::_thesis: x in Carrier l
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__::_thesis:_not_v_in_V_\_A
assume A15: v in V \ A ; ::_thesis: contradiction
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; ::_thesis: verum
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  x in Carrier l by A11, A12, A16; ::_thesis: verum
end;
then reconsider D = D as finite Subset of V ;
take  D ; ::_thesis: for v being Element of V st not v in D holds
f . v = 0. F
thus  for v being Element of V st not v in D holds
f . v = 0. F ; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of V by VECTSP_6:def_1;
 Carrier f c= A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in A )
assume A17: x in Carrier f ; ::_thesis: x in A
reconsider x = x as Element of V by A17;
A18: f . x <> 0. F by A17, VECTSP_6:2;
now__::_thesis:_x_in_A
assume  not x in A ; ::_thesis: contradiction
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; ::_thesis: verum
end;
hence  x in A ; ::_thesis: verum
end;
hence  (l | A) +* ((V \ A) --> (0. F)) is Linear_Combination of A by VECTSP_6:def_4; ::_thesis: verum
end;
end;

:: deftheorem  defines ! RANKNULL:def_4_:_
 for F being Field
for V being VectSp of F
for l being Linear_Combination of V
for A being Subset of V holds l ! A = (l | A) +* ((V \ A) --> (0. F));

theorem Th24: :: RANKNULL:24
for F being Field
for V being VectSp of F
for l being Linear_Combination of V holds l = l ! (Carrier l)
proof
let F be Field; ::_thesis: for V being VectSp of F
for l being Linear_Combination of V holds l = l ! (Carrier l)
let V be VectSp of F; ::_thesis: for l being Linear_Combination of V holds l = l ! (Carrier l)
let l be Linear_Combination of V; ::_thesis: l = l ! (Carrier l)
set f = l | (Carrier l);
set g = (V \ (Carrier l)) --> (0. F);
set m = (l | (Carrier l)) +* ((V \ (Carrier l)) --> (0. F));
A1: dom ((V \ (Carrier l)) --> (0. F)) = V \ (Carrier l) by FUNCOP_1:13;
A2: dom l = [#] V by FUNCT_2:92;
then  dom (l | (Carrier l)) = Carrier l by RELAT_1:62;
then A3: (dom (l | (Carrier l))) \/ (dom ((V \ (Carrier l)) --> (0. F))) = [#] V by A1, XBOOLE_1:45;
A4: for x being set st x in dom l holds
l . x = ((l | (Carrier l)) +* ((V \ (Carrier l)) --> (0. F))) . x
proof
let x be set ; ::_thesis: ( x in dom l implies l . x = ((l | (Carrier l)) +* ((V \ (Carrier l)) --> (0. F))) . x )
assume  x in dom l ; ::_thesis: l . x = ((l | (Carrier l)) +* ((V \ (Carrier l)) --> (0. F))) . x
then reconsider x = x as Element of V ;
percases ( x in Carrier l or not x in Carrier l ) ;
supposeA5: x in Carrier l ; ::_thesis: l . x = ((l | (Carrier l)) +* ((V \ (Carrier l)) --> (0. F))) . x
then  not x in dom ((V \ (Carrier l)) --> (0. F)) by XBOOLE_0:def_5;
then  ((l | (Carrier l)) +* ((V \ (Carrier l)) --> (0. F))) . x = (l | (Carrier l)) . x by A3, FUNCT_4:def_1;
hence  l . x = ((l | (Carrier l)) +* ((V \ (Carrier l)) --> (0. F))) . x by A5, FUNCT_1:49; ::_thesis: verum
end;
supposeA6: not x in Carrier l ; ::_thesis: l . x = ((l | (Carrier l)) +* ((V \ (Carrier l)) --> (0. F))) . x
then  x in V \ (Carrier l) by XBOOLE_0:def_5;
then  ( ((l | (Carrier l)) +* ((V \ (Carrier l)) --> (0. F))) . x = ((V \ (Carrier l)) --> (0. F)) . x & ((V \ (Carrier l)) --> (0. F)) . x = 0. F ) by A1, A3, FUNCOP_1:7, FUNCT_4:def_1;
hence  l . x = ((l | (Carrier l)) +* ((V \ (Carrier l)) --> (0. F))) . x by A6; ::_thesis: verum
end;
end;
end;
 dom l = dom ((l | (Carrier l)) +* ((V \ (Carrier l)) --> (0. F))) by A2, A3, FUNCT_4:def_1;
hence  l = l ! (Carrier l) by A4, FUNCT_1:def_11; ::_thesis: verum
end;

Lm1:  for F being Field
for V being VectSp of F
for l being Linear_Combination of V
for X being Subset of V holds l .: X is finite
proof
let F be Field; ::_thesis: for V being VectSp of F
for l being Linear_Combination of V
for X being Subset of V holds l .: X is finite
let V be VectSp of F; ::_thesis: for l being Linear_Combination of V
for X being Subset of V holds l .: X is finite
let l be Linear_Combination of V; ::_thesis: for X being Subset of V holds l .: X is finite
let X be Subset of V; ::_thesis: l .: X is finite
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  l .: X is finite by FINSET_1:1, RELAT_1:111; ::_thesis: verum
end;

theorem Th25: :: RANKNULL:25
for F being Field
for V being VectSp of F
for l being Linear_Combination of V
for A being Subset of V
for v being Element of V st v in A holds
(l ! A) . v = l . v
proof
let F be Field; ::_thesis: for V being VectSp of F
for l being Linear_Combination of V
for A being Subset of V
for v being Element of V st v in A holds
(l ! A) . v = l . v
let V be VectSp of F; ::_thesis: for l being Linear_Combination of V
for A being Subset of V
for v being Element of V st v in A holds
(l ! A) . v = l . v
let l be Linear_Combination of V; ::_thesis: for A being Subset of V
for v being Element of V st v in A holds
(l ! A) . v = l . v
let A be Subset of V; ::_thesis: for v being Element of V st v in A holds
(l ! A) . v = l . v
let v be Element of V; ::_thesis: ( v in A implies (l ! A) . v = l . v )
assume A1: v in A ; ::_thesis: (l ! A) . v = l . v
 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  (l ! A) . v = l . v ; ::_thesis: verum
end;

theorem Th26: :: RANKNULL:26
for F being Field
for V being VectSp of F
for l being Linear_Combination of V
for A being Subset of V
for v being Element of V st not v in A holds
(l ! A) . v = 0. F
proof
let F be Field; ::_thesis: for V being VectSp of F
for l being Linear_Combination of V
for A being Subset of V
for v being Element of V st not v in A holds
(l ! A) . v = 0. F
let V be VectSp of F; ::_thesis: for l being Linear_Combination of V
for A being Subset of V
for v being Element of V st not v in A holds
(l ! A) . v = 0. F
let l be Linear_Combination of V; ::_thesis: for A being Subset of V
for v being Element of V st not v in A holds
(l ! A) . v = 0. F
let A be Subset of V; ::_thesis: for v being Element of V st not v in A holds
(l ! A) . v = 0. F
let v be Element of V; ::_thesis: ( not v in A implies (l ! A) . v = 0. F )
assume  not v in A ; ::_thesis: (l ! A) . v = 0. F
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  (l ! A) . v = 0. F ; ::_thesis: verum
end;

theorem Th27: :: RANKNULL:27
for F being Field
for V being VectSp of F
for A, B being Subset of V
for l being Linear_Combination of B st A c= B holds
l = (l ! A) + (l ! (B \ A))
proof
let F be Field; ::_thesis: for V being VectSp of F
for A, B being Subset of V
for l being Linear_Combination of B st A c= B holds
l = (l ! A) + (l ! (B \ A))
let V be VectSp of F; ::_thesis: for A, B being Subset of V
for l being Linear_Combination of B st A c= B holds
l = (l ! A) + (l ! (B \ A))
let A, B be Subset of V; ::_thesis: for l being Linear_Combination of B st A c= B holds
l = (l ! A) + (l ! (B \ A))
let l be Linear_Combination of B; ::_thesis: ( A c= B implies l = (l ! A) + (l ! (B \ A)) )
assume A1: A c= B ; ::_thesis: l = (l ! A) + (l ! (B \ A))
set r = (l ! A) + (l ! (B \ A));
let v be Element of V; :: according to FUNCT_2:def_8 ::_thesis: l . v = ((l ! A) + (l ! (B \ A))) . v
A2: ( not v in B or v in A or v in B \ A )
proof
assume A3: v in B ; ::_thesis: ( v in A or v in B \ A )
 B = A \/ (B \ A) by A1, XBOOLE_1:45;
hence  ( v in A or v in B \ A ) by A3, XBOOLE_0:def_3; ::_thesis: verum
end;
percases ( v in A or v in B \ A or not v in B ) by A2;
supposeA4: v in A ; ::_thesis: l . v = ((l ! A) + (l ! (B \ A))) . v
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 ((l ! A) + (l ! (B \ A))) . v = (l . v) + (0. F) by A5, VECTSP_6:22
.= l . v by RLVECT_1:4 ;
hence  l . v = ((l ! A) + (l ! (B \ A))) . v ; ::_thesis: verum
end;
supposeA6: v in B \ A ; ::_thesis: l . v = ((l ! A) + (l ! (B \ A))) . v
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 ((l ! A) + (l ! (B \ A))) . v = (0. F) + (l . v) by A7, VECTSP_6:22
.= l . v by RLVECT_1:4 ;
hence  l . v = ((l ! A) + (l ! (B \ A))) . v ; ::_thesis: verum
end;
supposeA8: not v in B ; ::_thesis: l . v = ((l ! A) + (l ! (B \ A))) . v
 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 ((l ! A) + (l ! (B \ A))) . v = (0. F) + (0. F) by A10, VECTSP_6:22
.= 0. F by RLVECT_1:4 ;
hence  l . v = ((l ! A) + (l ! (B \ A))) . v by A9; ::_thesis: verum
end;
end;
end;

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

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

theorem Th28: :: RANKNULL:28
for F being Field
for V being VectSp of F
for l being Linear_Combination of V
for X being Subset of V st X misses Carrier l holds
l .: X c= {(0. F)}
proof
let F be Field; ::_thesis: for V being VectSp of F
for l being Linear_Combination of V
for X being Subset of V st X misses Carrier l holds
l .: X c= {(0. F)}
let V be VectSp of F; ::_thesis: for l being Linear_Combination of V
for X being Subset of V st X misses Carrier l holds
l .: X c= {(0. F)}
let l be Linear_Combination of V; ::_thesis: for X being Subset of V st X misses Carrier l holds
l .: X c= {(0. F)}
let X be Subset of V; ::_thesis: ( X misses Carrier l implies l .: X c= {(0. F)} )
assume A1: X misses Carrier l ; ::_thesis: l .: X c= {(0. F)}
set M = l .: X;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in l .: X or y in {(0. F)} )
assume  y in l .: X ; ::_thesis: y in {(0. F)}
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 = x as Element of V by A2;
now__::_thesis:_not_l_._x_<>_0._F
assume  l . x <> 0. F ; ::_thesis: contradiction
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; ::_thesis: verum
end;
hence  y in {(0. F)} by A4, TARSKI:def_1; ::_thesis: verum
end;

definition
let F be Field;
let V, W be VectSp of F;
let l be Linear_Combination of V;
let T be linear-transformation of V,W;
funcT @ l ->  Linear_Combination of W means :Def5: :: RANKNULL:def 5
 for w being Element of W holds it . w = Sum (l .: (T " {w}));
existence
 ex b1 being Linear_Combination of W st
for w being Element of W holds b1 . w = Sum (l .: (T " {w}))
proof
defpred S1[ 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 S1[x,y]
proof
let x be set ; ::_thesis: ( x in [#] W implies ex y being set st S1[x,y] )
assume  x in [#] W ; ::_thesis: ex y being set st S1[x,y]
then reconsider x = x as Element of W ;
take  Sum (l .: (T " {x})) ; ::_thesis: S1[x, Sum (l .: (T " {x}))]
thus  S1[x, Sum (l .: (T " {x}))] ; ::_thesis: verum
end;
consider f being Function such that
A2: dom f = [#] W and
A3: for x being set st x in [#] W holds
S1[x,f . x] from CLASSES1:sch_1(A1);
A4: rng f c= [#] F
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in [#] F )
assume  y in rng f ; ::_thesis: y in [#] 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  y in [#] F by A6; ::_thesis: verum
end;
A7: for w being Element of W holds f . w = Sum (l .: (T " {w}))
proof
let w be Element of W; ::_thesis: f . w = Sum (l .: (T " {w}))
 ex w9 being Element of W st
( w = w9 & f . w = Sum (l .: (T " {w9})) ) by A3;
hence  f . w = Sum (l .: (T " {w})) ; ::_thesis: verum
end;
reconsider f = 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  }  ;
  {  w where w is Element of W : f . w <> 0. F  }  c= [#] W
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  w where w is Element of W : f . w <> 0. F  }  or x in [#] W )
assume  x in  {  w where w is Element of W : f . w <> 0. F  }  ; ::_thesis: x in [#] W
then  ex w being Element of W st
( x = w & f . w <> 0. F ) ;
hence  x in [#] W ; ::_thesis: verum
end;
then reconsider X =  {  w where w is Element of W : f . w <> 0. F  }  as Subset of W ;
set C = Carrier l;
reconsider TC = T .: (Carrier l) as Subset of W ;
 X c= TC
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in TC )
assume  x in X ; ::_thesis: x in TC
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 ; ::_thesis: contradiction
then A11: l .: (T " {w}) c= {(0. F)} by Th28;
 Sum (l .: (T " {w})) = 0. F
proof
percases ( l .: (T " {w}) = {} F or l .: (T " {w}) <> {} F ) ;
suppose l .: (T " {w}) = {} F ; ::_thesis: Sum (l .: (T " {w})) = 0. F
hence  Sum (l .: (T " {w})) = 0. F by RLVECT_2:8; ::_thesis: verum
end;
supposeA12: l .: (T " {w}) <> {} F ; ::_thesis: Sum (l .: (T " {w})) = 0. F
A13: {(0. F)} c= l .: (T " {w})
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in {(0. F)} or y in l .: (T " {w}) )
assume  y in {(0. F)} ; ::_thesis: y in l .: (T " {w})
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  y in l .: (T " {w}) by A11, A14, TARSKI:def_1; ::_thesis: verum
end;
 l .: (T " {w}) c= {(0. F)} by A10, Th28;
then  l .: (T " {w}) = {(0. F)} by A13, XBOOLE_0:def_10;
hence  Sum (l .: (T " {w})) = 0. F by RLVECT_2:9; ::_thesis: verum
end;
end;
end;
hence  contradiction by A7, A9; ::_thesis: verum
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 = 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  x in TC by A8, A16, A17, FUNCT_1:def_6; ::_thesis: verum
end;
then reconsider X = X as finite Subset of W ;
take  X ; ::_thesis: for w being Element of W st not w in X holds
f . w = 0. F
thus  for w being Element of W st not w in X holds
f . w = 0. F ; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of W by VECTSP_6:def_1;
take  f ; ::_thesis: for w being Element of W holds f . w = Sum (l .: (T " {w}))
 for w being Element of W holds f . w = Sum (l .: (T " {w}))
proof
let w be Element of W; ::_thesis: f . w = Sum (l .: (T " {w}))
 ex w9 being Element of W st
( w = w9 & f . w = Sum (l .: (T " {w9})) ) by A3;
hence  f . w = Sum (l .: (T " {w})) ; ::_thesis: verum
end;
hence  for w being Element of W holds f . w = Sum (l .: (T " {w})) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Linear_Combination of W st ( for w being Element of W holds b1 . w = Sum (l .: (T " {w})) ) & ( for w being Element of W holds b2 . w = Sum (l .: (T " {w})) ) holds
b1 = b2
proof
let f, g be Linear_Combination of W; ::_thesis: ( ( for w being Element of W holds f . w = Sum (l .: (T " {w})) ) & ( for w being Element of W holds g . w = Sum (l .: (T " {w})) ) implies f = g )
assume 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})) ; ::_thesis: f = g
A20: for x being set st x in dom f holds
f . x = g . x
proof
let x be set ; ::_thesis: ( x in dom f implies f . x = g . x )
assume  x in dom f ; ::_thesis: f . x = g . x
then reconsider x = x as Element of W ;
 f . x = Sum (l .: (T " {x})) by A18;
hence  f . x = g . x by A19; ::_thesis: verum
end;
 ( dom f = [#] W & dom g = [#] W ) by FUNCT_2:92;
hence  f = g by A20, FUNCT_1:def_11; ::_thesis: verum
end;
end;

:: deftheorem Def5 defines @ RANKNULL:def_5_:_
 for F being Field
for V, W being VectSp of F
for l being Linear_Combination of V
for T being linear-transformation of V,W
for b6 being Linear_Combination of W holds
( b6 = T @ l iff for w being Element of W holds b6 . w = Sum (l .: (T " {w})) );

theorem Th29: :: RANKNULL:29
for F being Field
for W, V being VectSp of F
for T being linear-transformation of V,W
for l being Linear_Combination of V holds T @ l is Linear_Combination of T .: (Carrier l)
proof
let F be Field; ::_thesis: for W, V being VectSp of F
for T being linear-transformation of V,W
for l being Linear_Combination of V holds T @ l is Linear_Combination of T .: (Carrier l)
let W, V be VectSp of F; ::_thesis: for T being linear-transformation of V,W
for l being Linear_Combination of V holds T @ l is Linear_Combination of T .: (Carrier l)
let T be linear-transformation of V,W; ::_thesis: for l being Linear_Combination of V holds T @ l is Linear_Combination of T .: (Carrier l)
let l be Linear_Combination of V; ::_thesis: T @ l is Linear_Combination of T .: (Carrier l)
 Carrier (T @ l) c= T .: (Carrier l)
proof
let w be set ; :: according to TARSKI:def_3 ::_thesis: ( not w in Carrier (T @ l) or w in T .: (Carrier l) )
assume A1: w in Carrier (T @ l) ; ::_thesis: w in T .: (Carrier l)
reconsider w = w as Element of W by A1;
A2: (T @ l) . w <> 0. F by A1, VECTSP_6:2;
now__::_thesis:_not_T_"_{w}_misses_Carrier_l
assume A3: T " {w} misses Carrier l ; ::_thesis: contradiction
then A4: l .: (T " {w}) c= {(0. F)} by Th28;
 Sum (l .: (T " {w})) = 0. F
proof
percases ( l .: (T " {w}) = {} F or l .: (T " {w}) <> {} F ) ;
suppose l .: (T " {w}) = {} F ; ::_thesis: Sum (l .: (T " {w})) = 0. F
hence  Sum (l .: (T " {w})) = 0. F by RLVECT_2:8; ::_thesis: verum
end;
supposeA5: l .: (T " {w}) <> {} F ; ::_thesis: Sum (l .: (T " {w})) = 0. F
A6: {(0. F)} c= l .: (T " {w})
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in {(0. F)} or y in l .: (T " {w}) )
assume  y in {(0. F)} ; ::_thesis: y in l .: (T " {w})
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  y in l .: (T " {w}) by A4, A7, TARSKI:def_1; ::_thesis: verum
end;
 l .: (T " {w}) c= {(0. F)} by A3, Th28;
then  l .: (T " {w}) = {(0. F)} by A6, XBOOLE_0:def_10;
hence  Sum (l .: (T " {w})) = 0. F by RLVECT_2:9; ::_thesis: verum
end;
end;
end;
hence  contradiction by A2, Def5; ::_thesis: verum
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 = x as Element of V by A8;
 T . x = w by A11, TARSKI:def_1;
hence  w in T .: (Carrier l) by A9, A10, FUNCT_1:def_6; ::_thesis: verum
end;
hence  T @ l is Linear_Combination of T .: (Carrier l) by VECTSP_6:def_4; ::_thesis: verum
end;

theorem Th30: :: RANKNULL:30
for F being Field
for W, V being VectSp of F
for T being linear-transformation of V,W
for l being Linear_Combination of V holds Carrier (T @ l) c= T .: (Carrier l)
proof
let F be Field; ::_thesis: for W, V being VectSp of F
for T being linear-transformation of V,W
for l being Linear_Combination of V holds Carrier (T @ l) c= T .: (Carrier l)
let W, V be VectSp of F; ::_thesis: for T being linear-transformation of V,W
for l being Linear_Combination of V holds Carrier (T @ l) c= T .: (Carrier l)
let T be linear-transformation of V,W; ::_thesis: for l being Linear_Combination of V holds Carrier (T @ l) c= T .: (Carrier l)
let l be Linear_Combination of V; ::_thesis: Carrier (T @ l) c= T .: (Carrier l)
 T @ l is Linear_Combination of T .: (Carrier l) by Th29;
hence  Carrier (T @ l) c= T .: (Carrier l) by VECTSP_6:def_4; ::_thesis: verum
end;

theorem Th31: :: RANKNULL:31
for F being Field
for V being VectSp of F
for l, m being Linear_Combination of V st Carrier l misses Carrier m holds
Carrier (l + m) = (Carrier l) \/ (Carrier m)
proof
let F be Field; ::_thesis: for V being VectSp of F
for l, m being Linear_Combination of V st Carrier l misses Carrier m holds
Carrier (l + m) = (Carrier l) \/ (Carrier m)
let V be VectSp of F; ::_thesis: for l, m being Linear_Combination of V st Carrier l misses Carrier m holds
Carrier (l + m) = (Carrier l) \/ (Carrier m)
let l, m be Linear_Combination of V; ::_thesis: ( Carrier l misses Carrier m implies Carrier (l + m) = (Carrier l) \/ (Carrier m) )
assume A1: Carrier l misses Carrier m ; ::_thesis: Carrier (l + m) = (Carrier l) \/ (Carrier m)
thus  Carrier (l + m) c= (Carrier l) \/ (Carrier m) by VECTSP_6:23; :: according to XBOOLE_0:def_10 ::_thesis: (Carrier l) \/ (Carrier m) c= Carrier (l + m)
thus  (Carrier l) \/ (Carrier m) c= Carrier (l + m) ::_thesis: verum
proof
let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in (Carrier l) \/ (Carrier m) or v in Carrier (l + m) )
assume A2: v in (Carrier l) \/ (Carrier m) ; ::_thesis: v in Carrier (l + m)
percases ( v in Carrier l or v in Carrier m ) by A2, XBOOLE_0:def_3;
supposeA3: v in Carrier l ; ::_thesis: v in Carrier (l + m)
then reconsider v = 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  v in Carrier (l + m) by A4; ::_thesis: verum
end;
supposeA5: v in Carrier m ; ::_thesis: v in Carrier (l + m)
then reconsider v = 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  v in Carrier (l + m) by A6; ::_thesis: verum
end;
end;
end;
end;

theorem Th32: :: RANKNULL:32
for F being Field
for V being VectSp of F
for l, m being Linear_Combination of V st Carrier l misses Carrier m holds
Carrier (l - m) = (Carrier l) \/ (Carrier m)
proof
let F be Field; ::_thesis: for V being VectSp of F
for l, m being Linear_Combination of V st Carrier l misses Carrier m holds
Carrier (l - m) = (Carrier l) \/ (Carrier m)
let V be VectSp of F; ::_thesis: for l, m being Linear_Combination of V st Carrier l misses Carrier m holds
Carrier (l - m) = (Carrier l) \/ (Carrier m)
let l, m be Linear_Combination of V; ::_thesis: ( Carrier l misses Carrier m implies Carrier (l - m) = (Carrier l) \/ (Carrier m) )
assume A1: Carrier l misses Carrier m ; ::_thesis: Carrier (l - m) = (Carrier l) \/ (Carrier m)
 Carrier (- m) = Carrier m by VECTSP_6:38;
hence  Carrier (l - m) = (Carrier l) \/ (Carrier m) by A1, Th31; ::_thesis: verum
end;

theorem Th33: :: RANKNULL:33
for F being Field
for V being VectSp of F
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 F be Field; ::_thesis: for V being VectSp of F
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)
let V be VectSp of F; ::_thesis: 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)
let A, B be Subset of V; ::_thesis: ( A c= B & B is Basis of V implies V is_the_direct_sum_of Lin A, Lin (B \ A) )
assume that
A1: A c= B and
A2: B is Basis of V ; ::_thesis: V is_the_direct_sum_of Lin A, Lin (B \ A)
A3: (Lin A) /\ (Lin (B \ A)) = (0). V
proof
set U = (Lin A) /\ (Lin (B \ A));
reconsider W = (0). V as strict Subspace of (Lin A) /\ (Lin (B \ A)) by VECTSP_4:39;
 for v being Element of ((Lin A) /\ (Lin (B \ A))) holds v in W
proof
let v be Element of ((Lin A) /\ (Lin (B \ A))); ::_thesis: v in W
A4: B is linearly-independent by A2, VECTSP_7:def_3;
A5: v in (Lin A) /\ (Lin (B \ A)) 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  v in W by A6, VECTSP_4:35; ::_thesis: verum
end;
hence  (Lin A) /\ (Lin (B \ A)) = (0). V by VECTSP_4:32; ::_thesis: verum
end;
 (Omega). V = (Lin A) + (Lin (B \ A))
proof
set U = (Lin A) + (Lin (B \ A));
A11: [#] V c= [#] ((Lin A) + (Lin (B \ A)))
proof
let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in [#] V or v in [#] ((Lin A) + (Lin (B \ A))) )
assume  v in [#] V ; ::_thesis: v in [#] ((Lin A) + (Lin (B \ A)))
then reconsider v = 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 = (l ! A) + (l ! (B \ A)) 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 (l ! A) ; ::_thesis: ex v2 being Element of V st
( Sum (l ! A) in Lin A & v2 in Lin (B \ A) & v = (Sum (l ! A)) + v2 )
take  Sum (l ! (B \ A)) ; ::_thesis: ( Sum (l ! A) in Lin A & Sum (l ! (B \ A)) in Lin (B \ A) & v = (Sum (l ! A)) + (Sum (l ! (B \ A))) )
thus  ( Sum (l ! A) in Lin A & Sum (l ! (B \ A)) in Lin (B \ A) & v = (Sum (l ! A)) + (Sum (l ! (B \ A))) ) by A12, A13, VECTSP_6:44, VECTSP_7:7; ::_thesis: verum
end;
then  v in (Lin A) + (Lin (B \ A)) by VECTSP_5:1;
hence  v in [#] ((Lin A) + (Lin (B \ A))) by STRUCT_0:def_5; ::_thesis: verum
end;
 [#] ((Lin A) + (Lin (B \ A))) c= [#] V by VECTSP_4:def_2;
then  [#] ((Lin A) + (Lin (B \ A))) = [#] V by A11, XBOOLE_0:def_10;
hence  (Omega). V = (Lin A) + (Lin (B \ A)) by VECTSP_4:29; ::_thesis: verum
end;
hence  V is_the_direct_sum_of Lin A, Lin (B \ A) by A3, VECTSP_5:def_4; ::_thesis: verum
end;

theorem Th34: :: RANKNULL:34
for F being Field
for W, V being VectSp of F
for T being linear-transformation of V,W
for A being Subset of V
for l being Linear_Combination of A
for 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 F be Field; ::_thesis: for W, V being VectSp of F
for T being linear-transformation of V,W
for A being Subset of V
for l being Linear_Combination of A
for 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 )
let W, V be VectSp of F; ::_thesis: for T being linear-transformation of V,W
for A being Subset of V
for l being Linear_Combination of A
for 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 )
let T be linear-transformation of V,W; ::_thesis: for A being Subset of V
for l being Linear_Combination of A
for 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 )
let A be Subset of V; ::_thesis: for l being Linear_Combination of A
for 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 )
let l be Linear_Combination of A; ::_thesis: for 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 )
let v be Element of V; ::_thesis: ( T | A is one-to-one & v in A implies ex X being Subset of V st
( X misses A & T " {(T . v)} = {v} \/ X ) )
assume that
A1: T | A is one-to-one and
A2: v in A ; ::_thesis: ex X being Subset of V st
( X misses A & T " {(T . v)} = {v} \/ X )
set X = (T " {(T . v)}) \ {v};
A3: (T " {(T . v)}) \ {v} misses A
proof
 dom T = [#] V by Th7;
then A4: dom (T | A) = A by RELAT_1:62;
assume  (T " {(T . v)}) \ {v} meets A ; ::_thesis: contradiction
then consider x being set  such that
A5: x in (T " {(T . v)}) \ {v} 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  contradiction by A1, A2, A6, A7, A4, FUNCT_1:def_4; ::_thesis: verum
end;
take  (T " {(T . v)}) \ {v} ; ::_thesis: ( (T " {(T . v)}) \ {v} misses A & T " {(T . v)} = {v} \/ ((T " {(T . v)}) \ {v}) )
 {v} c= T " {(T . v)}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {v} or x in T " {(T . v)} )
assume  x in {v} ; ::_thesis: x in T " {(T . v)}
then A9: x = v by TARSKI:def_1;
 ( dom T = [#] V & T . v in {(T . v)} ) by Th7, TARSKI:def_1;
hence  x in T " {(T . v)} by A9, FUNCT_1:def_7; ::_thesis: verum
end;
hence  ( (T " {(T . v)}) \ {v} misses A & T " {(T . v)} = {v} \/ ((T " {(T . v)}) \ {v}) ) by A3, XBOOLE_1:45; ::_thesis: verum
end;

theorem Th35: :: RANKNULL:35
for F being Field
for V being VectSp of F
for l being Linear_Combination of V
for X being Subset of V st X misses Carrier l & X <> {} holds
l .: X = {(0. F)}
proof
let F be Field; ::_thesis: for V being VectSp of F
for l being Linear_Combination of V
for X being Subset of V st X misses Carrier l & X <> {} holds
l .: X = {(0. F)}
let V be VectSp of F; ::_thesis: for l being Linear_Combination of V
for X being Subset of V st X misses Carrier l & X <> {} holds
l .: X = {(0. F)}
let l be Linear_Combination of V; ::_thesis: for X being Subset of V st X misses Carrier l & X <> {} holds
l .: X = {(0. F)}
let X be Subset of V; ::_thesis: ( X misses Carrier l & X <> {} implies l .: X = {(0. F)} )
assume that
A1: X misses Carrier l and
A2: X <> {} ; ::_thesis: l .: X = {(0. F)}
 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  l .: X = {(0. F)} by A3, ZFMISC_1:33; ::_thesis: verum
end;

theorem Th36: :: RANKNULL:36
for F being Field
for V, W being VectSp of F
for T being linear-transformation of V,W
for l being Linear_Combination of V
for w being Element of W st w in Carrier (T @ l) holds
T " {w} meets Carrier l
proof
let F be Field; ::_thesis: for V, W being VectSp of F
for T being linear-transformation of V,W
for l being Linear_Combination of V
for w being Element of W st w in Carrier (T @ l) holds
T " {w} meets Carrier l
let V, W be VectSp of F; ::_thesis: for T being linear-transformation of V,W
for l being Linear_Combination of V
for w being Element of W st w in Carrier (T @ l) holds
T " {w} meets Carrier l
let T be linear-transformation of V,W; ::_thesis: for l being Linear_Combination of V
for w being Element of W st w in Carrier (T @ l) holds
T " {w} meets Carrier l
let l be Linear_Combination of V; ::_thesis: for w being Element of W st w in Carrier (T @ l) holds
T " {w} meets Carrier l
let w be Element of W; ::_thesis: ( w in Carrier (T @ l) implies T " {w} meets Carrier l )
assume  w in Carrier (T @ l) ; ::_thesis: T " {w} meets Carrier l
then A1: (T @ l) . w <> 0. F by VECTSP_6:2;
assume A2: T " {w} misses Carrier l ; ::_thesis: contradiction
percases ( T " {w} = {} or T " {w} <> {} ) ;
suppose T " {w} = {} ; ::_thesis: contradiction
then  Sum (l .: (T " {w})) = Sum ({} F)
.= 0. F by RLVECT_2:8 ;
hence  contradiction by A1, Def5; ::_thesis: verum
end;
suppose T " {w} <> {} ; ::_thesis: contradiction
then  l .: (T " {w}) = {(0. F)} by A2, Th35;
then  Sum (l .: (T " {w})) = 0. F by RLVECT_2:9;
hence  contradiction by A1, Def5; ::_thesis: verum
end;
end;
end;

theorem Th37: :: RANKNULL:37
for F being Field
for W, V being VectSp of F
for T being linear-transformation of V,W
for l being Linear_Combination of V
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 F be Field; ::_thesis: for W, V being VectSp of F
for T being linear-transformation of V,W
for l being Linear_Combination of V
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
let W, V be VectSp of F; ::_thesis: for T being linear-transformation of V,W
for l being Linear_Combination of V
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
let T be linear-transformation of V,W; ::_thesis: for l being Linear_Combination of V
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
let l be Linear_Combination of V; ::_thesis: 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
let v be Element of V; ::_thesis: ( T | (Carrier l) is one-to-one & v in Carrier l implies (T @ l) . (T . v) = l . v )
assume that
A1: T | (Carrier l) is one-to-one and
A2: v in Carrier l ; ::_thesis: (T @ l) . (T . v) = l . v
consider X being Subset of V such that
A3: X misses Carrier l and
A4: T " {(T . v)} = {v} \/ X by A1, A2, Th34;
percases ( X = {} or X <> {} ) ;
supposeA5: X = {} ; ::_thesis: (T @ l) . (T . v) = l . v
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  (T @ l) . (T . v) = l . v by Def5; ::_thesis: verum
end;
supposeA7: X <> {} ; ::_thesis: (T @ l) . (T . v) = l . v
A8: l .: X c= {(0. F)}
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in l .: X or y in {(0. F)} )
assume  y in l .: X ; ::_thesis: y in {(0. F)}
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__::_thesis:_not_x_in_Carrier_l
assume  x in Carrier l ; ::_thesis: contradiction
then  x in (Carrier l) /\ X by A10, XBOOLE_0:def_4;
hence  contradiction by A3, XBOOLE_0:def_7; ::_thesis: verum
end;
reconsider x = x as Element of V by A9;
 l . x = 0. F by A12;
hence  y in {(0. F)} by A11, TARSKI:def_1; ::_thesis: verum
end;
A13: l .: X misses l .: {v}
proof
assume  l .: X meets l .: {v} ; ::_thesis: contradiction
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  contradiction by A2, A17, VECTSP_6:2; ::_thesis: verum
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__::_thesis:_not_y_in_Carrier_l
assume  y in Carrier l ; ::_thesis: contradiction
then  y in (Carrier l) /\ X by A19, XBOOLE_0:def_4;
hence  contradiction by A3, XBOOLE_0:def_7; ::_thesis: verum
end;
reconsider y = y as Element of V by A19;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(0. F)} or x in l .: X )
assume  x in {(0. F)} ; ::_thesis: x in l .: X
then  x = 0. F by TARSKI:def_1;
then  l . y = x by A20;
hence  x in l .: X by A18, A19, FUNCT_1:def_6; ::_thesis: verum
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  (T @ l) . (T . v) = l . v by Def5; ::_thesis: verum
end;
end;
end;

theorem Th38: :: RANKNULL:38
for F being Field
for W, V being VectSp of F
for T being linear-transformation of V,W
for l being Linear_Combination of V
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 F be Field; ::_thesis: for W, V being VectSp of F
for T being linear-transformation of V,W
for l being Linear_Combination of V
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)
let W, V be VectSp of F; ::_thesis: for T being linear-transformation of V,W
for l being Linear_Combination of V
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)
let T be linear-transformation of V,W; ::_thesis: for l being Linear_Combination of V
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)
let l be Linear_Combination of V; ::_thesis: 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)
let G be FinSequence of V; ::_thesis: ( rng G = Carrier l & T | (Carrier l) is one-to-one implies T * (l (#) G) = (T @ l) (#) (T * G) )
assume that
A1: rng G = Carrier l and
A2: T | (Carrier l) is one-to-one ; ::_thesis: T * (l (#) G) = (T @ l) (#) (T * G)
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; ::_thesis: ( 1 <= k & k <= len L implies L . k = R . k )
assume A6: ( 1 <= k & k <= len L ) ; ::_thesis: L . k = R . k
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, FUNCT_1: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  L . k = R . k by A7, A8, A11, A5, A12, VECTSP_6:def_5; ::_thesis: verum
end;
hence  T * (l (#) G) = (T @ l) (#) (T * G) by A4, A3, FINSEQ_1:14; ::_thesis: verum
end;

theorem Th39: :: RANKNULL:39
for F being Field
for W, V being VectSp of F
for T being linear-transformation of V,W
for l being Linear_Combination of V st T | (Carrier l) is one-to-one holds
T .: (Carrier l) = Carrier (T @ l)
proof
let F be Field; ::_thesis: for W, V being VectSp of F
for T being linear-transformation of V,W
for l being Linear_Combination of V st T | (Carrier l) is one-to-one holds
T .: (Carrier l) = Carrier (T @ l)
let W, V be VectSp of F; ::_thesis: for T being linear-transformation of V,W
for l being Linear_Combination of V st T | (Carrier l) is one-to-one holds
T .: (Carrier l) = Carrier (T @ l)
let T be linear-transformation of V,W; ::_thesis: for l being Linear_Combination of V st T | (Carrier l) is one-to-one holds
T .: (Carrier l) = Carrier (T @ l)
let l be Linear_Combination of V; ::_thesis: ( T | (Carrier l) is one-to-one implies T .: (Carrier l) = Carrier (T @ l) )
assume A1: T | (Carrier l) is one-to-one ; ::_thesis: T .: (Carrier l) = Carrier (T @ l)
A2: T .: (Carrier l) c= Carrier (T @ l)
proof
let w be set ; :: according to TARSKI:def_3 ::_thesis: ( not w in T .: (Carrier l) or w in Carrier (T @ l) )
assume  w in T .: (Carrier l) ; ::_thesis: w in Carrier (T @ 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 = 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  w in Carrier (T @ l) by A5; ::_thesis: verum
end;
 Carrier (T @ l) c= T .: (Carrier l) by Th30;
hence  T .: (Carrier l) = Carrier (T @ l) by A2, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th40: :: RANKNULL:40
for F being Field
for W, V being VectSp of F
for T being linear-transformation of V,W
for A being Subset of V
for B being Basis of V
for 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 F be Field; ::_thesis: for W, V being VectSp of F
for T being linear-transformation of V,W
for A being Subset of V
for B being Basis of V
for l being Linear_Combination of B \ A st A is Basis of ker T & A c= B holds
T . (Sum l) = Sum (T @ l)
let W, V be VectSp of F; ::_thesis: for T being linear-transformation of V,W
for A being Subset of V
for B being Basis of V
for l being Linear_Combination of B \ A st A is Basis of ker T & A c= B holds
T . (Sum l) = Sum (T @ l)
let T be linear-transformation of V,W; ::_thesis: for A being Subset of V
for B being Basis of V
for l being Linear_Combination of B \ A st A is Basis of ker T & A c= B holds
T . (Sum l) = Sum (T @ l)
let A be Subset of V; ::_thesis: for B being Basis of V
for l being Linear_Combination of B \ A st A is Basis of ker T & A c= B holds
T . (Sum l) = Sum (T @ l)
let B be Basis of V; ::_thesis: for l being Linear_Combination of B \ A st A is Basis of ker T & A c= B holds
T . (Sum l) = Sum (T @ l)
let l be Linear_Combination of B \ A; ::_thesis: ( A is Basis of ker T & A c= B implies T . (Sum l) = Sum (T @ l) )
assume  ( A is Basis of ker T & A c= B ) ; ::_thesis: T . (Sum l) = Sum (T @ l)
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 = T * G 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  T . (Sum l) = Sum (T @ l) by A6, A8, MATRLIN:16; ::_thesis: verum
end;

theorem Th41: :: RANKNULL:41
for F being Field
for V being VectSp of F
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 F be Field; ::_thesis: for V being VectSp of F
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 )
let V be VectSp of F; ::_thesis: 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 )
let X be Subset of V; ::_thesis: ( X is linearly-dependent implies ex l being Linear_Combination of X st
( Carrier l <> {} & Sum l = 0. V ) )
assume  X is linearly-dependent ; ::_thesis: ex l being Linear_Combination of X st
( Carrier l <> {} & Sum l = 0. V )
then  ex l being Linear_Combination of X st
( Sum l = 0. V & not Carrier l = {} ) by VECTSP_7:def_1;
hence  ex l being Linear_Combination of X st
( Carrier l <> {} & Sum l = 0. V ) ; ::_thesis: verum
end;

definition
let F be Field;
let V, W be VectSp of F;
let X be Subset of V;
let T be linear-transformation of V,W;
let l be Linear_Combination of T .: X;
assume A1: T | X is one-to-one ;
funcT # l ->  Linear_Combination of X equals :Def6: :: RANKNULL:def 6
(l * T) +* ((V \ X) --> (0. F));
coherence
 (l * T) +* ((V \ X) --> (0. F)) is Linear_Combination of X
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 ((l * T) +* ((V \ X) --> (0. 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 ((l * T) +* ((V \ X) --> (0. F))) c= [#] F by XBOOLE_1:1;
 ( dom T = [#] V & ([#] V) \/ (([#] V) \ X) = [#] V ) by Th7, XBOOLE_1:12;
then  dom ((l * T) +* ((V \ X) --> (0. F))) = [#] V by A3, A4, FUNCT_4:def_1;
then reconsider f = (l * T) +* ((V \ X) --> (0. 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  }  ;
  {  v where v is Element of V : f . v <> 0. F  }  c= [#] V
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  v where v is Element of V : f . v <> 0. F  }  or x in [#] V )
assume  x in  {  v where v is Element of V : f . v <> 0. F  }  ; ::_thesis: x in [#] V
then  ex v being Element of V st
( v = x & f . v <> 0. F ) ;
hence  x in [#] V ; ::_thesis: verum
end;
then reconsider C =  {  v where v is Element of V : f . v <> 0. F  }  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 | ((T " (Carrier l)) /\ X);
take  T | ((T " (Carrier l)) /\ X) ; ::_thesis: ( T | ((T " (Carrier l)) /\ X) is one-to-one & dom (T | ((T " (Carrier l)) /\ X)) = C & rng (T | ((T " (Carrier l)) /\ X)) c= Carrier l )
A6: C c= (T " (Carrier l)) /\ X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in C or x in (T " (Carrier l)) /\ X )
assume A7: x in C ; ::_thesis: x in (T " (Carrier l)) /\ X
A8: ex v being Element of V st
( v = x & f . v <> 0. F ) by A7;
reconsider x = x as Element of V by A7;
A9: now__::_thesis:_x_in_X
assume  not x in X ; ::_thesis: contradiction
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; ::_thesis: verum
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  x in (T " (Carrier l)) /\ X by A9, XBOOLE_0:def_4; ::_thesis: verum
end;
A13: dom T = [#] V by Th7;
A14: rng (T | ((T " (Carrier l)) /\ X)) c= Carrier l
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (T | ((T " (Carrier l)) /\ X)) or y in Carrier l )
assume  y in rng (T | ((T " (Carrier l)) /\ X)) ; ::_thesis: y in Carrier l
then consider x being set  such that
A15: x in dom (T | ((T " (Carrier l)) /\ X)) and
A16: y = (T | ((T " (Carrier l)) /\ X)) . 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  y in Carrier l by A15, A16, FUNCT_1:49; ::_thesis: verum
end;
 (T " (Carrier l)) /\ X c= C
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (T " (Carrier l)) /\ X or x in C )
assume A17: x in (T " (Carrier l)) /\ X ; ::_thesis: x in C
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 = 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  x in C by A23, A22; ::_thesis: verum
end;
then  (T " (Carrier l)) /\ X = C by A6, XBOOLE_0:def_10;
hence  ( T | ((T " (Carrier l)) /\ X) is one-to-one & dom (T | ((T " (Carrier l)) /\ X)) = C & rng (T | ((T " (Carrier l)) /\ X)) c= Carrier l ) by A1, A13, A14, Th2, RELAT_1:62, XBOOLE_1:17; ::_thesis: verum
end;
then  card C c= card (Carrier l) by CARD_1:10;
then reconsider C = C as finite Subset of V ;
take  C ; ::_thesis: for v being Element of V st not v in C holds
f . v = 0. F
thus  for v being Element of V st not v in C holds
f . v = 0. F ; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of V by VECTSP_6:def_1;
 Carrier f c= X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in X )
assume A24: x in Carrier f ; ::_thesis: x in X
reconsider x = x as Element of V by A24;
now__::_thesis:_x_in_X
assume  not x in X ; ::_thesis: contradiction
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; ::_thesis: verum
end;
hence  x in X ; ::_thesis: verum
end;
hence  (l * T) +* ((V \ X) --> (0. F)) is Linear_Combination of X by VECTSP_6:def_4; ::_thesis: verum
end;
end;

:: deftheorem Def6 defines # RANKNULL:def_6_:_
 for F being Field
for V, W being VectSp of F
for X being Subset of V
for T being linear-transformation of V,W
for l being Linear_Combination of T .: X st T | X is one-to-one holds
T # l = (l * T) +* ((V \ X) --> (0. F));

theorem Th42: :: RANKNULL:42
for F being Field
for W, V being VectSp of F
for T being linear-transformation of V,W
for X being Subset of V
for l being Linear_Combination of T .: X
for v being Element of V st v in X & T | X is one-to-one holds
(T # l) . v = l . (T . v)
proof
let F be Field; ::_thesis: for W, V being VectSp of F
for T being linear-transformation of V,W
for X being Subset of V
for l being Linear_Combination of T .: X
for v being Element of V st v in X & T | X is one-to-one holds
(T # l) . v = l . (T . v)
let W, V be VectSp of F; ::_thesis: for T being linear-transformation of V,W
for X being Subset of V
for l being Linear_Combination of T .: X
for v being Element of V st v in X & T | X is one-to-one holds
(T # l) . v = l . (T . v)
let T be linear-transformation of V,W; ::_thesis: for X being Subset of V
for l being Linear_Combination of T .: X
for v being Element of V st v in X & T | X is one-to-one holds
(T # l) . v = l . (T . v)
let X be Subset of V; ::_thesis: for l being Linear_Combination of T .: X
for v being Element of V st v in X & T | X is one-to-one holds
(T # l) . v = l . (T . v)
let l be Linear_Combination of T .: X; ::_thesis: for v being Element of V st v in X & T | X is one-to-one holds
(T # l) . v = l . (T . v)
let v be Element of V; ::_thesis: ( v in X & T | X is one-to-one implies (T # l) . v = l . (T . v) )
assume  ( v in X & T | X is one-to-one ) ; ::_thesis: (T # l) . v = l . (T . v)
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  (T # l) . v = l . (T . v) by A1, FUNCT_1:13; ::_thesis: verum
end;

theorem Th43: :: RANKNULL:43
for F being Field
for W, V being VectSp of F
for T being linear-transformation of V,W
for X being Subset of V
for l being Linear_Combination of T .: X st T | X is one-to-one holds
T @ (T # l) = l
proof
let F be Field; ::_thesis: for W, V being VectSp of F
for T being linear-transformation of V,W
for X being Subset of V
for l being Linear_Combination of T .: X st T | X is one-to-one holds
T @ (T # l) = l
let W, V be VectSp of F; ::_thesis: for T being linear-transformation of V,W
for X being Subset of V
for l being Linear_Combination of T .: X st T | X is one-to-one holds
T @ (T # l) = l
let T be linear-transformation of V,W; ::_thesis: for X being Subset of V
for l being Linear_Combination of T .: X st T | X is one-to-one holds
T @ (T # l) = l
let X be Subset of V; ::_thesis: for l being Linear_Combination of T .: X st T | X is one-to-one holds
T @ (T # l) = l
let l be Linear_Combination of T .: X; ::_thesis: ( T | X is one-to-one implies T @ (T # l) = l )
assume A1: T | X is one-to-one ; ::_thesis: T @ (T # l) = l
let w be Element of W; :: according to FUNCT_2:def_8 ::_thesis: (T @ (T # l)) . w = l . w
set m = T @ (T # l);
percases ( w in Carrier l or not w in Carrier l ) ;
supposeA2: w in Carrier l ; ::_thesis: (T @ (T # l)) . w = l . w
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 = 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: (T @ (T # l)) . w = Sum ((T # l) .: (T " {(T . v)})) by A7, Def5
.= Sum ({(l . (T . v))} \/ ((T # l) .: B)) by A9, A10, A11, RELAT_1:120 ;
percases ( B = {} or B <> {} ) ;
suppose B = {} ; ::_thesis: (T @ (T # l)) . w = l . w
then (T @ (T # l)) . w = Sum ({(l . (T . v))} \/ ({} F)) by A12
.= l . w by A7, RLVECT_2:9 ;
hence  (T @ (T # l)) . w = l . w ; ::_thesis: verum
end;
supposeA13: B <> {} ; ::_thesis: (T @ (T # l)) . w = l . w
 Carrier (T # l) c= X by VECTSP_6:def_4;
then  B misses Carrier (T # l) by A8, XBOOLE_1:63;
then (T @ (T # l)) . 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  (T @ (T # l)) . w = l . w ; ::_thesis: verum
end;
end;
end;
supposeA14: not w in Carrier l ; ::_thesis: (T @ (T # l)) . w = l . w
then A15: l . w = 0. F ;
now__::_thesis:_not_(T_@_(T_#_l))_._w_<>_0._F
assume A16: (T @ (T # l)) . w <> 0. F ; ::_thesis: contradiction
then  w in Carrier (T @ (T # l)) ;
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 (T @ (T # l)) . w = (T # l) . v by A18, A19, Th37
.= 0. F by A1, A15, A18, A19, A20, Th42 ;
hence  contradiction by A16; ::_thesis: verum
end;
hence  (T @ (T # l)) . w = l . w by A14; ::_thesis: verum
end;
end;
end;

begin

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

:: deftheorem  defines rank RANKNULL:def_7_:_
 for F being Field
for V, W being finite-dimensional VectSp of F
for T being linear-transformation of V,W holds rank T = dim (im T);

:: deftheorem  defines nullity RANKNULL:def_8_:_
 for F being Field
for V, W being finite-dimensional VectSp of F
for T being linear-transformation of V,W holds nullity T = dim (ker T);

theorem Th44: :: RANKNULL:44
for F being Field
for V, W being finite-dimensional VectSp of F
for T being linear-transformation of V,W holds dim V = (rank T) + (nullity T)
proof
let F be Field; ::_thesis: for V, W being finite-dimensional VectSp of F
for T being linear-transformation of V,W holds dim V = (rank T) + (nullity T)
let V, W be finite-dimensional VectSp of F; ::_thesis: for T being linear-transformation of V,W holds dim V = (rank T) + (nullity T)
let T be linear-transformation of V,W; ::_thesis: dim V = (rank T) + (nullity T)
set A = the finite Basis of ker T;
reconsider A9 = the finite Basis of ker T as Subset of V by Th19;
consider B being Basis of V such that
A1: the finite Basis of ker T c= B by VECTSP_9:13;
reconsider B = 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 = X as finite Subset of V ;
A2: B = the finite Basis of ker T \/ X by A1, XBOOLE_1:45;
reconsider B = B as finite Basis of V ;
reconsider A = the finite Basis of ker T 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 ; ::_thesis: contradiction
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  T # l9 ; ::_thesis: l = T @ (T # l9)
thus  l = T @ (T # l9) by A3, Th43; ::_thesis: verum
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  contradiction by A5, A7, Th30, XBOOLE_1:3; ::_thesis: verum
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 = 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); ::_thesis: v in L
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 ; ::_thesis: v = Sum m
thus  v = Sum m by A1, A14, A21, A19, Th40; ::_thesis: verum
end;
then  v in Lin C9 by VECTSP_7:7;
hence  v in L by VECTSP_9:17; ::_thesis: verum
end;
then A22: Lin C = im T by VECTSP_4:32;
reconsider C = C as linearly-independent Subset of (im T) by A4, VECTSP_9:12;
reconsider C = 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  dim V = (rank T) + (nullity T) ; ::_thesis: verum
end;

theorem :: RANKNULL:45
for F being Field
for V, W being finite-dimensional VectSp of F
for T being linear-transformation of V,W st T is one-to-one holds
dim V = rank T
proof
let F be Field; ::_thesis: for V, W being finite-dimensional VectSp of F
for T being linear-transformation of V,W st T is one-to-one holds
dim V = rank T
let V, W be finite-dimensional VectSp of F; ::_thesis: for T being linear-transformation of V,W st T is one-to-one holds
dim V = rank T
let T be linear-transformation of V,W; ::_thesis: ( T is one-to-one implies dim V = rank T )
assume  T is one-to-one ; ::_thesis: dim V = rank T
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  dim V = rank T ; ::_thesis: verum
end;