:: VECTSP_7 semantic presentation

begin


definition
let GF be Field;
let V be VectSp of GF;
let IT be Subset of V;
attrIT is linearly-independent  means :Def1: :: VECTSP_7:def 1
 for l being Linear_Combination of IT st Sum l = 0. V holds
Carrier l = {} ;
end;

:: deftheorem Def1 defines linearly-independent VECTSP_7:def_1_:_
 for GF being Field
for V being VectSp of GF
for IT being Subset of V holds
( IT is linearly-independent iff for l being Linear_Combination of IT st Sum l = 0. V holds
Carrier l = {} );

notation
let GF be Field;
let V be VectSp of GF;
let IT be Subset of V;
antonym  linearly-dependent IT for  linearly-independent ;
end;

theorem :: VECTSP_7:1
for GF being Field
for V being VectSp of GF
for A, B being Subset of V st A c= B & B is linearly-independent holds
A is linearly-independent
proof
let GF be Field; ::_thesis: for V being VectSp of GF
for A, B being Subset of V st A c= B & B is linearly-independent holds
A is linearly-independent
let V be VectSp of GF; ::_thesis: for A, B being Subset of V st A c= B & B is linearly-independent holds
A is linearly-independent
let A, B be Subset of V; ::_thesis: ( A c= B & B is linearly-independent implies A is linearly-independent )
assume that
A1: A c= B and
A2: B is linearly-independent ; ::_thesis: A is linearly-independent
let l be Linear_Combination of A; :: according to VECTSP_7:def_1 ::_thesis: ( Sum l = 0. V implies Carrier l = {} )
reconsider L = l as Linear_Combination of B by A1, VECTSP_6:4;
assume  Sum l = 0. V ; ::_thesis: Carrier l = {}
then  Carrier L = {} by A2, Def1;
hence  Carrier l = {} ; ::_thesis: verum
end;

theorem Th2: :: VECTSP_7:2
for GF being Field
for V being VectSp of GF
for A being Subset of V st A is linearly-independent holds
not 0. V in A
proof
let GF be Field; ::_thesis: for V being VectSp of GF
for A being Subset of V st A is linearly-independent holds
not 0. V in A
let V be VectSp of GF; ::_thesis: for A being Subset of V st A is linearly-independent holds
not 0. V in A
let A be Subset of V; ::_thesis: ( A is linearly-independent implies not 0. V in A )
assume that
A1: A is linearly-independent and
A2: 0. V in A ; ::_thesis: contradiction
deffunc H1( set ) ->  Element of the carrier of GF = 0. GF;
consider f being Function of the carrier of V, the carrier of GF such that
A3: f . (0. V) = 1_ GF and
A4: for v being Element of V st v <> 0. V holds
f . v = H1(v) from FUNCT_2:sch_6();
reconsider f = f as Element of Funcs ( the carrier of V, the carrier of GF) by FUNCT_2:8;
 ex T being finite Subset of V st
for v being Vector of V st not v in T holds
f . v = 0. GF
proof
take T = {(0. V)}; ::_thesis: for v being Vector of V st not v in T holds
f . v = 0. GF
let v be Vector of V; ::_thesis: ( not v in T implies f . v = 0. GF )
assume  not v in T ; ::_thesis: f . v = 0. GF
then  v <> 0. V by TARSKI:def_1;
hence  f . v = 0. GF by A4; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of V by VECTSP_6:def_1;
A5: Carrier f = {(0. V)}
proof
thus  Carrier f c= {(0. V)} :: according to XBOOLE_0:def_10 ::_thesis: {(0. V)} c= Carrier f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in {(0. V)} )
assume  x in Carrier f ; ::_thesis: x in {(0. V)}
then consider v being Vector of V such that
A6: v = x and
A7: f . v <> 0. GF ;
 v = 0. V by A4, A7;
hence  x in {(0. V)} by A6, TARSKI:def_1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(0. V)} or x in Carrier f )
assume  x in {(0. V)} ; ::_thesis: x in Carrier f
then  x = 0. V by TARSKI:def_1;
hence  x in Carrier f by A3; ::_thesis: verum
end;
then  Carrier f c= A by A2, ZFMISC_1:31;
then reconsider f = f as Linear_Combination of A by VECTSP_6:def_4;
Sum f = (f . (0. V)) * (0. V) by A5, VECTSP_6:20
.= 0. V by VECTSP_1:15 ;
hence  contradiction by A1, A5, Def1; ::_thesis: verum
end;

registration
let GF be Field;
let V be VectSp of GF;
cluster empty  ->  linearly-independent for Element of bool the carrier of V;
coherence
 for b1 being Subset of V st b1 is empty holds
b1 is linearly-independent
proof
let S be Subset of V; ::_thesis: ( S is empty implies S is linearly-independent )
assume A1: S is empty ; ::_thesis: S is linearly-independent
let l be Linear_Combination of S; :: according to VECTSP_7:def_1 ::_thesis: ( Sum l = 0. V implies Carrier l = {} )
 Carrier l c= {} by A1, VECTSP_6:def_4;
hence  ( Sum l = 0. V implies Carrier l = {} ) ; ::_thesis: verum
end;
end;

registration
let GF be Field;
let V be VectSp of GF;
cluster finite linearly-independent for Element of bool the carrier of V;
existence
 ex b1 being Subset of V st
( b1 is finite & b1 is linearly-independent )
proof
take  {} V ; ::_thesis: ( {} V is finite & {} V is linearly-independent )
thus  ( {} V is finite & {} V is linearly-independent ) ; ::_thesis: verum
end;
end;

theorem :: VECTSP_7:3
for GF being Field
for V being VectSp of GF
for v being Vector of V holds
( {v} is linearly-independent iff v <> 0. V )
proof
let GF be Field; ::_thesis: for V being VectSp of GF
for v being Vector of V holds
( {v} is linearly-independent iff v <> 0. V )
let V be VectSp of GF; ::_thesis: for v being Vector of V holds
( {v} is linearly-independent iff v <> 0. V )
let v be Vector of V; ::_thesis: ( {v} is linearly-independent iff v <> 0. V )
thus  ( {v} is linearly-independent implies v <> 0. V ) ::_thesis: ( v <> 0. V implies {v} is linearly-independent )
proof
assume  {v} is linearly-independent ; ::_thesis: v <> 0. V
then  not 0. V in {v} by Th2;
hence  v <> 0. V by TARSKI:def_1; ::_thesis: verum
end;
assume A1: v <> 0. V ; ::_thesis: {v} is linearly-independent
let l be Linear_Combination of {v}; :: according to VECTSP_7:def_1 ::_thesis: ( Sum l = 0. V implies Carrier l = {} )
A2: Carrier l c= {v} by VECTSP_6:def_4;
assume A3: Sum l = 0. V ; ::_thesis: Carrier l = {}
now__::_thesis:_Carrier_l_=_{}
percases ( Carrier l = {} or Carrier l = {v} ) by A2, ZFMISC_1:33;
suppose Carrier l = {} ; ::_thesis: Carrier l = {}
hence  Carrier l = {} ; ::_thesis: verum
end;
supposeA4: Carrier l = {v} ; ::_thesis: Carrier l = {}
A5: 0. V = (l . v) * v by A3, VECTSP_6:17;
now__::_thesis:_not_v_in_Carrier_l
assume  v in Carrier l ; ::_thesis: contradiction
then  ex u being Vector of V st
( v = u & l . u <> 0. GF ) ;
hence  contradiction by A1, A5, VECTSP_1:15; ::_thesis: verum
end;
hence  Carrier l = {} by A4, TARSKI:def_1; ::_thesis: verum
end;
end;
end;
hence  Carrier l = {} ; ::_thesis: verum
end;

theorem Th4: :: VECTSP_7:4
for GF being Field
for V being VectSp of GF
for v1, v2 being Vector of V st {v1,v2} is linearly-independent holds
v1 <> 0. V
proof
let GF be Field; ::_thesis: for V being VectSp of GF
for v1, v2 being Vector of V st {v1,v2} is linearly-independent holds
v1 <> 0. V
let V be VectSp of GF; ::_thesis: for v1, v2 being Vector of V st {v1,v2} is linearly-independent holds
v1 <> 0. V
let v1, v2 be Vector of V; ::_thesis: ( {v1,v2} is linearly-independent implies v1 <> 0. V )
A1: v1 in {v1,v2} by TARSKI:def_2;
assume  {v1,v2} is linearly-independent ; ::_thesis: v1 <> 0. V
hence  v1 <> 0. V by A1, Th2; ::_thesis: verum
end;

theorem Th5: :: VECTSP_7:5
for GF being Field
for V being VectSp of GF
for v1, v2 being Vector of V holds
( v1 <> v2 & {v1,v2} is linearly-independent iff ( v2 <> 0. V & ( for a being Element of GF holds v1 <> a * v2 ) ) )
proof
let GF be Field; ::_thesis: for V being VectSp of GF
for v1, v2 being Vector of V holds
( v1 <> v2 & {v1,v2} is linearly-independent iff ( v2 <> 0. V & ( for a being Element of GF holds v1 <> a * v2 ) ) )
let V be VectSp of GF; ::_thesis: for v1, v2 being Vector of V holds
( v1 <> v2 & {v1,v2} is linearly-independent iff ( v2 <> 0. V & ( for a being Element of GF holds v1 <> a * v2 ) ) )
let v1, v2 be Vector of V; ::_thesis: ( v1 <> v2 & {v1,v2} is linearly-independent iff ( v2 <> 0. V & ( for a being Element of GF holds v1 <> a * v2 ) ) )
thus  ( v1 <> v2 & {v1,v2} is linearly-independent implies ( v2 <> 0. V & ( for a being Element of GF holds v1 <> a * v2 ) ) ) ::_thesis: ( v2 <> 0. V & ( for a being Element of GF holds v1 <> a * v2 ) implies ( v1 <> v2 & {v1,v2} is linearly-independent ) )
proof
deffunc H1( set ) ->  Element of the carrier of GF = 0. GF;
assume that
A1: v1 <> v2 and
A2: {v1,v2} is linearly-independent ; ::_thesis: ( v2 <> 0. V & ( for a being Element of GF holds v1 <> a * v2 ) )
thus  v2 <> 0. V by A2, Th4; ::_thesis: for a being Element of GF holds v1 <> a * v2
let a be Element of GF; ::_thesis: v1 <> a * v2
consider f being Function of the carrier of V, the carrier of GF such that
A3: ( f . v1 = - (1_ GF) & f . v2 = a ) and
A4: for v being Element of V st v <> v1 & v <> v2 holds
f . v = H1(v) from FUNCT_2:sch_7(A1);
reconsider f = f as Element of Funcs ( the carrier of V, the carrier of GF) by FUNCT_2:8;
now__::_thesis:_for_v_being_Vector_of_V_st_not_v_in_{v1,v2}_holds_
f_._v_=_0._GF
let v be Vector of V; ::_thesis: ( not v in {v1,v2} implies f . v = 0. GF )
assume  not v in {v1,v2} ; ::_thesis: f . v = 0. GF
then  ( v <> v1 & v <> v2 ) by TARSKI:def_2;
hence  f . v = 0. GF by A4; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of V by VECTSP_6:def_1;
 Carrier f c= {v1,v2}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in {v1,v2} )
