:: MOD_3 semantic presentation

begin

Lm1:  for R being Ring
for a being Scalar of R st - a = 0. R holds
a = 0. R
proof
let R be Ring; ::_thesis: for a being Scalar of R st - a = 0. R holds
a = 0. R
let a be Scalar of R; ::_thesis: ( - a = 0. R implies a = 0. R )
assume  - a = 0. R ; ::_thesis: a = 0. R
then  - (- a) = 0. R by RLVECT_1:12;
hence  a = 0. R by RLVECT_1:17; ::_thesis: verum
end;

theorem Th1: :: MOD_3:1
for R being non empty non degenerated right_complementable add-associative right_zeroed doubleLoopStr holds 0. R <> - (1. R)
proof
let R be non empty non degenerated right_complementable add-associative right_zeroed doubleLoopStr ; ::_thesis: 0. R <> - (1. R)
assume  0. R = - (1. R) ; ::_thesis: contradiction
then  0. R = - (- (1. R)) by RLVECT_1:12
.= 1. R by RLVECT_1:17 ;
hence  contradiction ; ::_thesis: verum
end;


theorem Th2: :: MOD_3:2
for R being Ring
for V being LeftMod of R
for L being Linear_Combination of V
for C being finite Subset of V st Carrier L c= C holds
ex F being FinSequence of the carrier of V st
( F is one-to-one & rng F = C & Sum L = Sum (L (#) F) )
proof
let R be Ring; ::_thesis: for V being LeftMod of R
for L being Linear_Combination of V
for C being finite Subset of V st Carrier L c= C holds
ex F being FinSequence of the carrier of V st
( F is one-to-one & rng F = C & Sum L = Sum (L (#) F) )
let V be LeftMod of R; ::_thesis: for L being Linear_Combination of V
for C being finite Subset of V st Carrier L c= C holds
ex F being FinSequence of the carrier of V st
( F is one-to-one & rng F = C & Sum L = Sum (L (#) F) )
let L be Linear_Combination of V; ::_thesis: for C being finite Subset of V st Carrier L c= C holds
ex F being FinSequence of the carrier of V st
( F is one-to-one & rng F = C & Sum L = Sum (L (#) F) )
let C be finite Subset of V; ::_thesis: ( Carrier L c= C implies ex F being FinSequence of the carrier of V st
( F is one-to-one & rng F = C & Sum L = Sum (L (#) F) ) )
assume A1: Carrier L c= C ; ::_thesis: ex F being FinSequence of the carrier of V st
( F is one-to-one & rng F = C & Sum L = Sum (L (#) F) )
set D = C \ (Carrier L);
consider G being FinSequence of the carrier of V such that
A2: G is one-to-one and
A3: rng G = Carrier L and
A4: Sum L = Sum (L (#) G) by VECTSP_6:def_6;
consider p being FinSequence such that
A5: rng p = C \ (Carrier L) and
A6: p is one-to-one by FINSEQ_4:58;
reconsider p = p as FinSequence of the carrier of V by A5, FINSEQ_1:def_4;
A7: rng G misses rng p
proof
assume  rng G meets rng p ; ::_thesis: contradiction
then  ex x being set st
( x in Carrier L & x in C \ (Carrier L) ) by A3, A5, XBOOLE_0:3;
hence  contradiction by XBOOLE_0:def_5; ::_thesis: verum
end;
A8: len p = len (L (#) p) by VECTSP_6:def_5;
now__::_thesis:_for_k_being_Element_of_NAT_st_k_in_dom_p_holds_
(L_(#)_p)_._k_=_(0._R)_*_(p_/._k)
let k be Element of NAT ; ::_thesis: ( k in dom p implies (L (#) p) . k = (0. R) * (p /. k) )
assume A9: k in dom p ; ::_thesis: (L (#) p) . k = (0. R) * (p /. k)
then  p /. k = p . k by PARTFUN1:def_6;
then  p /. k in C \ (Carrier L) by A5, A9, FUNCT_1:def_3;
then A10: not p /. k in Carrier L by XBOOLE_0:def_5;
 k in dom (L (#) p) by A8, A9, FINSEQ_3:29;
then  (L (#) p) . k = (L . (p /. k)) * (p /. k) by VECTSP_6:def_5;
hence  (L (#) p) . k = (0. R) * (p /. k) by A10; ::_thesis: verum
end;
then A11: Sum (L (#) p) = (0. R) * (Sum p) by A8, RLVECT_2:67
.= 0. V by VECTSP_1:14 ;
set F = G ^ p;
take  G ^ p ; ::_thesis: ( G ^ p is one-to-one & rng (G ^ p) = C & Sum L = Sum (L (#) (G ^ p)) )
A12: Sum (L (#) (G ^ p)) = Sum ((L (#) G) ^ (L (#) p)) by VECTSP_6:13
.= (Sum (L (#) G)) + (0. V) by A11, RLVECT_1:41
.= Sum L by A4, RLVECT_1:def_4 ;
rng (G ^ p) = (Carrier L) \/ (C \ (Carrier L)) by A3, A5, FINSEQ_1:31
.= C by A1, XBOOLE_1:45 ;
hence  ( G ^ p is one-to-one & rng (G ^ p) = C & Sum L = Sum (L (#) (G ^ p)) ) by A2, A6, A12, A7, FINSEQ_3:91; ::_thesis: verum
end;

theorem Th3: :: MOD_3:3
for R being Ring
for V being LeftMod of R
for L being Linear_Combination of V
for a being Scalar of R holds Sum (a * L) = a * (Sum L)
proof
let R be Ring; ::_thesis: for V being LeftMod of R
for L being Linear_Combination of V
for a being Scalar of R holds Sum (a * L) = a * (Sum L)
let V be LeftMod of R; ::_thesis: for L being Linear_Combination of V
for a being Scalar of R holds Sum (a * L) = a * (Sum L)
let L be Linear_Combination of V; ::_thesis: for a being Scalar of R holds Sum (a * L) = a * (Sum L)
let a be Scalar of R; ::_thesis: Sum (a * L) = a * (Sum L)
set l = a * L;
 Carrier (a * L) c= Carrier L by VECTSP_6:28;
then consider F being FinSequence of the carrier of V such that
A1: ( F is one-to-one & rng F = Carrier L ) and
A2: Sum (a * L) = Sum ((a * L) (#) F) by Th2;
set f = (a * L) (#) F;
set g = L (#) F;
A3: len ((a * L) (#) F) = len F by VECTSP_6:def_5
.= len (L (#) F) by VECTSP_6:def_5 ;
 len ((a * L) (#) F) = len F by VECTSP_6:def_5;
then A4: dom F = Seg (len ((a * L) (#) F)) by FINSEQ_1:def_3;
A5: now__::_thesis:_for_k_being_Element_of_NAT_
for_v_being_Vector_of_V_st_k_in_dom_((a_*_L)_(#)_F)_&_v_=_(L_(#)_F)_._k_holds_
((a_*_L)_(#)_F)_._k_=_a_*_v
let k be Element of NAT ; ::_thesis: for v being Vector of V st k in dom ((a * L) (#) F) & v = (L (#) F) . k holds
((a * L) (#) F) . k = a * v
let v be Vector of V; ::_thesis: ( k in dom ((a * L) (#) F) & v = (L (#) F) . k implies ((a * L) (#) F) . k = a * v )
assume that
A6: k in dom ((a * L) (#) F) and
A7: v = (L (#) F) . k ; ::_thesis: ((a * L) (#) F) . k = a * v
set v9 = F /. k;
A8: k in Seg (len ((a * L) (#) F)) by A6, FINSEQ_1:def_3;
then A9: F /. k = F . k by A4, PARTFUN1:def_6;
hence ((a * L) (#) F) . k = ((a * L) . (F /. k)) * (F /. k) by A4, A8, VECTSP_6:8
.= (a * (L . (F /. k))) * (F /. k) by VECTSP_6:def_9
.= a * ((L . (F /. k)) * (F /. k)) by VECTSP_1:def_16
.= a * v by A4, A7, A8, A9, VECTSP_6:8 ;
::_thesis: verum
end;
 Sum L = Sum (L (#) F) by A1, VECTSP_6:def_6;
hence  Sum (a * L) = a * (Sum L) by A2, A3, A5, RLVECT_2:66; ::_thesis: verum
end;


definition
let R be Ring;
let V be LeftMod of R;
let A be Subset of V;
func Lin A ->  strict Subspace of V means :Def1: :: MOD_3:def 1
 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 R
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 Scalar of R; ::_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, Th3;
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 Def1 defines Lin MOD_3:def_1_:_
 for R being Ring
for V being LeftMod of R
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 Th4: :: MOD_3:4
for x being set
for R being Ring
for V being LeftMod of R
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 R being Ring
for V being LeftMod of R
for A being Subset of V holds
( x in Lin A iff ex l being Linear_Combination of A st x = Sum l )
let R be Ring; ::_thesis: for V being LeftMod of R
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 LeftMod of R; ::_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 Def1;
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 Def1;
hence  x in Lin A by STRUCT_0:def_5; ::_thesis: verum
end;

theorem Th5: :: MOD_3:5
for x being set
for R being Ring
for V being LeftMod of R
for A being Subset of V st x in A holds
x in Lin A
proof
let x be set ; ::_thesis: for R being Ring
for V being LeftMod of R
for A being Subset of V st x in A holds
x in Lin A
let R be Ring; ::_thesis: for V being LeftMod of R
for A being Subset of V st x in A holds
x in Lin A
let V be LeftMod of R; ::_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( Vector of V) ->  Element of the carrier of R = 0. R;
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 R such that
A2: f . v = 1. R 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 R) 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. R
proof
take T = {v}; ::_thesis: for u being Vector of V st not u in T holds
f . u = 0. R
let u be Vector of V; ::_thesis: ( not u in T implies f . u = 0. R )
assume  not u in T ; ::_thesis: f . u = 0. R
then  u <> v by TARSKI:def_1;
hence  f . u = 0. R 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. R ;
 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. R) * 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 Th4; ::_thesis: verum
end;

theorem Th6: :: MOD_3:6
for R being Ring
for V being LeftMod of R holds Lin ({} the carrier of V) = (0). V
proof
let R be Ring; ::_thesis: for V being LeftMod of R holds Lin ({} the carrier of V) = (0). V
let V be LeftMod of R; ::_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 Def1;
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 :: MOD_3:7
for R being Ring
for V being LeftMod of R
for A being Subset of V holds
( not Lin A = (0). V or A = {} or A = {(0. V)} )
proof
let R be Ring; ::_thesis: for V being LeftMod of R
for A being Subset of V holds
( not Lin A = (0). V or A = {} or A = {(0. V)} )
let V be LeftMod of R; ::_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 Th5;
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, Th5;
hence  x in A by A1, A3, VECTSP_4:35; ::_thesis: verum
end;

theorem Th8: :: MOD_3:8
for R being Ring
for V being LeftMod of R
for A being Subset of V
for W being strict Subspace of V st 0. R <> 1. R & A = the carrier of W holds
Lin A = W
proof
let R be Ring; ::_thesis: for V being LeftMod of R
for A being Subset of V
for W being strict Subspace of V st 0. R <> 1. R & A = the carrier of W holds
Lin A = W
let V be LeftMod of R; ::_thesis: for A being Subset of V
for W being strict Subspace of V st 0. R <> 1. R & A = the carrier of W holds
Lin A = W
let A be Subset of V; ::_thesis: for W being strict Subspace of V st 0. R <> 1. R & A = the carrier of W holds
Lin A = W
let W be strict Subspace of V; ::_thesis: ( 0. R <> 1. R & A = the carrier of W implies Lin A = W )
assume that
A1: 0. R <> 1. R and
A2: 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 ) )
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 Th4;
 A is linearly-closed by A2, 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 A2, Th5; ::_thesis: verum
end;
hence  Lin A = W by VECTSP_4:30; ::_thesis: verum
end;

theorem :: MOD_3:9
for R being Ring
for V being strict LeftMod of R
for A being Subset of V st 0. R <> 1. R & A = the carrier of V holds
Lin A = V
proof
let R be Ring; ::_thesis: for V being strict LeftMod of R
for A being Subset of V st 0. R <> 1. R & A = the carrier of V holds
Lin A = V
let V be strict LeftMod of R; ::_thesis: for A being Subset of V st 0. R <> 1. R & A = the carrier of V holds
Lin A = V
let A be Subset of V; ::_thesis: ( 0. R <> 1. R & A = the carrier of V implies Lin A = V )
assume that
A1: 0. R <> 1. R and
A2: A = the carrier of V ; ::_thesis: Lin A = V
 A = the carrier of ((Omega). V) by A2;
hence  Lin A = V by A1, Th8; ::_thesis: verum
end;

theorem Th10: :: MOD_3:10
for R being Ring
for V being LeftMod of R
for A, B being Subset of V st A c= B holds
Lin A is Subspace of Lin B
proof
let R be Ring; ::_thesis: for V being LeftMod of R
for A, B being Subset of V st A c= B holds
Lin A is Subspace of Lin B
let V be LeftMod of R; ::_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 Th4;
reconsider l = l as Linear_Combination of B by A1, VECTSP_6:4;
 Sum l = v by A2;
hence  v in Lin B by Th4; ::_thesis: verum
end;
hence  Lin A is Subspace of Lin B by VECTSP_4:28; ::_thesis: verum
end;

theorem :: MOD_3:11
for R being Ring
for V being LeftMod of R
for A, B being Subset of V st Lin A = V & A c= B holds
Lin B = V
proof
let R be Ring; ::_thesis: for V being LeftMod of R
for A, B being Subset of V st Lin A = V & A c= B holds
Lin B = V
let V be LeftMod of R; ::_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 that
A1: Lin A = V and
A2: A c= B ; ::_thesis: Lin B = V
 V is Subspace of Lin B by A1, A2, Th10;
hence  Lin B = V by A1, VECTSP_4:25; ::_thesis: verum
end;

theorem :: MOD_3:12
for R being Ring
for V being LeftMod of R
for A, B being Subset of V holds Lin (A \/ B) = (Lin A) + (Lin B)
proof
let R be Ring; ::_thesis: for V being LeftMod of R
for A, B being Subset of V holds Lin (A \/ B) = (Lin A) + (Lin B)
let V be LeftMod of R; ::_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 R = 0. R;
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 Th4;
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: for x being set st x in the carrier of V holds
( ( S1[x] implies H2(x) in the carrier of R ) & ( not S1[x] implies H1(x) in the carrier of R ) )
proof
let x be set ; ::_thesis: ( x in the carrier of V implies ( ( S1[x] implies H2(x) in the carrier of R ) & ( not S1[x] implies H1(x) in the carrier of R ) ) )
assume  x in the carrier of V ; ::_thesis: ( ( S1[x] implies H2(x) in the carrier of R ) & ( not S1[x] implies H1(x) in the carrier of R ) )
then reconsider v = x as Vector of V ;
 for f being Function of the carrier of V, the carrier of R holds f . v in the carrier of R ;
hence  ( x in (Carrier l) /\ A implies l . x in the carrier of R ) ; ::_thesis: ( not S1[x] implies H1(x) in the carrier of R )
assume  not x in (Carrier l) /\ A ; ::_thesis: H1(x) in the carrier of R
thus  H1(x) in the carrier of R ; ::_thesis: verum
end;
reconsider C = (Carrier l) /\ A as finite Subset of V ;
defpred S2[ set ] means $1 in (Carrier l) \ A;
A3: for x being set st x in the carrier of V holds
( ( S2[x] implies H2(x) in the carrier of R ) & ( not S2[x] implies H1(x) in the carrier of R ) )
proof
let x be set ; ::_thesis: ( x in the carrier of V implies ( ( S2[x] implies H2(x) in the carrier of R ) & ( not S2[x] implies H1(x) in the carrier of R ) ) )
assume  x in the carrier of V ; ::_thesis: ( ( S2[x] implies H2(x) in the carrier of R ) & ( not S2[x] implies H1(x) in the carrier of R ) )
then reconsider v = x as Vector of V ;
 for g being Function of the carrier of V, the carrier of R holds g . v in the carrier of R ;
hence  ( x in (Carrier l) \ A implies l . x in the carrier of R ) ; ::_thesis: ( not S2[x] implies H1(x) in the carrier of R )
assume  not x in (Carrier l) \ A ; ::_thesis: H1(x) in the carrier of R
thus  H1(x) in the carrier of R ; ::_thesis: verum
end;
consider g being Function of the carrier of V, the carrier of R such that
A4: for x being set st x in the carrier of V holds
( ( S2[x] implies g . x = H2(x) ) & ( not S2[x] implies g . x = H1(x) ) ) from FUNCT_2:sch_5(A3);
reconsider D = (Carrier l) \ A as finite Subset of V ;
A5: 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 A6: ( 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 A6, XBOOLE_0:def_3; ::_thesis: verum
end;
reconsider g = g as Element of Funcs ( the carrier of V, the carrier of R) by FUNCT_2:8;
 for u being Vector of V st not u in D holds
g . u = 0. R by A4;
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 A7: ex u being Vector of V st
( x = u & g . u <> 0. R ) ;
assume  not x in D ; ::_thesis: contradiction
hence  contradiction by A4, A7; ::_thesis: verum
end;
then  Carrier g c= B by A5, XBOOLE_1:1;
then reconsider g = g as Linear_Combination of B by VECTSP_6:def_4;
consider f being Function of the carrier of V, the carrier of R such that
A8: 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 R) by FUNCT_2:8;
 for u being Vector of V st not u in C holds
f . u = 0. R by A8;
then reconsider f = f as Linear_Combination of V by VECTSP_6:def_1;
A9: 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 A10: ex u being Vector of V st
( x = u & f . u <> 0. R ) ;
assume  not x in C ; ::_thesis: contradiction
hence  contradiction by A8, A10; ::_thesis: verum
end;
 C c= A by XBOOLE_1:17;
then  Carrier f c= A by A9, XBOOLE_1:1;
then reconsider f = f as Linear_Combination of A 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 A8, A11
.= (l . v) + (0. R) by A4, 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
.= (0. R) + (g . v) by A8, A13
.= g . v by RLVECT_1:4
.= l . v by A4, 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. R) + (g . v) by A8, A18
.= (0. R) + (0. R) by A4, A17
.= 0. R 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 Th4;
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 Th10, 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 :: MOD_3:13
for R being Ring
for V being LeftMod of R
for A, B being Subset of V holds Lin (A /\ B) is Subspace of (Lin A) /\ (Lin B)
proof
let R be Ring; ::_thesis: for V being LeftMod of R
for A, B being Subset of V holds Lin (A /\ B) is Subspace of (Lin A) /\ (Lin B)
let V be LeftMod of R; ::_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 Th10, XBOOLE_1:17;
hence  Lin (A /\ B) is Subspace of (Lin A) /\ (Lin B) by VECTSP_5:19; ::_thesis: verum
end;

definition
let R be Ring;
let V be LeftMod of R;
let IT be Subset of V;
attrIT is base  means :Def2: :: MOD_3:def 2
( IT is linearly-independent & Lin IT = VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) );
end;

:: deftheorem Def2 defines base MOD_3:def_2_:_
 for R being Ring
for V being LeftMod of R
for IT being Subset of V holds
( IT is base iff ( IT is linearly-independent & Lin IT = VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) ) );

definition
let R be Ring;
let IT be LeftMod of R;
attrIT is free  means :Def3: :: MOD_3:def 3
 ex B being Subset of IT st B is base ;
end;

:: deftheorem Def3 defines free MOD_3:def_3_:_
 for R being Ring
for IT being LeftMod of R holds
( IT is free iff ex B being Subset of IT st B is base );

theorem Th14: :: MOD_3:14
for R being Ring
for V being LeftMod of R holds (0). V is free
proof
let R be Ring; ::_thesis: for V being LeftMod of R holds (0). V is free
let V be LeftMod of R; ::_thesis: (0). V is free
set W = (0). V;
reconsider B9 = {} the carrier of V as Subset of ((0). V) by SUBSET_1:1;
reconsider V9 = V as Subspace of V by VECTSP_4:24;
A1: B9 = {} the carrier of ((0). V) ;
then A2: B9 is linearly-independent by LMOD_5:3;
 (0). V9 = (0). ((0). V) by VECTSP_4:37;
then  Lin B9 = (0). V by A1, Th6;
then  B9 is base by A2, Def2;
hence  (0). V is free by Def3; ::_thesis: verum
end;

registration
let R be Ring;
cluster non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed free for VectSpStr over R;
existence
 ex b1 being LeftMod of R st
( b1 is strict & b1 is free )
proof
 (0). (LeftModule R) is free by Th14;
hence  ex b1 being LeftMod of R st
( b1 is strict & b1 is free ) ; ::_thesis: verum
end;
end;

         Lm2:  for R being Skew-Field
for a being Scalar of R
for V being LeftMod of R
for v being Vector of V st a <> 0. R holds
( (a ") * (a * v) = (1. R) * v & ((a ") * a) * v = (1. R) * v )
proof
let R be Skew-Field; ::_thesis: for a being Scalar of R
for V being LeftMod of R
for v being Vector of V st a <> 0. R holds
( (a ") * (a * v) = (1. R) * v & ((a ") * a) * v = (1. R) * v )
let a be Scalar of R; ::_thesis: for V being LeftMod of R
for v being Vector of V st a <> 0. R holds
( (a ") * (a * v) = (1. R) * v & ((a ") * a) * v = (1. R) * v )
let V be LeftMod of R; ::_thesis: for v being Vector of V st a <> 0. R holds
( (a ") * (a * v) = (1. R) * v & ((a ") * a) * v = (1. R) * v )
let v be Vector of V; ::_thesis: ( a <> 0. R implies ( (a ") * (a * v) = (1. R) * v & ((a ") * a) * v = (1. R) * v ) )
assume A1: a <> 0. R ; ::_thesis: ( (a ") * (a * v) = (1. R) * v & ((a ") * a) * v = (1. R) * v )
hence (a ") * (a * v) = v by VECTSP_2:31
.= (1. R) * v by VECTSP_1:def_17 ;
::_thesis: ((a ") * a) * v = (1. R) * v
thus  ((a ") * a) * v = (1. R) * v by A1, VECTSP_2:9; ::_thesis: verum
end;

theorem :: MOD_3:15
for R being Skew-Field
for V being LeftMod of R
for v being Vector of V holds
( {v} is linearly-independent iff v <> 0. V )
proof
let R be Skew-Field; ::_thesis: for V being LeftMod of R
for v being Vector of V holds
( {v} is linearly-independent iff v <> 0. V )
let V be LeftMod of R; ::_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 )
A1: 0. R <> 1. R ;
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 A1, LMOD_5:2;
hence  v <> 0. V by TARSKI:def_1; ::_thesis: verum
end;
assume A2: v <> 0. V ; ::_thesis: {v} is linearly-independent
let l be Linear_Combination of {v}; :: according to LMOD_5:def_1 ::_thesis: ( not Sum l = 0. V or Carrier l = {} )
A3: Carrier l c= {v} by VECTSP_6:def_4;
assume A4: Sum l = 0. V ; ::_thesis: Carrier l = {}
now__::_thesis:_Carrier_l_=_{}
percases ( Carrier l = {} or Carrier l = {v} ) by A3, ZFMISC_1:33;
suppose Carrier l = {} ; ::_thesis: Carrier l = {}
hence  Carrier l = {} ; ::_thesis: verum
end;
supposeA5: Carrier l = {v} ; ::_thesis: Carrier l = {}
A6: 0. V = (l . v) * v by A4, VECTSP_6:17;
now__::_thesis:_not_v_in_Carrier_l
assume  v in Carrier l ; ::_thesis: contradiction
then  l . v <> 0. R by VECTSP_6:2;
hence  contradiction by A2, A6, VECTSP_2:30; ::_thesis: verum
end;
hence  Carrier l = {} by A5, TARSKI:def_1; ::_thesis: verum
end;
end;
end;
hence  Carrier l = {} ; ::_thesis: verum
end;

theorem Th16: :: MOD_3:16
for R being Skew-Field
for V being LeftMod of R
for v1, v2 being Vector of V holds
( v1 <> v2 & {v1,v2} is linearly-independent iff ( v2 <> 0. V & ( for a being Scalar of R holds v1 <> a * v2 ) ) )
proof
let R be Skew-Field; ::_thesis: for V being LeftMod of R
for v1, v2 being Vector of V holds
( v1 <> v2 & {v1,v2} is linearly-independent iff ( v2 <> 0. V & ( for a being Scalar of R holds v1 <> a * v2 ) ) )
let V be LeftMod of R; ::_thesis: for v1, v2 being Vector of V holds
( v1 <> v2 & {v1,v2} is linearly-independent iff ( v2 <> 0. V & ( for a being Scalar of R 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 Scalar of R holds v1 <> a * v2 ) ) )
A1: 0. R <> 1. R ;
thus  ( v1 <> v2 & {v1,v2} is linearly-independent implies ( v2 <> 0. V & ( for a being Scalar of R holds v1 <> a * v2 ) ) ) ::_thesis: ( v2 <> 0. V & ( for a being Scalar of R holds v1 <> a * v2 ) implies ( v1 <> v2 & {v1,v2} is linearly-independent ) )
proof
deffunc H1( Element of V) ->  Element of the carrier of R = 0. R;
assume that
A2: v1 <> v2 and
A3: {v1,v2} is linearly-independent ; ::_thesis: ( v2 <> 0. V & ( for a being Scalar of R holds v1 <> a * v2 ) )
thus  v2 <> 0. V by A1, A3, LMOD_5:4; ::_thesis: for a being Scalar of R holds v1 <> a * v2
let a be Scalar of R; ::_thesis: v1 <> a * v2
consider f being Function of the carrier of V, the carrier of R such that
A4: ( f . v1 = - (1. R) & f . v2 = a ) and
A5: for v being Element of V st v <> v1 & v <> v2 holds
f . v = H1(v) from FUNCT_2:sch_7(A2);
reconsider f = f as Element of Funcs ( the carrier of V, the carrier of R) by FUNCT_2:8;
now__::_thesis:_for_v_being_Vector_of_V_st_not_v_in_{v1,v2}_holds_
f_._v_=_0._R
let v be Vector of V; ::_thesis: ( not v in {v1,v2} implies f . v = 0. R )
assume  not v in {v1,v2} ; ::_thesis: f . v = 0. R
then  ( v <> v1 & v <> v2 ) by TARSKI:def_2;
hence  f . v = 0. R by A5; ::_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 A6: ex u being Vector of V st
( x = u & f . u <> 0. R ) ;
assume  not x in {v1,v2} ; ::_thesis: contradiction
then  ( x <> v1 & x <> v2 ) by TARSKI:def_2;
hence  contradiction by A5, A6; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of {v1,v2} by VECTSP_6:def_4;
A7: now__::_thesis:_v1_in_Carrier_f
assume  not v1 in Carrier f ; ::_thesis: contradiction
then  0. R = - (1. R) by A4;
hence  contradiction by Th1; ::_thesis: verum
end;
set w = a * v2;
assume  v1 = a * v2 ; ::_thesis: contradiction
then  Sum f = ((- (1. R)) * (a * v2)) + (a * v2) by A2, A4, VECTSP_6:18
.= (- (a * v2)) + (a * v2) by VECTSP_1:14
.= 0. V by RLVECT_1:5 ;
hence  contradiction by A3, A7, LMOD_5:def_1; ::_thesis: verum
end;
assume A8: v2 <> 0. V ; ::_thesis: ( ex a being Scalar of R st not v1 <> a * v2 or ( v1 <> v2 & {v1,v2} is linearly-independent ) )
assume A9: for a being Scalar of R holds v1 <> a * v2 ; ::_thesis: ( v1 <> v2 & {v1,v2} is linearly-independent )
A10: (1. R) * v2 = v2 by VECTSP_1:def_17;
hence  v1 <> v2 by A9; ::_thesis: {v1,v2} is linearly-independent
let l be Linear_Combination of {v1,v2}; :: according to LMOD_5:def_1 ::_thesis: ( not Sum l = 0. V or Carrier l = {} )
assume that
A11: Sum l = 0. V and
A12: Carrier l <> {} ; ::_thesis: contradiction
A13: 0. V = ((l . v1) * v1) + ((l . v2) * v2) by A9, A10, A11, VECTSP_6:18;
set x = the Element of Carrier l;
 Carrier l c= {v1,v2} by VECTSP_6:def_4;
then A14: the Element of Carrier l in {v1,v2} by A12, TARSKI:def_3;
 the Element of Carrier l in Carrier l by A12;
then A15: ex u being Vector of V st
( the Element of Carrier l = u & l . u <> 0. R ) ;
now__::_thesis:_contradiction
percases ( l . v1 <> 0. R or ( l . v2 <> 0. R & l . v1 = 0. R ) ) by A15, A14, TARSKI:def_2;
supposeA16: l . v1 <> 0. R ; ::_thesis: contradiction
0. V = ((l . v1) ") * (((l . v1) * v1) + ((l . v2) * v2)) by A13, VECTSP_2:30
.= (((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. R) * v1) + ((((l . v1) ") * (l . v2)) * v2) by A16, Lm2
.= v1 + ((((l . v1) ") * (l . v2)) * v2) by VECTSP_1:def_17 ;
then v1 = - ((((l . v1) ") * (l . v2)) * v2) by VECTSP_1:16
.= (- (1. R)) * ((((l . v1) ") * (l . v2)) * v2) by VECTSP_1:14
.= ((- (1. R)) * (((l . v1) ") * (l . v2))) * v2 by VECTSP_1:def_16 ;
hence  contradiction by A9; ::_thesis: verum
end;
supposeA17: ( l . v2 <> 0. R & l . v1 = 0. R ) ; ::_thesis: contradiction
0. V = ((l . v2) ") * (((l . v1) * v1) + ((l . v2) * v2)) by A13, VECTSP_2:30
.= (((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) + ((1. R) * v2) by A17, Lm2
.= ((((l . v2) ") * (l . v1)) * v1) + v2 by VECTSP_1:def_17
.= ((0. R) * v1) + v2 by A17, VECTSP_1:6
.= (0. V) + v2 by VECTSP_2:30
.= v2 by RLVECT_1:def_4 ;
hence  contradiction by A8; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;

theorem :: MOD_3:17
for R being Skew-Field
for V being LeftMod of R
for v1, v2 being Vector of V holds
( ( v1 <> v2 & {v1,v2} is linearly-independent ) iff for a, b being Scalar of R st (a * v1) + (b * v2) = 0. V holds
( a = 0. R & b = 0. R ) )
proof
let R be Skew-Field; ::_thesis: for V being LeftMod of R
for v1, v2 being Vector of V holds
( ( v1 <> v2 & {v1,v2} is linearly-independent ) iff for a, b being Scalar of R st (a * v1) + (b * v2) = 0. V holds
( a = 0. R & b = 0. R ) )
let V be LeftMod of R; ::_thesis: for v1, v2 being Vector of V holds
( ( v1 <> v2 & {v1,v2} is linearly-independent ) iff for a, b being Scalar of R st (a * v1) + (b * v2) = 0. V holds
( a = 0. R & b = 0. R ) )
let v1, v2 be Vector of V; ::_thesis: ( ( v1 <> v2 & {v1,v2} is linearly-independent ) iff for a, b being Scalar of R st (a * v1) + (b * v2) = 0. V holds
( a = 0. R & b = 0. R ) )
thus  ( v1 <> v2 & {v1,v2} is linearly-independent implies for a, b being Scalar of R st (a * v1) + (b * v2) = 0. V holds
( a = 0. R & b = 0. R ) ) ::_thesis: ( ( for a, b being Scalar of R st (a * v1) + (b * v2) = 0. V holds
( a = 0. R & b = 0. R ) ) implies ( v1 <> v2 & {v1,v2} is linearly-independent ) )
proof
assume A1: ( v1 <> v2 & {v1,v2} is linearly-independent ) ; ::_thesis: for a, b being Scalar of R st (a * v1) + (b * v2) = 0. V holds
( a = 0. R & b = 0. R )
let a, b be Scalar of R; ::_thesis: ( (a * v1) + (b * v2) = 0. V implies ( a = 0. R & b = 0. R ) )
assume that
A2: (a * v1) + (b * v2) = 0. V and
A3: ( a <> 0. R or b <> 0. R ) ; ::_thesis: contradiction
now__::_thesis:_contradiction
percases ( a <> 0. R or b <> 0. R ) by A3;
supposeA4: a <> 0. R ; ::_thesis: contradiction
0. V = (a ") * ((a * v1) + (b * v2)) by A2, VECTSP_2:30
.= ((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. R) * v1) + (((a ") * b) * v2) by A4, Lm2
.= v1 + (((a ") * b) * v2) by VECTSP_1:def_17 ;
then v1 = - (((a ") * b) * v2) by VECTSP_1:16
.= (- (1. R)) * (((a ") * b) * v2) by VECTSP_1:14
.= ((- (1. R)) * ((a ") * b)) * v2 by VECTSP_1:def_16 ;
hence  contradiction by A1, Th16; ::_thesis: verum
end;
supposeA5: b <> 0. R ; ::_thesis: contradiction
0. V = (b ") * ((a * v1) + (b * v2)) by A2, VECTSP_2:30
.= ((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) + ((1. R) * v2) by A5, Lm2
.= (((b ") * a) * v1) + v2 by VECTSP_1:def_17 ;
then v2 = - (((b ") * a) * v1) by VECTSP_1:16
.= (- (1. R)) * (((b ") * a) * v1) by VECTSP_1:14
.= ((- (1. R)) * ((b ") * a)) * v1 by VECTSP_1:def_16 ;
hence  contradiction by A1, Th16; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;
assume A6: for a, b being Scalar of R st (a * v1) + (b * v2) = 0. V holds
( a = 0. R & b = 0. R ) ; ::_thesis: ( v1 <> v2 & {v1,v2} is linearly-independent )
A7: now__::_thesis:_for_a_being_Scalar_of_R_holds_not_v1_=_a_*_v2
let a be Scalar of R; ::_thesis: not v1 = a * v2
assume  v1 = a * v2 ; ::_thesis: contradiction
then  v1 = (0. V) + (a * v2) by RLVECT_1:def_4;
then  0. V = v1 - (a * v2) by RLSUB_2:61
.= v1 + ((- a) * v2) by VECTSP_1:21
.= ((1. R) * 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:def_4
.= ((0. R) * v1) + (0. V) by VECTSP_2:30
.= ((0. R) * v1) + ((1. R) * v2) by A8, VECTSP_2:30 ;
hence  contradiction by A6; ::_thesis: verum
end;
hence  ( v1 <> v2 & {v1,v2} is linearly-independent ) by A7, Th16; ::_thesis: verum
end;

theorem Th18: :: MOD_3:18
for R being Skew-Field
for V being LeftMod of R
for A being Subset of V st A is linearly-independent holds
ex B being Subset of V st
( A c= B & B is base )
proof
let R be Skew-Field; ::_thesis: for V being LeftMod of R
for A being Subset of V st A is linearly-independent holds
ex B being Subset of V st
( A c= B & B is base )
let V be LeftMod of R; ::_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 base )
let A be Subset of V; ::_thesis: ( A is linearly-independent implies ex B being Subset of V st
( A c= B & B is base ) )
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 LMOD_5:def_1 ::_thesis: ( not Sum l = 0. V or 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, LMOD_5:def_1; ::_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 base )
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 base )
thus  ( A c= B & B is linearly-independent ) by A36, A37; :: according to MOD_3:def_2 ::_thesis: Lin B = VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #)
assume  Lin B <> VectSpStr(# the carrier of V, the addF 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 LMOD_5:def_1 ::_thesis: ( not Sum l = 0. V or 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. R by VECTSP_6:2;
then  - (l . v) <> 0. R by Lm1;
then A41: ((- (l . v)) ") * ((- (l . v)) * v) = (1. R) * v by Lm2
.= v by VECTSP_1:def_17 ;
deffunc H1( Vector of V) ->  Element of the carrier of R = l . $1;
consider f being Function of the carrier of V, the carrier of R such that
A42: f . v = 0. R and
A43: 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 R) by FUNCT_2:8;
now__::_thesis:_for_u_being_Vector_of_V_st_not_u_in_(Carrier_l)_\_{v}_holds_
f_._u_=_0._R
let u be Vector of V; ::_thesis: ( not u in (Carrier l) \ {v} implies f . u = 0. R )
assume  not u in (Carrier l) \ {v} ; ::_thesis: f . u = 0. R
then  ( not u in Carrier l or u in {v} ) by XBOOLE_0:def_5;
then  ( ( l . u = 0. R & u <> v ) or u = v ) by TARSKI:def_1;
hence  f . u = 0. R 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. R ;
 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;
deffunc H2( Vector of V) ->  Element of the carrier of R = 0. R;
consider g being Function of the carrier of V, the carrier of R such that
A47: g . v = - (l . v) and
A48: for u being Vector of V st u <> v holds
g . u = H2(u) from FUNCT_2:sch_6();
reconsider g = g as Element of Funcs ( the carrier of V, the carrier of R) by FUNCT_2:8;
now__::_thesis:_for_u_being_Vector_of_V_st_not_u_in_{v}_holds_
g_._u_=_0._R
let u be Vector of V; ::_thesis: ( not u in {v} implies g . u = 0. R )
assume  not u in {v} ; ::_thesis: g . u = 0. R
then  u <> v by TARSKI:def_1;
hence  g . u = 0. R 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. R ) ;
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;
 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 ) ;
supposeA49: v = u ; ::_thesis: (f - g) . u = l . u
thus (f - g) . u = (f . u) - (g . u) by VECTSP_6:40
.= (0. R) + (- (- (l . v))) by A42, A47, A49, RLVECT_1:def_11
.= (l . v) + (0. R) by RLVECT_1:17
.= l . u by A49, RLVECT_1:4 ; ::_thesis: verum
end;
supposeA50: 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, A50
.= (l . u) - (0. R) by A48, A50
.= l . u by RLVECT_1:13 ; ::_thesis: verum
end;
end;
end;
hence  (f - g) . u = l . u ; ::_thesis: verum
end;
then A51: 0. V = (Sum f) - (Sum g) by A40, VECTSP_6:47;
 Sum g = (- (l . v)) * v by A47, VECTSP_6:17;
then  Sum f = (- (l . v)) * v by A51, VECTSP_1:19;
then  (- (l . v)) * v in Lin B by Th4;
hence  Carrier l = {} by A38, A41, STRUCT_0:def_5, VECTSP_4:21; ::_thesis: verum
end;
supposeA52: 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 A53: 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 A53, XBOOLE_0:def_3;
hence  x in B by A52, A53, TARSKI:def_1; ::_thesis: verum
end;
then  l is Linear_Combination of B by VECTSP_6:def_4;
hence  Carrier l = {} by A37, A40, LMOD_5:def_1; ::_thesis: verum
end;
end;
end;
hence  Carrier l = {} ; ::_thesis: verum
end;
 v in {v} by TARSKI:def_1;
then A54: v in B \/ {v} by XBOOLE_0:def_3;
A55: not v in B by A38, Th5, STRUCT_0:def_5;
 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, A54, A55, XBOOLE_1:7; ::_thesis: verum
end;

theorem Th19: :: MOD_3:19
for R being Skew-Field
for V being LeftMod of R
for A being Subset of V st Lin A = V holds
ex B being Subset of V st
( B c= A & B is base )
proof
let R be Skew-Field; ::_thesis: for V being LeftMod of R
for A being Subset of V st Lin A = V holds
ex B being Subset of V st
( B c= A & B is base )
let V be LeftMod of R; ::_thesis: for A being Subset of V st Lin A = V holds
ex B being Subset of V st
( B c= A & B is base )
let A be Subset of V; ::_thesis: ( Lin A = V implies ex B being Subset of V st
( B c= A & B is base ) )
A1: 0. R <> 1. R ;
defpred S1[ set ] means  ex B being Subset of V st
( B = $1 & B c= A & B is linearly-independent );
assume A2: Lin A = V ; ::_thesis: ex B being Subset of V st
( B c= A & B is base )
consider Q being set  such that
A3: for Z being set holds
( Z in Q iff ( Z in bool the carrier of V & S1[Z] ) ) from XBOOLE_0:sch_1();
A4: 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
A5: Z c= Q and
A6: 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
A7: x in X and
A8: X in Z by TARSKI:def_4;
 X in bool the carrier of V by A3, A5, A8;
hence  x in the carrier of V by A7; ::_thesis: verum
end;
then reconsider W = union Z as Subset of V ;
A9: 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 LMOD_5:def_1 ::_thesis: ( not Sum l = 0. V or Carrier l = {} )
assume that
A10: Sum l = 0. V and
A11: Carrier l <> {} ; ::_thesis: contradiction
consider f being Function such that
A12: dom f = Carrier l and
A13: 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 A11, A12, RELAT_1:42;
set F = the Choice_Function of M;
set S = rng the Choice_Function of M;
A14: now__::_thesis:_not_{}_in_M
assume  {} in M ; ::_thesis: contradiction
then consider x being set  such that
A15: x in dom f and
A16: f . x = {} by FUNCT_1:def_3;
 Carrier l c= W by VECTSP_6:def_4;
then consider X being set  such that
A17: x in X and
A18: X in Z by A12, A15, TARSKI:def_4;
reconsider X = X as Subset of V by A3, A5, A18;
 X in  {  C where C is Subset of V : ( x in C & C in Z )  }  by A17, A18;
hence  contradiction by A12, A13, A15, A16; ::_thesis: verum
end;
then A19: dom the Choice_Function of M = M by RLVECT_3:28;
then  dom the Choice_Function of M is finite by A12, FINSET_1:8;
then A20: rng the Choice_Function of M is finite by FINSET_1:8;
A21: 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
A22: x in dom the Choice_Function of M and
A23: the Choice_Function of M . x = X by FUNCT_1:def_3;
consider y being set  such that
A24: ( y in dom f & f . y = x ) by A19, A22, FUNCT_1:def_3;
A25: x =  {  C where C is Subset of V : ( y in C & C in Z )  }  by A12, A13, A24;
 X in x by A14, A19, A22, A23, ORDERS_1:def_1;
then  ex C being Subset of V st
( C = X & y in C & C in Z ) by A25;
hence  X in Z ; ::_thesis: verum
end;
A26: 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 A21;
then  X,Y are_c=-comparable by A6, 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 A19, RELAT_1:42;
then  union (rng the Choice_Function of M) in rng the Choice_Function of M by A26, A20, CARD_2:62;
then  union (rng the Choice_Function of M) in Z by A21;
then consider B being Subset of V such that
A27: B = union (rng the Choice_Function of M) and
 B c= A and
A28: B is linearly-independent by A3, A5;
 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 A29: x in Carrier l ; ::_thesis: x in union (rng the Choice_Function of M)
then A30: f . x =  {  C where C is Subset of V : ( x in C & C in Z )  }  by A13;
A31: f . x in M by A12, A29, FUNCT_1:def_3;
then  the Choice_Function of M . (f . x) in f . x by A14, ORDERS_1:def_1;
then A32: ex C being Subset of V st
( the Choice_Function of M . (f . x) = C & x in C & C in Z ) by A30;
 the Choice_Function of M . (f . x) in rng the Choice_Function of M by A19, A31, FUNCT_1:def_3;
hence  x in union (rng the Choice_Function of M) by A32, TARSKI:def_4; ::_thesis: verum
end;
then  l is Linear_Combination of B by A27, VECTSP_6:def_4;
hence  contradiction by A10, A11, A28, LMOD_5:def_1; ::_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
A33: x in X and
A34: X in Z by TARSKI:def_4;
 ex B being Subset of V st
( B = X & B c= A & B is linearly-independent ) by A3, A5, A34;
hence  x in A by A33; ::_thesis: verum
end;
hence  union Z in Q by A3, A9; ::_thesis: verum
end;
 ( {} the carrier of V c= A & {} the carrier of V is linearly-independent ) by LMOD_5:3, XBOOLE_1:2;
then  Q <> {} by A3;
then consider X being set  such that
A35: X in Q and
A36: for Z being set st Z in Q & Z <> X holds
not X c= Z by A4, ORDERS_1:67;
consider B being Subset of V such that
A37: B = X and
A38: B c= A and
A39: B is linearly-independent by A3, A35;
take  B ; ::_thesis: ( B c= A & B is base )
thus  ( B c= A & B is linearly-independent ) by A38, A39; :: according to MOD_3:def_2 ::_thesis: Lin B = VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #)
assume A40: Lin B <> VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) ; ::_thesis: contradiction
now__::_thesis:_ex_v_being_Vector_of_V_st_
(_v_in_A_&_not_v_in_Lin_B_)
assume A41: 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
A42: v = Sum l by Th4;
 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 A43: 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 A41, A43;
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 A42;
then  v in Lin F by Th4;
hence  v in Lin B by A1, Th8; ::_thesis: verum
end;
then  Lin A is Subspace of Lin B by VECTSP_4:28;
hence  contradiction by A2, A40, VECTSP_4:25; ::_thesis: verum
end;
then consider v being Vector of V such that
A44: v in A and
A45: not v in Lin B ;
A46: B \/ {v} is linearly-independent
proof
let l be Linear_Combination of B \/ {v}; :: according to LMOD_5:def_1 ::_thesis: ( not Sum l = 0. V or Carrier l = {} )
assume A47: 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. R by VECTSP_6:2;
then  - (l . v) <> 0. R by Lm1;
then A48: ((- (l . v)) ") * ((- (l . v)) * v) = (1. R) * v by Lm2
.= v by VECTSP_1:def_17 ;
deffunc H1( Vector of V) ->  Element of the carrier of R = l . $1;
consider f being Function of the carrier of V, the carrier of R such that
A49: f . v = 0. R and
A50: 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 R) by FUNCT_2:8;
now__::_thesis:_for_u_being_Vector_of_V_st_not_u_in_(Carrier_l)_\_{v}_holds_
f_._u_=_0._R
let u be Vector of V; ::_thesis: ( not u in (Carrier l) \ {v} implies f . u = 0. R )
assume  not u in (Carrier l) \ {v} ; ::_thesis: f . u = 0. R
then  ( not u in Carrier l or u in {v} ) by XBOOLE_0:def_5;
then  ( ( l . u = 0. R & u <> v ) or u = v ) by TARSKI:def_1;
hence  f . u = 0. R by A49, A50; ::_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 )
A51: 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
A52: u = x and
A53: f . u <> 0. R ;
 f . u = l . u by A49, A50, A53;
then  u in Carrier l by A53;
then  ( u in B or u in {v} ) by A51, XBOOLE_0:def_3;
hence  x in B by A49, A52, A53, TARSKI:def_1; ::_thesis: verum
end;
then reconsider f = f as Linear_Combination of B by VECTSP_6:def_4;
deffunc H2( Vector of V) ->  Element of the carrier of R = 0. R;
consider g being Function of the carrier of V, the carrier of R such that
A54: g . v = - (l . v) and
A55: for u being Vector of V st u <> v holds
g . u = H2(u) from FUNCT_2:sch_6();
reconsider g = g as Element of Funcs ( the carrier of V, the carrier of R) by FUNCT_2:8;
now__::_thesis:_for_u_being_Vector_of_V_st_not_u_in_{v}_holds_
g_._u_=_0._R
let u be Vector of V; ::_thesis: ( not u in {v} implies g . u = 0. R )
assume  not u in {v} ; ::_thesis: g . u = 0. R
then  u <> v by TARSKI:def_1;
hence  g . u = 0. R by A55; ::_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. R ) ;
then  x = v by A55;
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;
 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. R) + (- (- (l . v))) by A49, A54, A56, RLVECT_1:def_11
.= (l . v) + (0. R) 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 A50, A57
.= (l . u) - (0. R) by A55, A57
.= l . u by RLVECT_1:13 ; ::_thesis: verum
end;
end;
end;
hence  (f - g) . u = l . u ; ::_thesis: verum
end;
then A58: 0. V = (Sum f) - (Sum g) by A47, VECTSP_6:47;
 Sum g = (- (l . v)) * v by A54, VECTSP_6:17;
then  Sum f = (- (l . v)) * v by A58, VECTSP_1:19;
then  (- (l . v)) * v in Lin B by Th4;
hence  Carrier l = {} by A45, A48, 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 A39, A47, LMOD_5:def_1; ::_thesis: verum
end;
end;
end;
hence  Carrier l = {} ; ::_thesis: verum
end;
 {v} c= A by A44, ZFMISC_1:31;
then  B \/ {v} c= A by A38, XBOOLE_1:8;
then A61: B \/ {v} in Q by A3, A46;
 v in {v} by TARSKI:def_1;
then A62: v in B \/ {v} by XBOOLE_0:def_3;
 not v in B by A45, Th5;
hence  contradiction by A36, A37, A62, A61, XBOOLE_1:7; ::_thesis: verum
end;

Lm3:  for R being Skew-Field
for V being LeftMod of R ex B being Subset of V st B is base
proof
let R be Skew-Field; ::_thesis: for V being LeftMod of R ex B being Subset of V st B is base
let V be LeftMod of R; ::_thesis: ex B being Subset of V st B is base
 ex B being Subset of V st
( {} the carrier of V c= B & B is base ) by Th18, LMOD_5:3;
hence  ex B being Subset of V st B is base ; ::_thesis: verum
end;

theorem :: MOD_3:20
for R being Skew-Field
for V being LeftMod of R holds V is free
proof
let R be Skew-Field; ::_thesis: for V being LeftMod of R holds V is free
let V be LeftMod of R; ::_thesis: V is free
 ex B being Subset of V st B is base by Lm3;
hence  V is free by Def3; ::_thesis: verum
end;

definition
let R be Skew-Field;
let V be LeftMod of R;
mode Basis of V ->  Subset of V means :Def4: :: MOD_3:def 4
it is base ;
existence
 ex b1 being Subset of V st b1 is base by Lm3;
end;

:: deftheorem Def4 defines Basis MOD_3:def_4_:_
 for R being Skew-Field
for V being LeftMod of R
for b3 being Subset of V holds
( b3 is Basis of V iff b3 is base );

theorem :: MOD_3:21
for R being Skew-Field
for V being LeftMod of R
for A being Subset of V st A is linearly-independent holds
ex I being Basis of V st A c= I
proof
let R be Skew-Field; ::_thesis: for V being LeftMod of R
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 LeftMod of R; ::_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 base by Th18;
reconsider B = B as Basis of V by A2, Def4;
take  B ; ::_thesis: A c= B
thus  A c= B by A1; ::_thesis: verum
end;

theorem :: MOD_3:22
for R being Skew-Field
for V being LeftMod of R
for A being Subset of V st Lin A = V holds
ex I being Basis of V st I c= A
proof
let R be Skew-Field; ::_thesis: for V being LeftMod of R
for A being Subset of V st Lin A = V holds
ex I being Basis of V st I c= A
let V be LeftMod of R; ::_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 base by Th19;
reconsider B = B as Basis of V by A2, Def4;
take  B ; ::_thesis: B c= A
thus  B c= A by A1; ::_thesis: verum
end;