assume  x in Carrier f ; ::_thesis: x in {v1,v2}
then A5: ex u being Vector of V st
( x = u & f . u <> 0. GF ) ;
assume  not x in {v1,v2} ; ::_thesis: contradiction
then  ( x <> v1 & x <> v2 ) by TARSKI:def_2;
hence  contradiction by A4, A5; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of {v1,v2} by VECTSP_6:def_4;
A6: now__::_thesis:_v1_in_Carrier_f
assume  not v1 in Carrier f ; ::_thesis: contradiction
then  0. GF = - (1_ GF) by A3;
hence  contradiction by VECTSP_6:49; ::_thesis: verum
end;
set w = a * v2;
assume  v1 = a * v2 ; ::_thesis: contradiction
then  Sum f = ((- (1_ GF)) * (a * v2)) + (a * v2) by A1, A3, VECTSP_6:18
.= (- (a * v2)) + (a * v2) by VECTSP_1:14
.= - ((a * v2) - (a * v2)) by VECTSP_1:17
.= - (0. V) by VECTSP_1:19
.= 0. V by RLVECT_1:12 ;
hence  contradiction by A2, A6, Def1; ::_thesis: verum
end;
assume A7: v2 <> 0. V ; ::_thesis: ( ex a being Element of GF st not v1 <> a * v2 or ( v1 <> v2 & {v1,v2} is linearly-independent ) )
assume A8: for a being Element of GF holds v1 <> a * v2 ; ::_thesis: ( v1 <> v2 & {v1,v2} is linearly-independent )
A9: (1_ GF) * v2 = v2 by VECTSP_1:def_17;
hence  v1 <> v2 by A8; ::_thesis: {v1,v2} is linearly-independent
let l be Linear_Combination of {v1,v2}; :: according to VECTSP_7:def_1 ::_thesis: ( Sum l = 0. V implies Carrier l = {} )
assume that
A10: Sum l = 0. V and
A11: Carrier l <> {} ; ::_thesis: contradiction
A12: 0. V = ((l . v1) * v1) + ((l . v2) * v2) by A8, A9, A10, VECTSP_6:18;
set x = the Element of Carrier l;
 Carrier l c= {v1,v2} by VECTSP_6:def_4;
then A13: the Element of Carrier l in {v1,v2} by A11, TARSKI:def_3;
 the Element of Carrier l in Carrier l by A11;
then A14: ex u being Vector of V st
( the Element of Carrier l = u & l . u <> 0. GF ) ;
now__::_thesis:_contradiction
percases ( l . v1 <> 0. GF or ( l . v2 <> 0. GF & l . v1 = 0. GF ) ) by A14, A13, TARSKI:def_2;
supposeA15: l . v1 <> 0. GF ; ::_thesis: contradiction
0. V = ((l . v1) ") * (((l . v1) * v1) + ((l . v2) * v2)) by A12, VECTSP_1:15
.= (((l . v1) ") * ((l . v1) * v1)) + (((l . v1) ") * ((l . v2) * v2)) by VECTSP_1:def_14
.= ((((l . v1) ") * (l . v1)) * v1) + (((l . v1) ") * ((l . v2) * v2)) by VECTSP_1:def_16
.= ((((l . v1) ") * (l . v1)) * v1) + ((((l . v1) ") * (l . v2)) * v2) by VECTSP_1:def_16
.= ((1_ GF) * v1) + ((((l . v1) ") * (l . v2)) * v2) by A15, VECTSP_1:def_10
.= v1 + ((((l . v1) ") * (l . v2)) * v2) by VECTSP_1:def_17 ;
then v1 = - ((((l . v1) ") * (l . v2)) * v2) by VECTSP_1:16
.= (- (1_ GF)) * ((((l . v1) ") * (l . v2)) * v2) by VECTSP_1:14
.= ((- (1_ GF)) * (((l . v1) ") * (l . v2))) * v2 by VECTSP_1:def_16 ;
hence  contradiction by A8; ::_thesis: verum
end;
supposeA16: ( l . v2 <> 0. GF & l . v1 = 0. GF ) ; ::_thesis: contradiction
0. V = ((l . v2) ") * (((l . v1) * v1) + ((l . v2) * v2)) by A12, VECTSP_1:15
.= (((l . v2) ") * ((l . v1) * v1)) + (((l . v2) ") * ((l . v2) * v2)) by VECTSP_1:def_14
.= ((((l . v2) ") * (l . v1)) * v1) + (((l . v2) ") * ((l . v2) * v2)) by VECTSP_1:def_16
.= ((((l . v2) ") * (l . v1)) * v1) + ((((l . v2) ") * (l . v2)) * v2) by VECTSP_1:def_16
.= ((((l . v2) ") * (l . v1)) * v1) + ((1_ GF) * v2) by A16, VECTSP_1:def_10
.= ((((l . v2) ") * (l . v1)) * v1) + v2 by VECTSP_1:def_17
.= ((0. GF) * v1) + v2 by A16, VECTSP_1:12
.= (0. V) + v2 by VECTSP_1:15
.= v2 by RLVECT_1:4 ;
hence  contradiction by A7; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;

theorem :: VECTSP_7:6
for GF being Field
for V being VectSp of GF
for v1, v2 being Vector of V holds
( ( v1 <> v2 & {v1,v2} is linearly-independent ) iff for a, b being Element of GF st (a * v1) + (b * v2) = 0. V holds
( a = 0. GF & b = 0. GF ) )
proof
let GF be Field; ::_thesis: for V being VectSp of GF
for v1, v2 being Vector of V holds
( ( v1 <> v2 & {v1,v2} is linearly-independent ) iff for a, b being Element of GF st (a * v1) + (b * v2) = 0. V holds
( a = 0. GF & b = 0. GF ) )
let V be VectSp of GF; ::_thesis: for v1, v2 being Vector of V holds
( ( v1 <> v2 & {v1,v2} is linearly-independent ) iff for a, b being Element of GF st (a * v1) + (b * v2) = 0. V holds
( a = 0. GF & b = 0. GF ) )
let v1, v2 be Vector of V; ::_thesis: ( ( v1 <> v2 & {v1,v2} is linearly-independent ) iff for a, b being Element of GF st (a * v1) + (b * v2) = 0. V holds
( a = 0. GF & b = 0. GF ) )
thus  ( v1 <> v2 & {v1,v2} is linearly-independent implies for a, b being Element of GF st (a * v1) + (b * v2) = 0. V holds
( a = 0. GF & b = 0. GF ) ) ::_thesis: ( ( for a, b being Element of GF st (a * v1) + (b * v2) = 0. V holds
( a = 0. GF & b = 0. GF ) ) implies ( v1 <> v2 & {v1,v2} is linearly-independent ) )
proof
assume A1: ( v1 <> v2 & {v1,v2} is linearly-independent ) ; ::_thesis: for a, b being Element of GF st (a * v1) + (b * v2) = 0. V holds
( a = 0. GF & b = 0. GF )
let a, b be Element of GF; ::_thesis: ( (a * v1) + (b * v2) = 0. V implies ( a = 0. GF & b = 0. GF ) )
assume that
A2: (a * v1) + (b * v2) = 0. V and
A3: ( a <> 0. GF or b <> 0. GF ) ; ::_thesis: contradiction
now__::_thesis:_contradiction
percases ( a <> 0. GF or b <> 0. GF ) by A3;
supposeA4: a <> 0. GF ; ::_thesis: contradiction
0. V = (a ") * ((a * v1) + (b * v2)) by A2, VECTSP_1:15
.= ((a ") * (a * v1)) + ((a ") * (b * v2)) by VECTSP_1:def_14
.= (((a ") * a) * v1) + ((a ") * (b * v2)) by VECTSP_1:def_16
.= (((a ") * a) * v1) + (((a ") * b) * v2) by VECTSP_1:def_16
.= ((1_ GF) * v1) + (((a ") * b) * v2) by A4, VECTSP_1:def_10
.= v1 + (((a ") * b) * v2) by VECTSP_1:def_17 ;
then v1 = - (((a ") * b) * v2) by VECTSP_1:16
.= (- (1_ GF)) * (((a ") * b) * v2) by VECTSP_1:14
.= ((- (1_ GF)) * ((a ") * b)) * v2 by VECTSP_1:def_16 ;
hence  contradiction by A1, Th5; ::_thesis: verum
end;
supposeA5: b <> 0. GF ; ::_thesis: contradiction
0. V = (b ") * ((a * v1) + (b * v2)) by A2, VECTSP_1:15
.= ((b ") * (a * v1)) + ((b ") * (b * v2)) by VECTSP_1:def_14
.= (((b ") * a) * v1) + ((b ") * (b * v2)) by VECTSP_1:def_16
.= (((b ") * a) * v1) + (((b ") * b) * v2) by VECTSP_1:def_16
.= (((b ") * a) * v1) + ((1_ GF) * v2) by A5, VECTSP_1:def_10
.= (((b ") * a) * v1) + v2 by VECTSP_1:def_17 ;
then v2 = - (((b ") * a) * v1) by VECTSP_1:16
.= (- (1_ GF)) * (((b ") * a) * v1) by VECTSP_1:14
.= ((- (1_ GF)) * ((b ") * a)) * v1 by VECTSP_1:def_16 ;
hence  contradiction by A1, Th5; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;
assume A6: for a, b being Element of GF st (a * v1) + (b * v2) = 0. V holds
( a = 0. GF & b = 0. GF ) ; ::_thesis: ( v1 <> v2 & {v1,v2} is linearly-independent )
A7: now__::_thesis:_for_a_being_Element_of_GF_holds_not_v1_=_a_*_v2
let a be Element of GF; ::_thesis: not v1 = a * v2
assume  v1 = a * v2 ; ::_thesis: contradiction
then  v1 = (0. V) + (a * v2) by RLVECT_1:4;
then  0. V = v1 - (a * v2) by VECTSP_2:2
.= v1 + ((- a) * v2) by VECTSP_1:21
.= ((1. GF) * v1) + ((- a) * v2) by VECTSP_1:def_17 ;
hence  contradiction by A6; ::_thesis: verum
end;
now__::_thesis:_not_v2_=_0._V
assume A8: v2 = 0. V ; ::_thesis: contradiction
0. V = (0. V) + (0. V) by RLVECT_1:4
.= ((0. GF) * v1) + (0. V) by VECTSP_1:15
.= ((0. GF) * v1) + ((1. GF) * v2) by A8, VECTSP_1:15 ;
hence  contradiction by A6; ::_thesis: verum
end;
hence  ( v1 <> v2 & {v1,v2} is linearly-independent ) by A7, Th5; ::_thesis: verum
end;

definition
let GF be Field;
let V be VectSp of GF;
let A be Subset of V;
func Lin A ->  strict Subspace of V means :Def2: :: VECTSP_7:def 2
 the carrier of it =  {  (Sum l) where l is Linear_Combination of A : verum  }  ;
existence
 ex b1 being strict Subspace of V st the carrier of b1 =  {  (Sum l) where l is Linear_Combination of A : verum  }
proof
set A1 =  {  (Sum l) where l is Linear_Combination of A : verum  }  ;
  {  (Sum l) where l is Linear_Combination of A : verum  }  c= the carrier of V
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  (Sum l) where l is Linear_Combination of A : verum  }  or x in the carrier of V )
assume  x in  {  (Sum l) where l is Linear_Combination of A : verum  }  ; ::_thesis: x in the carrier of V
then  ex l being Linear_Combination of A st x = Sum l ;
hence  x in the carrier of V ; ::_thesis: verum
end;
then reconsider A1 =  {  (Sum l) where l is Linear_Combination of A : verum  }  as Subset of V ;
reconsider l = ZeroLC V as Linear_Combination of A by VECTSP_6:5;
A1: A1 is linearly-closed
proof
thus  for v, u being Vector of V st v in A1 & u in A1 holds
v + u in A1 :: according to VECTSP_4:def_1 ::_thesis: for b1 being Element of the carrier of GF
for b2 being Element of the carrier of V holds
( not b2 in A1 or b1 * b2 in A1 )
proof
let v, u be Vector of V; ::_thesis: ( v in A1 & u in A1 implies v + u in A1 )
assume that
A2: v in A1 and
A3: u in A1 ; ::_thesis: v + u in A1
consider l1 being Linear_Combination of A such that
A4: v = Sum l1 by A2;
consider l2 being Linear_Combination of A such that
A5: u = Sum l2 by A3;
reconsider f = l1 + l2 as Linear_Combination of A by VECTSP_6:24;
 v + u = Sum f by A4, A5, VECTSP_6:44;
hence  v + u in A1 ; ::_thesis: verum
end;
let a be Element of GF; ::_thesis: for b1 being Element of the carrier of V holds
( not b1 in A1 or a * b1 in A1 )
let v be Vector of V; ::_thesis: ( not v in A1 or a * v in A1 )
assume  v in A1 ; ::_thesis: a * v in A1
then consider l being Linear_Combination of A such that
A6: v = Sum l ;
reconsider f = a * l as Linear_Combination of A by VECTSP_6:31;
 a * v = Sum f by A6, VECTSP_6:45;
hence  a * v in A1 ; ::_thesis: verum
end;
 Sum l = 0. V by VECTSP_6:15;
then  0. V in A1 ;
hence  ex b1 being strict Subspace of V st the carrier of b1 =  {  (Sum l) where l is Linear_Combination of A : verum  }  by A1, VECTSP_4:34; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict Subspace of V st the carrier of b1 =  {  (Sum l) where l is Linear_Combination of A : verum  }  & the carrier of b2 =  {  (Sum l) where l is Linear_Combination of A : verum  }  holds
b1 = b2 by VECTSP_4:29;
end;

:: deftheorem Def2 defines Lin VECTSP_7:def_2_:_
 for GF being Field
for V being VectSp of GF
for A being Subset of V
for b4 being strict Subspace of V holds
( b4 = Lin A iff the carrier of b4 =  {  (Sum l) where l is Linear_Combination of A : verum  }  );

theorem Th7: :: VECTSP_7:7
for x being set
for GF being Field
for V being VectSp of GF
for A being Subset of V holds
( x in Lin A iff ex l being Linear_Combination of A st x = Sum l )
proof
let x be set ; ::_thesis: for GF being Field
for V being VectSp of GF
for A being Subset of V holds
( x in Lin A iff ex l being Linear_Combination of A st x = Sum l )
let GF be Field; ::_thesis: for V being VectSp of GF
for A being Subset of V holds
( x in Lin A iff ex l being Linear_Combination of A st x = Sum l )
let V be VectSp of GF; ::_thesis: for A being Subset of V holds
( x in Lin A iff ex l being Linear_Combination of A st x = Sum l )
let A be Subset of V; ::_thesis: ( x in Lin A iff ex l being Linear_Combination of A st x = Sum l )
thus  ( x in Lin A implies ex l being Linear_Combination of A st x = Sum l ) ::_thesis: ( ex l being Linear_Combination of A st x = Sum l implies x in Lin A )
proof
assume  x in Lin A ; ::_thesis: ex l being Linear_Combination of A st x = Sum l
then  x in the carrier of (Lin A) by STRUCT_0:def_5;
then  x in  {  (Sum l) where l is Linear_Combination of A : verum  }  by Def2;
hence  ex l being Linear_Combination of A st x = Sum l ; ::_thesis: verum
end;
given k being Linear_Combination of A such that A1: x = Sum k ; ::_thesis: x in Lin A
 x in  {  (Sum l) where l is Linear_Combination of A : verum  }  by A1;
then  x in the carrier of (Lin A) by Def2;
hence  x in Lin A by STRUCT_0:def_5; ::_thesis: verum
end;

theorem Th8: :: VECTSP_7:8
for x being set
for GF being Field
for V being VectSp of GF
for A being Subset of V st x in A holds
x in Lin A
proof
let x be set ; ::_thesis: for GF being Field
for V being VectSp of GF
for A being Subset of V st x in A holds
x in Lin A
let GF be Field; ::_thesis: for V being VectSp of GF
for A being Subset of V st x in A holds
x in Lin A
let V be VectSp of GF; ::_thesis: for A being Subset of V st x in A holds
x in Lin A
let A be Subset of V; ::_thesis: ( x in A implies x in Lin A )
deffunc H1( set ) ->  Element of the carrier of GF = 0. GF;
assume A1: x in A ; ::_thesis: x in Lin A
then reconsider v = x as Vector of V ;
consider f being Function of the carrier of V, the carrier of GF such that
A2: f . v = 1_ GF and
A3: for u being Vector of V st u <> v holds
f . u = H1(u) from FUNCT_2:sch_6();
reconsider f = f as Element of Funcs ( the carrier of V, the carrier of GF) by FUNCT_2:8;
 ex T being finite Subset of V st
for u being Vector of V st not u in T holds
f . u = 0. GF
proof
take T = {v}; ::_thesis: for u being Vector of V st not u in T holds
f . u = 0. GF
let u be Vector of V; ::_thesis: ( not u in T implies f . u = 0. GF )
assume  not u in T ; ::_thesis: f . u = 0. GF
then  u <> v by TARSKI:def_1;
hence  f . u = 0. GF by A3; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of V by VECTSP_6:def_1;
A4: Carrier f c= {v}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in {v} )
assume  x in Carrier f ; ::_thesis: x in {v}
then consider u being Vector of V such that
A5: x = u and
A6: f . u <> 0. GF ;
 u = v by A3, A6;
hence  x in {v} by A5, TARSKI:def_1; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of {v} by VECTSP_6:def_4;
A7: Sum f = (1_ GF) * v by A2, VECTSP_6:17
.= v by VECTSP_1:def_17 ;
 {v} c= A by A1, ZFMISC_1:31;
then  Carrier f c= A by A4, XBOOLE_1:1;
then reconsider f = f as Linear_Combination of A by VECTSP_6:def_4;
 Sum f = v by A7;
hence  x in Lin A by Th7; ::_thesis: verum
end;

theorem :: VECTSP_7:9
for GF being Field
for V being VectSp of GF holds Lin ({} the carrier of V) = (0). V
proof
let GF be Field; ::_thesis: for V being VectSp of GF holds Lin ({} the carrier of V) = (0). V
let V be VectSp of GF; ::_thesis: Lin ({} the carrier of V) = (0). V
set A = Lin ({} the carrier of V);
now__::_thesis:_for_v_being_Vector_of_V_holds_
(_(_v_in_Lin_({}_the_carrier_of_V)_implies_v_in_(0)._V_)_&_(_v_in_(0)._V_implies_v_in_Lin_({}_the_carrier_of_V)_)_)
let v be Vector of V; ::_thesis: ( ( v in Lin ({} the carrier of V) implies v in (0). V ) & ( v in (0). V implies v in Lin ({} the carrier of V) ) )
thus  ( v in Lin ({} the carrier of V) implies v in (0). V ) ::_thesis: ( v in (0). V implies v in Lin ({} the carrier of V) )
proof
assume  v in Lin ({} the carrier of V) ; ::_thesis: v in (0). V
then A1: v in the carrier of (Lin ({} the carrier of V)) by STRUCT_0:def_5;
 the carrier of (Lin ({} the carrier of V)) =  {  (Sum l0) where l0 is Linear_Combination of {} the carrier of V : verum  }  by Def2;
then  ex l0 being Linear_Combination of {} the carrier of V st v = Sum l0 by A1;
then  v = 0. V by VECTSP_6:16;
hence  v in (0). V by VECTSP_4:35; ::_thesis: verum
end;
assume  v in (0). V ; ::_thesis: v in Lin ({} the carrier of V)
then  v = 0. V by VECTSP_4:35;
hence  v in Lin ({} the carrier of V) by VECTSP_4:17; ::_thesis: verum
end;
hence  Lin ({} the carrier of V) = (0). V by VECTSP_4:30; ::_thesis: verum
end;

theorem :: VECTSP_7:10
for GF being Field
for V being VectSp of GF
for A being Subset of V holds
( not Lin A = (0). V or A = {} or A = {(0. V)} )
proof
let GF be Field; ::_thesis: for V being VectSp of GF
for A being Subset of V holds
( not Lin A = (0). V or A = {} or A = {(0. V)} )
let V be VectSp of GF; ::_thesis: for A being Subset of V holds
( not Lin A = (0). V or A = {} or A = {(0. V)} )
let A be Subset of V; ::_thesis: ( not Lin A = (0). V or A = {} or A = {(0. V)} )
assume that
A1: Lin A = (0). V and
A2: A <> {} ; ::_thesis: A = {(0. V)}
thus  A c= {(0. V)} :: according to XBOOLE_0:def_10 ::_thesis: {(0. V)} c= A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in {(0. V)} )
assume  x in A ; ::_thesis: x in {(0. V)}
then  x in Lin A by Th8;
then  x = 0. V by A1, VECTSP_4:35;
hence  x in {(0. V)} by TARSKI:def_1; ::_thesis: verum
end;
set y = the Element of A;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(0. V)} or x in A )
assume  x in {(0. V)} ; ::_thesis: x in A
then A3: x = 0. V by TARSKI:def_1;
 ( the Element of A in A & the Element of A in Lin A ) by A2, Th8;
hence  x in A by A1, A3, VECTSP_4:35; ::_thesis: verum
end;

theorem Th11: :: VECTSP_7:11
for GF being Field
for V being VectSp of GF
for A being Subset of V
for W being strict Subspace of V st A = the carrier of W holds
Lin A = W
proof
let GF be Field; ::_thesis: for V being VectSp of GF
for A being Subset of V
for W being strict Subspace of V st A = the carrier of W holds
Lin A = W
let V be VectSp of GF; ::_thesis: for A being Subset of V
for W being strict Subspace of V st A = the carrier of W holds
Lin A = W
let A be Subset of V; ::_thesis: for W being strict Subspace of V st A = the carrier of W holds
Lin A = W
let W be strict Subspace of V; ::_thesis: ( A = the carrier of W implies Lin A = W )
assume A1: A = the carrier of W ; ::_thesis: Lin A = W
now__::_thesis:_for_v_being_Vector_of_V_holds_
(_(_v_in_Lin_A_implies_v_in_W_)_&_(_v_in_W_implies_v_in_Lin_A_)_)
let v be Vector of V; ::_thesis: ( ( v in Lin A implies v in W ) & ( v in W implies v in Lin A ) )
A2: 0. GF <> 1. GF ;
thus  ( v in Lin A implies v in W ) ::_thesis: ( v in W implies v in Lin A )
proof
assume  v in Lin A ; ::_thesis: v in W
then A3: ex l being Linear_Combination of A st v = Sum l by Th7;
 A is linearly-closed by A1, VECTSP_4:33;
then  v in the carrier of W by A1, A2, A3, VECTSP_6:14;
hence  v in W by STRUCT_0:def_5; ::_thesis: verum
end;
 ( v in W iff v in the carrier of W ) by STRUCT_0:def_5;
hence  ( v in W implies v in Lin A ) by A1, Th8; ::_thesis: verum
end;
hence  Lin A = W by VECTSP_4:30; ::_thesis: verum
end;

theorem :: VECTSP_7:12
for GF being Field
for V being strict VectSp of GF
for A being Subset of V st A = the carrier of V holds
Lin A = V
proof
let GF be Field; ::_thesis: for V being strict VectSp of GF
for A being Subset of V st A = the carrier of V holds
Lin A = V
let V be strict VectSp of GF; ::_thesis: for A being Subset of V st A = the carrier of V holds
Lin A = V
let A be Subset of V; ::_thesis: ( A = the carrier of V implies Lin A = V )
assume A1: A = the carrier of V ; ::_thesis: Lin A = V
 (Omega). V = V ;
hence  Lin A = V by A1, Th11; ::_thesis: verum
end;

theorem Th13: :: VECTSP_7:13
for GF being Field
for V being VectSp of GF
for A, B being Subset of V st A c= B holds
Lin A is Subspace of Lin B
proof
let GF be Field; ::_thesis: for V being VectSp of GF
for A, B being Subset of V st A c= B holds
Lin A is Subspace of Lin B
let V be VectSp of GF; ::_thesis: for A, B being Subset of V st A c= B holds
Lin A is Subspace of Lin B
let A, B be Subset of V; ::_thesis: ( A c= B implies Lin A is Subspace of Lin B )
assume A1: A c= B ; ::_thesis: Lin A is Subspace of Lin B
now__::_thesis:_for_v_being_Vector_of_V_st_v_in_Lin_A_holds_
v_in_Lin_B
let v be Vector of V; ::_thesis: ( v in Lin A implies v in Lin B )
assume  v in Lin A ; ::_thesis: v in Lin B
then consider l being Linear_Combination of A such that
A2: v = Sum l by Th7;
reconsider l = l as Linear_Combination of B by A1, VECTSP_6:4;
 Sum l = v by A2;
hence  v in Lin B by Th7; ::_thesis: verum
end;
hence  Lin A is Subspace of Lin B by VECTSP_4:28; ::_thesis: verum
end;

theorem :: VECTSP_7:14
for GF being Field
for V being strict VectSp of GF
for A, B being Subset of V st Lin A = V & A c= B holds
Lin B = V
proof
let GF be Field; ::_thesis: for V being strict VectSp of GF
for A, B being Subset of V st Lin A = V & A c= B holds
Lin B = V
let V be strict VectSp of GF; ::_thesis: for A, B being Subset of V st Lin A = V & A c= B holds
Lin B = V
let A, B be Subset of V; ::_thesis: ( Lin A = V & A c= B implies Lin B = V )
assume  ( Lin A = V & A c= B ) ; ::_thesis: Lin B = V
then  V is Subspace of Lin B by Th13;
hence  Lin B = V by VECTSP_4:25; ::_thesis: verum
end;

theorem :: VECTSP_7:15
for GF being Field
for V being VectSp of GF
for A, B being Subset of V holds Lin (A \/ B) = (Lin A) + (Lin B)
proof
let GF be Field; ::_thesis: for V being VectSp of GF
for A, B being Subset of V holds Lin (A \/ B) = (Lin A) + (Lin B)
let V be VectSp of GF; ::_thesis: for A, B being Subset of V holds Lin (A \/ B) = (Lin A) + (Lin B)
let A, B be Subset of V; ::_thesis: Lin (A \/ B) = (Lin A) + (Lin B)
now__::_thesis:_for_v_being_Vector_of_V_st_v_in_Lin_(A_\/_B)_holds_
v_in_(Lin_A)_+_(Lin_B)
deffunc H1( set ) ->  Element of the carrier of GF = 0. GF;
let v be Vector of V; ::_thesis: ( v in Lin (A \/ B) implies v in (Lin A) + (Lin B) )
assume  v in Lin (A \/ B) ; ::_thesis: v in (Lin A) + (Lin B)
then consider l being Linear_Combination of A \/ B such that
A1: v = Sum l by Th7;
deffunc H2( set ) ->  set = l . $1;
set D = (Carrier l) \ A;
set C = (Carrier l) /\ A;
defpred S1[ set ] means $1 in (Carrier l) /\ A;
A2: now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_V_holds_
(_(_S1[x]_implies_H2(x)_in_the_carrier_of_GF_)_&_(_not_S1[x]_implies_H1(x)_in_the_carrier_of_GF_)_)
let x be set ; ::_thesis: ( x in the carrier of V implies ( ( S1[x] implies H2(x) in the carrier of GF ) & ( not S1[x] implies H1(x) in the carrier of GF ) ) )
assume  x in the carrier of V ; ::_thesis: ( ( S1[x] implies H2(x) in the carrier of GF ) & ( not S1[x] implies H1(x) in the carrier of GF ) )
then reconsider v = x as Vector of V ;
 for f being Function of the carrier of V, the carrier of GF holds f . v in the carrier of GF ;
hence  ( S1[x] implies H2(x) in the carrier of GF ) ; ::_thesis: ( not S1[x] implies H1(x) in the carrier of GF )
assume  not S1[x] ; ::_thesis: H1(x) in the carrier of GF
thus  H1(x) in the carrier of GF ; ::_thesis: verum
end;
reconsider C = (Carrier l) /\ A as finite Subset of V ;
defpred S2[ set ] means $1 in (Carrier l) \ A;
reconsider D = (Carrier l) \ A as finite Subset of V ;
A3: D c= B
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D or x in B )
assume  x in D ; ::_thesis: x in B
then A4: ( x in Carrier l & not x in A ) by XBOOLE_0:def_5;
 Carrier l c= A \/ B by VECTSP_6:def_4;
hence  x in B by A4, XBOOLE_0:def_3; ::_thesis: verum
end;
consider f being Function of the carrier of V, the carrier of GF such that
A5: for x being set st x in the carrier of V holds
( ( S1[x] implies f . x = H2(x) ) & ( not S1[x] implies f . x = H1(x) ) ) from FUNCT_2:sch_5(A2);
reconsider f = f as Element of Funcs ( the carrier of V, the carrier of GF) by FUNCT_2:8;
 for u being Vector of V st not u in C holds
f . u = 0. GF by A5;
then reconsider f = f as Linear_Combination of V by VECTSP_6:def_1;
A6: Carrier f c= C
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in C )
assume  x in Carrier f ; ::_thesis: x in C
then A7: ex u being Vector of V st
( x = u & f . u <> 0. GF ) ;
assume  not x in C ; ::_thesis: contradiction
hence  contradiction by A5, A7; ::_thesis: verum
end;
 C c= A by XBOOLE_1:17;
then  Carrier f c= A by A6, XBOOLE_1:1;
then reconsider f = f as Linear_Combination of A by VECTSP_6:def_4;
deffunc H3( set ) ->  set = l . $1;
A8: now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_V_holds_
(_(_S2[x]_implies_H3(x)_in_the_carrier_of_GF_)_&_(_not_S2[x]_implies_H1(x)_in_the_carrier_of_GF_)_)
let x be set ; ::_thesis: ( x in the carrier of V implies ( ( S2[x] implies H3(x) in the carrier of GF ) & ( not S2[x] implies H1(x) in the carrier of GF ) ) )
assume  x in the carrier of V ; ::_thesis: ( ( S2[x] implies H3(x) in the carrier of GF ) & ( not S2[x] implies H1(x) in the carrier of GF ) )
then reconsider v = x as Vector of V ;
 for g being Function of the carrier of V, the carrier of GF holds g . v in the carrier of GF ;
hence  ( S2[x] implies H3(x) in the carrier of GF ) ; ::_thesis: ( not S2[x] implies H1(x) in the carrier of GF )
assume  not S2[x] ; ::_thesis: H1(x) in the carrier of GF
thus  H1(x) in the carrier of GF ; ::_thesis: verum
end;
consider g being Function of the carrier of V, the carrier of GF such that
A9: for x being set st x in the carrier of V holds
( ( S2[x] implies g . x = H3(x) ) & ( not S2[x] implies g . x = H1(x) ) ) from FUNCT_2:sch_5(A8);
reconsider g = g as Element of Funcs ( the carrier of V, the carrier of GF) by FUNCT_2:8;
 for u being Vector of V st not u in D holds
g . u = 0. GF by A9;
then reconsider g = g as Linear_Combination of V by VECTSP_6:def_1;
 Carrier g c= D
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier g or x in D )
assume  x in Carrier g ; ::_thesis: x in D
then A10: ex u being Vector of V st
( x = u & g . u <> 0. GF ) ;
assume  not x in D ; ::_thesis: contradiction
hence  contradiction by A9, A10; ::_thesis: verum
end;
then  Carrier g c= B by A3, XBOOLE_1:1;
then reconsider g = g as Linear_Combination of B by VECTSP_6:def_4;
 l = f + g
proof
let v be Vector of V; :: according to VECTSP_6:def_7 ::_thesis: l . v = (f + g) . v
now__::_thesis:_(f_+_g)_._v_=_l_._v
percases ( v in C or not v in C ) ;
supposeA11: v in C ; ::_thesis: (f + g) . v = l . v
A12: now__::_thesis:_not_v_in_D
assume  v in D ; ::_thesis: contradiction
then  not v in A by XBOOLE_0:def_5;
hence  contradiction by A11, XBOOLE_0:def_4; ::_thesis: verum
end;
thus (f + g) . v = (f . v) + (g . v) by VECTSP_6:22
.= (l . v) + (g . v) by A5, A11
.= (l . v) + (0. GF) by A9, A12
.= l . v by RLVECT_1:4 ; ::_thesis: verum
end;
supposeA13: not v in C ; ::_thesis: l . v = (f + g) . v
now__::_thesis:_(f_+_g)_._v_=_l_._v
percases ( v in Carrier l or not v in Carrier l ) ;
supposeA14: v in Carrier l ; ::_thesis: (f + g) . v = l . v
A15: now__::_thesis:_v_in_D
assume  not v in D ; ::_thesis: contradiction
then  ( not v in Carrier l or v in A ) by XBOOLE_0:def_5;
hence  contradiction by A13, A14, XBOOLE_0:def_4; ::_thesis: verum
end;
thus (f + g) . v = (f . v) + (g . v) by VECTSP_6:22
.= (g . v) + (0. GF) by A5, A13
.= g . v by RLVECT_1:4
.= l . v by A9, A15 ; ::_thesis: verum
end;
supposeA16: not v in Carrier l ; ::_thesis: (f + g) . v = l . v
then A17: not v in D by XBOOLE_0:def_5;
A18: not v in C by A16, XBOOLE_0:def_4;
thus (f + g) . v = (f . v) + (g . v) by VECTSP_6:22
.= (0. GF) + (g . v) by A5, A18
.= (0. GF) + (0. GF) by A9, A17
.= 0. GF by RLVECT_1:4
.= l . v by A16 ; ::_thesis: verum
end;
end;
end;
hence  l . v = (f + g) . v ; ::_thesis: verum
end;
end;
end;
hence  l . v = (f + g) . v ; ::_thesis: verum
end;
then A19: v = (Sum f) + (Sum g) by A1, VECTSP_6:44;
 ( Sum f in Lin A & Sum g in Lin B ) by Th7;
hence  v in (Lin A) + (Lin B) by A19, VECTSP_5:1; ::_thesis: verum
end;
then A20: Lin (A \/ B) is Subspace of (Lin A) + (Lin B) by VECTSP_4:28;
 ( Lin A is Subspace of Lin (A \/ B) & Lin B is Subspace of Lin (A \/ B) ) by Th13, XBOOLE_1:7;
then  (Lin A) + (Lin B) is Subspace of Lin (A \/ B) by VECTSP_5:34;
hence  Lin (A \/ B) = (Lin A) + (Lin B) by A20, VECTSP_4:25; ::_thesis: verum
end;

theorem :: VECTSP_7:16
for GF being Field
for V being VectSp of GF
for A, B being Subset of V holds Lin (A /\ B) is Subspace of (Lin A) /\ (Lin B)
proof
let GF be Field; ::_thesis: for V being VectSp of GF
for A, B being Subset of V holds Lin (A /\ B) is Subspace of (Lin A) /\ (Lin B)
let V be VectSp of GF; ::_thesis: for A, B being Subset of V holds Lin (A /\ B) is Subspace of (Lin A) /\ (Lin B)
let A, B be Subset of V; ::_thesis: Lin (A /\ B) is Subspace of (Lin A) /\ (Lin B)
 ( Lin (A /\ B) is Subspace of Lin A & Lin (A /\ B) is Subspace of Lin B ) by Th13, XBOOLE_1:17;
hence  Lin (A /\ B) is Subspace of (Lin A) /\ (Lin B) by VECTSP_5:19; ::_thesis: verum
end;

theorem Th17: :: VECTSP_7:17
for GF being Field
for V being VectSp of GF
for A being Subset of V st A is linearly-independent holds
ex B being Subset of V st
( A c= B & B is linearly-independent & Lin B = VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) )
proof
let GF be Field; ::_thesis: for V being VectSp of GF
for A being Subset of V st A is linearly-independent holds
ex B being Subset of V st
( A c= B & B is linearly-independent & Lin B = VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) )
let V be VectSp of GF; ::_thesis: for A being Subset of V st A is linearly-independent holds
ex B being Subset of V st
( A c= B & B is linearly-independent & Lin B = VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) )
let A be Subset of V; ::_thesis: ( A is linearly-independent implies ex B being Subset of V st
( A c= B & B is linearly-independent & Lin B = VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) ) )
defpred S1[ set ] means  ex B being Subset of V st
( B = $1 & A c= B & B is linearly-independent );
consider Q being set  such that
A1: for Z being set holds
( Z in Q iff ( Z in bool the carrier of V & S1[Z] ) ) from XBOOLE_0:sch_1();
A2: now__::_thesis:_for_Z_being_set_st_Z_<>_{}_&_Z_c=_Q_&_Z_is_c=-linear_holds_
union_Z_in_Q
let Z be set ; ::_thesis: ( Z <> {} & Z c= Q & Z is c=-linear implies union Z in Q )
assume that
A3: Z <> {} and
A4: Z c= Q and
A5: Z is c=-linear ; ::_thesis: union Z in Q
set W = union Z;
 union Z c= the carrier of V
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union Z or x in the carrier of V )
assume  x in union Z ; ::_thesis: x in the carrier of V
then consider X being set  such that
A6: x in X and
A7: X in Z by TARSKI:def_4;
 X in bool the carrier of V by A1, A4, A7;
hence  x in the carrier of V by A6; ::_thesis: verum
end;
then reconsider W = union Z as Subset of V ;
A8: W is linearly-independent
proof
deffunc H1( set ) ->  set =  {  C where C is Subset of V : ( $1 in C & C in Z )  }  ;
let l be Linear_Combination of W; :: according to VECTSP_7:def_1 ::_thesis: ( Sum l = 0. V implies Carrier l = {} )
assume that
A9: Sum l = 0. V and
A10: Carrier l <> {} ; ::_thesis: contradiction
consider f being Function such that
A11: dom f = Carrier l and
A12: for x being set st x in Carrier l holds
f . x = H1(x) from FUNCT_1:sch_3();
reconsider M = rng f as non empty set by A10, A11, RELAT_1:42;
set F = the Choice_Function of M;
set S = rng the Choice_Function of M;
A13: now__::_thesis:_not_{}_in_M
assume  {} in M ; ::_thesis: contradiction
then consider x being set  such that
A14: x in dom f and
A15: f . x = {} by FUNCT_1:def_3;
 Carrier l c= W by VECTSP_6:def_4;
then consider X being set  such that
A16: x in X and
A17: X in Z by A11, A14, TARSKI:def_4;
reconsider X = X as Subset of V by A1, A4, A17;
 X in  {  C where C is Subset of V : ( x in C & C in Z )  }  by A16, A17;
hence  contradiction by A11, A12, A14, A15; ::_thesis: verum
end;
then A18: dom the Choice_Function of M = M by RLVECT_3:28;
then  dom the Choice_Function of M is finite by A11, FINSET_1:8;
then A19: rng the Choice_Function of M is finite by FINSET_1:8;
A20: now__::_thesis:_for_X_being_set_st_X_in_rng_the_Choice_Function_of_M_holds_
X_in_Z
let X be set ; ::_thesis: ( X in rng the Choice_Function of M implies X in Z )
assume  X in rng the Choice_Function of M ; ::_thesis: X in Z
then consider x being set  such that
A21: x in dom the Choice_Function of M and
A22: the Choice_Function of M . x = X by FUNCT_1:def_3;
consider y being set  such that
A23: ( y in dom f & f . y = x ) by A18, A21, FUNCT_1:def_3;
A24: x =  {  C where C is Subset of V : ( y in C & C in Z )  }  by A11, A12, A23;
 X in x by A13, A18, A21, A22, ORDERS_1:def_1;
then  ex C being Subset of V st
( C = X & y in C & C in Z ) by A24;
hence  X in Z ; ::_thesis: verum
end;
A25: now__::_thesis:_for_X,_Y_being_set_st_X_in_rng_the_Choice_Function_of_M_&_Y_in_rng_the_Choice_Function_of_M_&_not_X_c=_Y_holds_
Y_c=_X
let X, Y be set ; ::_thesis: ( X in rng the Choice_Function of M & Y in rng the Choice_Function of M & not X c= Y implies Y c= X )
assume  ( X in rng the Choice_Function of M & Y in rng the Choice_Function of M ) ; ::_thesis: ( X c= Y or Y c= X )
then  ( X in Z & Y in Z ) by A20;
then  X,Y are_c=-comparable by A5, ORDINAL1:def_8;
hence  ( X c= Y or Y c= X ) by XBOOLE_0:def_9; ::_thesis: verum
end;
 rng the Choice_Function of M <> {} by A18, RELAT_1:42;
then  union (rng the Choice_Function of M) in rng the Choice_Function of M by A25, A19, CARD_2:62;
then  union (rng the Choice_Function of M) in Z by A20;
then consider B being Subset of V such that
A26: B = union (rng the Choice_Function of M) and
 A c= B and
A27: B is linearly-independent by A1, A4;
 Carrier l c= union (rng the Choice_Function of M)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier l or x in union (rng the Choice_Function of M) )
set X = f . x;
assume A28: x in Carrier l ; ::_thesis: x in union (rng the Choice_Function of M)
then A29: f . x =  {  C where C is Subset of V : ( x in C & C in Z )  }  by A12;
A30: f . x in M by A11, A28, FUNCT_1:def_3;
then  the Choice_Function of M . (f . x) in f . x by A13, ORDERS_1:def_1;
then A31: ex C being Subset of V st
( the Choice_Function of M . (f . x) = C & x in C & C in Z ) by A29;
 the Choice_Function of M . (f . x) in rng the Choice_Function of M by A18, A30, FUNCT_1:def_3;
hence  x in union (rng the Choice_Function of M) by A31, TARSKI:def_4; ::_thesis: verum
end;
then  l is Linear_Combination of B by A26, VECTSP_6:def_4;
hence  contradiction by A9, A10, A27, Def1; ::_thesis: verum
end;
set x = the Element of Z;
 the Element of Z in Q by A3, A4, TARSKI:def_3;
then A32: ex B being Subset of V st
( B = the Element of Z & A c= B & B is linearly-independent ) by A1;
 the Element of Z c= W by A3, ZFMISC_1:74;
then  A c= W by A32, XBOOLE_1:1;
hence  union Z in Q by A1, A8; ::_thesis: verum
end;
assume  A is linearly-independent ; ::_thesis: ex B being Subset of V st
( A c= B & B is linearly-independent & Lin B = VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) )
then  Q <> {} by A1;
then consider X being set  such that
A33: X in Q and
A34: for Z being set st Z in Q & Z <> X holds
not X c= Z by A2, ORDERS_1:67;
consider B being Subset of V such that
A35: B = X and
A36: A c= B and
A37: B is linearly-independent by A1, A33;
take  B ; ::_thesis: ( A c= B & B is linearly-independent & Lin B = VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) )
thus  ( A c= B & B is linearly-independent ) by A36, A37; ::_thesis: Lin B = VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #)
assume  Lin B <> VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) ; ::_thesis: contradiction
then consider v being Vector of V such that
A38: ( ( v in Lin B & not v in (Omega). V ) or ( v in (Omega). V & not v in Lin B ) ) by VECTSP_4:30;
A39: B \/ {v} is linearly-independent
proof
let l be Linear_Combination of B \/ {v}; :: according to VECTSP_7:def_1 ::_thesis: ( Sum l = 0. V implies Carrier l = {} )
assume A40: Sum l = 0. V ; ::_thesis: Carrier l = {}
now__::_thesis:_Carrier_l_=_{}
percases ( v in Carrier l or not v in Carrier l ) ;
suppose v in Carrier l ; ::_thesis: Carrier l = {}
then  l . v <> 0. GF by VECTSP_6:2;
then A41: - (l . v) <> 0. GF by VECTSP_2:3;
deffunc H1( set ) ->  Element of the carrier of GF = 0. GF;
deffunc H2( Vector of V) ->  Element of the carrier of GF = l . $1;
consider f being Function of the carrier of V, the carrier of GF such that
A42: f . v = 0. GF and
A43: for u being Vector of V st u <> v holds
f . u = H2(u) from FUNCT_2:sch_6();
reconsider f = f as Element of Funcs ( the carrier of V, the carrier of GF) by FUNCT_2:8;
now__::_thesis:_for_u_being_Vector_of_V_st_not_u_in_(Carrier_l)_\_{v}_holds_
f_._u_=_0._GF
let u be Vector of V; ::_thesis: ( not u in (Carrier l) \ {v} implies f . u = 0. GF )
assume  not u in (Carrier l) \ {v} ; ::_thesis: f . u = 0. GF
then  ( not u in Carrier l or u in {v} ) by XBOOLE_0:def_5;
then  ( ( l . u = 0. GF & u <> v ) or u = v ) by TARSKI:def_1;
hence  f . u = 0. GF by A42, A43; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of V by VECTSP_6:def_1;
 Carrier f c= B
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in B )
A44: Carrier l c= B \/ {v} by VECTSP_6:def_4;
assume  x in Carrier f ; ::_thesis: x in B
then consider u being Vector of V such that
A45: u = x and
A46: f . u <> 0. GF ;
 f . u = l . u by A42, A43, A46;
then  u in Carrier l by A46;
then  ( u in B or u in {v} ) by A44, XBOOLE_0:def_3;
hence  x in B by A42, A45, A46, TARSKI:def_1; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of B by VECTSP_6:def_4;
consider g being Function of the carrier of V, the carrier of GF such that
A47: g . v = - (l . v) and
A48: for u being Vector of V st u <> v holds
g . u = H1(u) from FUNCT_2:sch_6();
reconsider g = g as Element of Funcs ( the carrier of V, the carrier of GF) by FUNCT_2:8;
now__::_thesis:_for_u_being_Vector_of_V_st_not_u_in_{v}_holds_
g_._u_=_0._GF
let u be Vector of V; ::_thesis: ( not u in {v} implies g . u = 0. GF )
assume  not u in {v} ; ::_thesis: g . u = 0. GF
then  u <> v by TARSKI:def_1;
hence  g . u = 0. GF by A48; ::_thesis: verum
end;
then reconsider g = g as Linear_Combination of V by VECTSP_6:def_1;
 Carrier g c= {v}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier g or x in {v} )
assume  x in Carrier g ; ::_thesis: x in {v}
then  ex u being Vector of V st
( x = u & g . u <> 0. GF ) ;
then  x = v by A48;
hence  x in {v} by TARSKI:def_1; ::_thesis: verum
end;
then reconsider g = g as Linear_Combination of {v} by VECTSP_6:def_4;
A49: Sum g = (- (l . v)) * v by A47, VECTSP_6:17;
 f - g = l
proof
let u be Vector of V; :: according to VECTSP_6:def_7 ::_thesis: (f - g) . u = l . u
now__::_thesis:_(f_-_g)_._u_=_l_._u
percases ( v = u or v <> u ) ;
supposeA50: v = u ; ::_thesis: (f - g) . u = l . u
thus (f - g) . u = (f . u) - (g . u) by VECTSP_6:40
.= (0. GF) + (- (- (l . v))) by A42, A47, A50, RLVECT_1:def_11
.= (l . v) + (0. GF) by RLVECT_1:17
.= l . u by A50, RLVECT_1:4 ; ::_thesis: verum
end;
supposeA51: v <> u ; ::_thesis: (f - g) . u = l . u
thus (f - g) . u = (f . u) - (g . u) by VECTSP_6:40
.= (l . u) - (g . u) by A43, A51
.= (l . u) - (0. GF) by A48, A51
.= l . u by RLVECT_1:13 ; ::_thesis: verum
end;
end;
end;
hence  (f - g) . u = l . u ; ::_thesis: verum
end;
then  0. V = (Sum f) - (Sum g) by A40, VECTSP_6:47;
then  Sum f = (0. V) + (Sum g) by VECTSP_2:2
.= (- (l . v)) * v by A49, RLVECT_1:4 ;
then A52: (- (l . v)) * v in Lin B by Th7;
((- (l . v)) ") * ((- (l . v)) * v) = (((- (l . v)) ") * (- (l . v))) * v by VECTSP_1:def_16
.= (1_ GF) * v by A41, VECTSP_1:def_10
.= v by VECTSP_1:def_17 ;
hence  Carrier l = {} by A38, A52, RLVECT_1:1, VECTSP_4:21; ::_thesis: verum
end;
supposeA53: not v in Carrier l ; ::_thesis: Carrier l = {}
 Carrier l c= B
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier l or x in B )
assume A54: x in Carrier l ; ::_thesis: x in B
 Carrier l c= B \/ {v} by VECTSP_6:def_4;
then  ( x in B or x in {v} ) by A54, XBOOLE_0:def_3;
hence  x in B by A53, A54, TARSKI:def_1; ::_thesis: verum
end;
then  l is Linear_Combination of B by VECTSP_6:def_4;
hence  Carrier l = {} by A37, A40, Def1; ::_thesis: verum
end;
end;
end;
hence  Carrier l = {} ; ::_thesis: verum
end;
 v in {v} by TARSKI:def_1;
then A55: v in B \/ {v} by XBOOLE_0:def_3;
A56: not v in B by A38, Th8, RLVECT_1:1;
 B c= B \/ {v} by XBOOLE_1:7;
then  A c= B \/ {v} by A36, XBOOLE_1:1;
then  B \/ {v} in Q by A1, A39;
hence  contradiction by A34, A35, A55, A56, XBOOLE_1:7; ::_thesis: verum
end;

theorem Th18: :: VECTSP_7:18
for GF being Field
for V being VectSp of GF
for A being Subset of V st Lin A = V holds
ex B being Subset of V st
( B c= A & B is linearly-independent & Lin B = V )
proof
let GF be Field; ::_thesis: for V being VectSp of GF
for A being Subset of V st Lin A = V holds
ex B being Subset of V st
( B c= A & B is linearly-independent & Lin B = V )
let V be VectSp of GF; ::_thesis: for A being Subset of V st Lin A = V holds
ex B being Subset of V st
( B c= A & B is linearly-independent & Lin B = V )
let A be Subset of V; ::_thesis: ( Lin A = V implies ex B being Subset of V st
( B c= A & B is linearly-independent & Lin B = V ) )
assume A1: Lin A = V ; ::_thesis: ex B being Subset of V st
( B c= A & B is linearly-independent & Lin B = V )
defpred S1[ set ] means  ex B being Subset of V st
( B = $1 & B c= A & B is linearly-independent );
consider Q being set  such that
A2: for Z being set holds
( Z in Q iff ( Z in bool the carrier of V & S1[Z] ) ) from XBOOLE_0:sch_1();
A3: now__::_thesis:_for_Z_being_set_st_Z_<>_{}_&_Z_c=_Q_&_Z_is_c=-linear_holds_
union_Z_in_Q
let Z be set ; ::_thesis: ( Z <> {} & Z c= Q & Z is c=-linear implies union Z in Q )
assume that
 Z <> {} and
A4: Z c= Q and
A5: Z is c=-linear ; ::_thesis: union Z in Q
set W = union Z;
 union Z c= the carrier of V
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union Z or x in the carrier of V )
assume  x in union Z ; ::_thesis: x in the carrier of V
then consider X being set  such that
A6: x in X and
A7: X in Z by TARSKI:def_4;
 X in bool the carrier of V by A2, A4, A7;
hence  x in the carrier of V by A6; ::_thesis: verum
end;
then reconsider W = union Z as Subset of V ;
A8: W is linearly-independent
proof
deffunc H1( set ) ->  set =  {  C where C is Subset of V : ( $1 in C & C in Z )  }  ;
let l be Linear_Combination of W; :: according to VECTSP_7:def_1 ::_thesis: ( Sum l = 0. V implies Carrier l = {} )
assume that
A9: Sum l = 0. V and
A10: Carrier l <> {} ; ::_thesis: contradiction
consider f being Function such that
A11: dom f = Carrier l and
A12: for x being set st x in Carrier l holds
f . x = H1(x) from FUNCT_1:sch_3();
reconsider M = rng f as non empty set by A10, A11, RELAT_1:42;
set F = the Choice_Function of M;
set S = rng the Choice_Function of M;
A13: now__::_thesis:_not_{}_in_M
assume  {} in M ; ::_thesis: contradiction
then consider x being set  such that
A14: x in dom f and
A15: f . x = {} by FUNCT_1:def_3;
 Carrier l c= W by VECTSP_6:def_4;
then consider X being set  such that
A16: x in X and
A17: X in Z by A11, A14, TARSKI:def_4;
reconsider X = X as Subset of V by A2, A4, A17;
 X in  {  C where C is Subset of V : ( x in C & C in Z )  }  by A16, A17;
hence  contradiction by A11, A12, A14, A15; ::_thesis: verum
end;
then A18: dom the Choice_Function of M = M by RLVECT_3:28;
then  dom the Choice_Function of M is finite by A11, FINSET_1:8;
then A19: rng the Choice_Function of M is finite by FINSET_1:8;
A20: now__::_thesis:_for_X_being_set_st_X_in_rng_the_Choice_Function_of_M_holds_
X_in_Z
let X be set ; ::_thesis: ( X in rng the Choice_Function of M implies X in Z )
assume  X in rng the Choice_Function of M ; ::_thesis: X in Z
then consider x being set  such that
A21: x in dom the Choice_Function of M and
A22: the Choice_Function of M . x = X by FUNCT_1:def_3;
consider y being set  such that
A23: ( y in dom f & f . y = x ) by A18, A21, FUNCT_1:def_3;
A24: x =  {  C where C is Subset of V : ( y in C & C in Z )  }  by A11, A12, A23;
 X in x by A13, A18, A21, A22, ORDERS_1:def_1;
then  ex C being Subset of V st
( C = X & y in C & C in Z ) by A24;
hence  X in Z ; ::_thesis: verum
end;
A25: now__::_thesis:_for_X,_Y_being_set_st_X_in_rng_the_Choice_Function_of_M_&_Y_in_rng_the_Choice_Function_of_M_&_not_X_c=_Y_holds_
Y_c=_X
let X, Y be set ; ::_thesis: ( X in rng the Choice_Function of M & Y in rng the Choice_Function of M & not X c= Y implies Y c= X )
assume  ( X in rng the Choice_Function of M & Y in rng the Choice_Function of M ) ; ::_thesis: ( X c= Y or Y c= X )
then  ( X in Z & Y in Z ) by A20;
then  X,Y are_c=-comparable by A5, ORDINAL1:def_8;
hence  ( X c= Y or Y c= X ) by XBOOLE_0:def_9; ::_thesis: verum
end;
 rng the Choice_Function of M <> {} by A18, RELAT_1:42;
then  union (rng the Choice_Function of M) in rng the Choice_Function of M by A25, A19, CARD_2:62;
then  union (rng the Choice_Function of M) in Z by A20;
then consider B being Subset of V such that
A26: B = union (rng the Choice_Function of M) and
 B c= A and
A27: B is linearly-independent by A2, A4;
 Carrier l c= union (rng the Choice_Function of M)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier l or x in union (rng the Choice_Function of M) )
set X = f . x;
assume A28: x in Carrier l ; ::_thesis: x in union (rng the Choice_Function of M)
then A29: f . x =  {  C where C is Subset of V : ( x in C & C in Z )  }  by A12;
A30: f . x in M by A11, A28, FUNCT_1:def_3;
then  the Choice_Function of M . (f . x) in f . x by A13, ORDERS_1:def_1;
then A31: ex C being Subset of V st
( the Choice_Function of M . (f . x) = C & x in C & C in Z ) by A29;
 the Choice_Function of M . (f . x) in rng the Choice_Function of M by A18, A30, FUNCT_1:def_3;
hence  x in union (rng the Choice_Function of M) by A31, TARSKI:def_4; ::_thesis: verum
end;
then  l is Linear_Combination of B by A26, VECTSP_6:def_4;
hence  contradiction by A9, A10, A27, Def1; ::_thesis: verum
end;
 W c= A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in W or x in A )
assume  x in W ; ::_thesis: x in A
then consider X being set  such that
A32: x in X and
A33: X in Z by TARSKI:def_4;
 ex B being Subset of V st
( B = X & B c= A & B is linearly-independent ) by A2, A4, A33;
hence  x in A by A32; ::_thesis: verum
end;
hence  union Z in Q by A2, A8; ::_thesis: verum
end;
 {} the carrier of V c= A by XBOOLE_1:2;
then  Q <> {} by A2;
then consider X being set  such that
A34: X in Q and
A35: for Z being set st Z in Q & Z <> X holds
not X c= Z by A3, ORDERS_1:67;
consider B being Subset of V such that
A36: B = X and
A37: B c= A and
A38: B is linearly-independent by A2, A34;
take  B ; ::_thesis: ( B c= A & B is linearly-independent & Lin B = V )
thus  ( B c= A & B is linearly-independent ) by A37, A38; ::_thesis: Lin B = V
assume A39: Lin B <> V ; ::_thesis: contradiction
now__::_thesis:_ex_v_being_Vector_of_V_st_
(_v_in_A_&_not_v_in_Lin_B_)
assume A40: for v being Vector of V st v in A holds
v in Lin B ; ::_thesis: contradiction
now__::_thesis:_for_v_being_Vector_of_V_st_v_in_Lin_A_holds_
v_in_Lin_B
reconsider F = the carrier of (Lin B) as Subset of V by VECTSP_4:def_2;
let v be Vector of V; ::_thesis: ( v in Lin A implies v in Lin B )
assume  v in Lin A ; ::_thesis: v in Lin B
then consider l being Linear_Combination of A such that
A41: v = Sum l by Th7;
 Carrier l c= the carrier of (Lin B)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier l or x in the carrier of (Lin B) )
assume A42: x in Carrier l ; ::_thesis: x in the carrier of (Lin B)
then reconsider a = x as Vector of V ;
 Carrier l c= A by VECTSP_6:def_4;
then  a in Lin B by A40, A42;
hence  x in the carrier of (Lin B) by STRUCT_0:def_5; ::_thesis: verum
end;
then reconsider l = l as Linear_Combination of F by VECTSP_6:def_4;
 Sum l = v by A41;
then  v in Lin F by Th7;
hence  v in Lin B by Th11; ::_thesis: verum
end;
then  Lin A is Subspace of Lin B by VECTSP_4:28;
hence  contradiction by A1, A39, VECTSP_4:25; ::_thesis: verum
end;
then consider v being Vector of V such that
A43: v in A and
A44: not v in Lin B ;
A45: B \/ {v} is linearly-independent
proof
let l be Linear_Combination of B \/ {v}; :: according to VECTSP_7:def_1 ::_thesis: ( Sum l = 0. V implies Carrier l = {} )
assume A46: Sum l = 0. V ; ::_thesis: Carrier l = {}
now__::_thesis:_Carrier_l_=_{}
percases ( v in Carrier l or not v in Carrier l ) ;
suppose v in Carrier l ; ::_thesis: Carrier l = {}
then  l . v <> 0. GF by VECTSP_6:2;
then A47: - (l . v) <> 0. GF by VECTSP_2:3;
deffunc H1( Vector of V) ->  Element of the carrier of GF = 0. GF;
deffunc H2( Vector of V) ->  Element of the carrier of GF = l . $1;
consider f being Function of the carrier of V, the carrier of GF such that
A48: f . v = 0. GF and
A49: for u being Vector of V st u <> v holds
f . u = H2(u) from FUNCT_2:sch_6();
reconsider f = f as Element of Funcs ( the carrier of V, the carrier of GF) by FUNCT_2:8;
now__::_thesis:_for_u_being_Vector_of_V_st_not_u_in_(Carrier_l)_\_{v}_holds_
f_._u_=_0._GF
let u be Vector of V; ::_thesis: ( not u in (Carrier l) \ {v} implies f . u = 0. GF )
assume  not u in (Carrier l) \ {v} ; ::_thesis: f . u = 0. GF
then  ( not u in Carrier l or u in {v} ) by XBOOLE_0:def_5;
then  ( ( l . u = 0. GF & u <> v ) or u = v ) by TARSKI:def_1;
hence  f . u = 0. GF by A48, A49; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of V by VECTSP_6:def_1;
 Carrier f c= B
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier f or x in B )
A50: Carrier l c= B \/ {v} by VECTSP_6:def_4;
assume  x in Carrier f ; ::_thesis: x in B
then consider u being Vector of V such that
A51: u = x and
A52: f . u <> 0. GF ;
 f . u = l . u by A48, A49, A52;
then  u in Carrier l by A52;
then  ( u in B or u in {v} ) by A50, XBOOLE_0:def_3;
hence  x in B by A48, A51, A52, TARSKI:def_1; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of B by VECTSP_6:def_4;
consider g being Function of the carrier of V, the carrier of GF such that
A53: g . v = - (l . v) and
A54: for u being Vector of V st u <> v holds
g . u = H1(u) from FUNCT_2:sch_6();
reconsider g = g as Element of Funcs ( the carrier of V, the carrier of GF) by FUNCT_2:8;
now__::_thesis:_for_u_being_Vector_of_V_st_not_u_in_{v}_holds_
g_._u_=_0._GF
let u be Vector of V; ::_thesis: ( not u in {v} implies g . u = 0. GF )
assume  not u in {v} ; ::_thesis: g . u = 0. GF
then  u <> v by TARSKI:def_1;
hence  g . u = 0. GF by A54; ::_thesis: verum
end;
then reconsider g = g as Linear_Combination of V by VECTSP_6:def_1;
 Carrier g c= {v}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier g or x in {v} )
assume  x in Carrier g ; ::_thesis: x in {v}
then  ex u being Vector of V st
( x = u & g . u <> 0. GF ) ;
then  x = v by A54;
hence  x in {v} by TARSKI:def_1; ::_thesis: verum
end;
then reconsider g = g as Linear_Combination of {v} by VECTSP_6:def_4;
A55: Sum g = (- (l . v)) * v by A53, VECTSP_6:17;
 f - g = l
proof
let u be Vector of V; :: according to VECTSP_6:def_7 ::_thesis: (f - g) . u = l . u
now__::_thesis:_(f_-_g)_._u_=_l_._u
percases ( v = u or v <> u ) ;
supposeA56: v = u ; ::_thesis: (f - g) . u = l . u
thus (f - g) . u = (f . u) - (g . u) by VECTSP_6:40
.= (0. GF) + (- (- (l . v))) by A48, A53, A56, RLVECT_1:def_11
.= (l . v) + (0. GF) by RLVECT_1:17
.= l . u by A56, RLVECT_1:4 ; ::_thesis: verum
end;
supposeA57: v <> u ; ::_thesis: (f - g) . u = l . u
thus (f - g) . u = (f . u) - (g . u) by VECTSP_6:40
.= (l . u) - (g . u) by A49, A57
.= (l . u) - (0. GF) by A54, A57
.= l . u by RLVECT_1:13 ; ::_thesis: verum
end;
end;
end;
hence  (f - g) . u = l . u ; ::_thesis: verum
end;
then  0. V = (Sum f) - (Sum g) by A46, VECTSP_6:47;
then  Sum f = (0. V) + (Sum g) by VECTSP_2:2
.= (- (l . v)) * v by A55, RLVECT_1:4 ;
then A58: (- (l . v)) * v in Lin B by Th7;
((- (l . v)) ") * ((- (l . v)) * v) = (((- (l . v)) ") * (- (l . v))) * v by VECTSP_1:def_16
.= (1_ GF) * v by A47, VECTSP_1:def_10
.= v by VECTSP_1:def_17 ;
hence  Carrier l = {} by A44, A58, VECTSP_4:21; ::_thesis: verum
end;
supposeA59: not v in Carrier l ; ::_thesis: Carrier l = {}
 Carrier l c= B
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Carrier l or x in B )
assume A60: x in Carrier l ; ::_thesis: x in B
 Carrier l c= B \/ {v} by VECTSP_6:def_4;
then  ( x in B or x in {v} ) by A60, XBOOLE_0:def_3;
hence  x in B by A59, A60, TARSKI:def_1; ::_thesis: verum
end;
then  l is Linear_Combination of B by VECTSP_6:def_4;
hence  Carrier l = {} by A38, A46, Def1; ::_thesis: verum
end;
end;
end;
hence  Carrier l = {} ; ::_thesis: verum
end;
 {v} c= A by A43, ZFMISC_1:31;
then  B \/ {v} c= A by A37, XBOOLE_1:8;
then A61: B \/ {v} in Q by A2, A45;
 v in {v} by TARSKI:def_1;
then A62: v in B \/ {v} by XBOOLE_0:def_3;
 not v in B by A44, Th8;
hence  contradiction by A35, A36, A62, A61, XBOOLE_1:7; ::_thesis: verum
end;

definition
let GF be Field;
let V be VectSp of GF;
mode Basis of V ->  Subset of V means :Def3: :: VECTSP_7:def 3
( it is linearly-independent & Lin it = VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) );
existence
 ex b1 being Subset of V st
( b1 is linearly-independent & Lin b1 = VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) )
proof
 ex B being Subset of V st
( {} the carrier of V c= B & B is linearly-independent & Lin B = VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) ) by Th17;
hence  ex b1 being Subset of V st
( b1 is linearly-independent & Lin b1 = VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) ) ; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines Basis VECTSP_7:def_3_:_
 for GF being Field
for V being VectSp of GF
for b3 being Subset of V holds
( b3 is Basis of V iff ( b3 is linearly-independent & Lin b3 = VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) ) );

theorem :: VECTSP_7:19
for GF being Field
for V being VectSp of GF
for A being Subset of V st A is linearly-independent holds
ex I being Basis of V st A c= I
proof
let GF be Field; ::_thesis: for V being VectSp of GF
for A being Subset of V st A is linearly-independent holds
ex I being Basis of V st A c= I
let V be VectSp of GF; ::_thesis: for A being Subset of V st A is linearly-independent holds
ex I being Basis of V st A c= I
let A be Subset of V; ::_thesis: ( A is linearly-independent implies ex I being Basis of V st A c= I )
assume  A is linearly-independent ; ::_thesis: ex I being Basis of V st A c= I
then consider B being Subset of V such that
A1: A c= B and
A2: ( B is linearly-independent & Lin B = VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) ) by Th17;
reconsider B = B as Basis of V by A2, Def3;
take  B ; ::_thesis: A c= B
thus  A c= B by A1; ::_thesis: verum
end;

theorem :: VECTSP_7:20
for GF being Field
for V being VectSp of GF
for A being Subset of V st Lin A = V holds
ex I being Basis of V st I c= A
proof
let GF be Field; ::_thesis: for V being VectSp of GF
for A being Subset of V st Lin A = V holds
ex I being Basis of V st I c= A
let V be VectSp of GF; ::_thesis: for A being Subset of V st Lin A = V holds
ex I being Basis of V st I c= A
let A be Subset of V; ::_thesis: ( Lin A = V implies ex I being Basis of V st I c= A )
assume  Lin A = V ; ::_thesis: ex I being Basis of V st I c= A
then consider B being Subset of V such that
A1: B c= A and
A2: ( B is linearly-independent & Lin B = V ) by Th18;
reconsider B = B as Basis of V by A2, Def3;
take  B ; ::_thesis: B c= A
thus  B c= A by A1; ::_thesis: verum
end;