let K be Ring; :: thesis:
let V be LeftMod of K; :: thesis:
let b be FinSequence of V; :: thesis:
assume AS: b is one-to-one ; :: thesis:

hereby :: thesis:

assume AS1: rng b is linearly-independent ; :: thesis:
let r be FinSequence of K; :: thesis:
let rb be FinSequence of V; :: thesis:
assume that
A1: ( len r = len b & len rb = len b ) and
A2: for i being Nat st i in dom rb holds
rb . i = (r /. i) * (b /. i) and
A3: Sum rb = 0. V ; :: thesis:
DRB: dom r = dom b by A1, FINSEQ_3:29;
defpred S₁[ object , object ] means ( ( $1 in rng b & $2 = (r * (b ")) . $1 ) or ( not $1 in rng b & $2 = 0. K ) );
XA2: for x being object st x in the carrier of V holds
ex y being object st
( y in the carrier of K & S₁[x,y] )

proof

let x be object ; :: thesis:
assume x in the carrier of V ; :: thesis:
then reconsider x = x as Vector of V ;

per cases ;

suppose XA3: x in rng b ; :: thesis:

then XA31: x in dom (b ") by FUNCT_1:33, AS;
(b ") . x in rng (b ") by FUNCT_1:3, XA31;
then (b ") . x in dom r by AS, DRB, FUNCT_1:33;
then r . ((b ") . x) in rng r by FUNCT_1:3;
then reconsider y = (r * (b ")) . x as Element of K by XA31, FUNCT_1:13;
S₁[x,y] by XA3;
hence ex y being object st
( y in the carrier of K & S₁[x,y] ) ; :: thesis:

end;

suppose not x in rng b ; :: thesis:

hence ex y being object st
( y in the carrier of K & S₁[x,y] ) ; :: thesis:

end;

consider L being Function of the carrier of V, the carrier of K such that
XA5: for x being object st x in the carrier of V holds
S₁[x,L . x] from FUNCT_2:sch 1(XA2);
XA6: for v being Vector of V st not v in rng b holds
L . v = 0. K by XA5;
L is Element of Funcs ( the carrier of V, the carrier of K) by FUNCT_2:8;
then reconsider L = L as Linear_Combination of V by XA6, VECTSP_6:def 1;

now :: thesis:

let x be object ; :: thesis:
assume that
XA7: x in Carrier L and
XA8: not x in rng b ; :: thesis:
consider v being Vector of V such that
XA9: x = v and
XA10: L . v <> 0. K by XA7;
thus contradiction by XA5, XA8, XA9, XA10; :: thesis:

end;

then Carrier L c= rng b ;
then reconsider L = L as Linear_Combination of rng b by VECTSP_6:def 4;
XA41: dom L = the carrier of V by FUNCT_2:def 1;
rng (b ") = dom r by AS, DRB, FUNCT_1:33;
then XA43: dom (r * (b ")) = dom (b ") by RELAT_1:27
.= rng b by FUNCT_1:33, AS ;
for i being object st i in dom (L | (rng b)) holds
(L | (rng b)) . i = (r * (b ")) . i

proof

let i be object ; :: thesis:
assume ASXA: i in dom (L | (rng b)) ; :: thesis:
then XA45: i in rng b ;
(L | (rng b)) . i = L . i by ASXA, FUNCT_1:49;
hence (L | (rng b)) . i = (r * (b ")) . i by XA5, XA45; :: thesis:

end;

then A4: L | (rng b) = r * (b ") by XA41, XA43, RELAT_1:62;
ZA2: dom rb = Seg (len b) by A1, FINSEQ_1:def 3;
ZA3: dom (L (#) b) = Seg (len (L (#) b)) by FINSEQ_1:def 3
.= Seg (len b) by VECTSP_6:def 5 ;
for i being Nat st i in dom (L (#) b) holds
(L (#) b) . i = rb . i

proof

let i be Nat; :: thesis:
assume ZA40: i in dom (L (#) b) ; :: thesis:
then ZA41: (L (#) b) . i = (L . (b /. i)) * (b /. i) by VECTSP_6:def 5;
ZA42: i in dom b by FINSEQ_1:def 3, ZA40, ZA3;
then ZA45: b . i in rng b by FUNCT_1:3;
then ZA49: b . i in dom (b ") by AS, FUNCT_1:33;
L . (b . i) = (r * (b ")) . (b . i) by XA5, ZA45
.= r . ((b ") . (b . i)) by ZA49, FUNCT_1:13
.= r . i by AS, FUNCT_1:34, ZA42
.= r /. i by PARTFUN1:def 6, ZA42, DRB ;
then L . (b /. i) = r /. i by ZA42, PARTFUN1:def 6;
hence (L (#) b) . i = rb . i by A2, ZA2, ZA3, ZA40, ZA41; :: thesis:

end;

then ZA1: rb = L (#) b by ZA2, ZA3;
reconsider B = Carrier L as finite Subset of V ;
set F0 = canFS B;
BS3: rng (canFS B) = B by FUNCT_2:def 3;
rng (canFS B) c= the carrier of V by TARSKI:def 3;
then reconsider F0 = canFS B as FinSequence of V by FINSEQ_1:def 4;
reconsider C = (rng b) \ B as finite Subset of V ;
set G0 = canFS C;
BS4: rng (canFS C) = C by FUNCT_2:def 3;
rng (canFS C) c= the carrier of V by TARSKI:def 3;
then reconsider G0 = canFS C as FinSequence of V by FINSEQ_1:def 4;
BS5: (rng F0) /\ (rng G0) = B /\ ((rng b) \ B) by BS3, FUNCT_2:def 3
.= (B /\ (rng b)) \ B by XBOOLE_1:49
.= {} by XBOOLE_1:37, XBOOLE_1:17 ;
then BS6: F0 ^ G0 is one-to-one by LMBASE2A;
BS7: rng (F0 ^ G0) = B \/ ((rng b) \ B) by BS3, BS4, BS5, LMBASE2A
.= (rng b) \/ B by XBOOLE_1:39
.= rng b by VECTSP_6:def 4, XBOOLE_1:12 ;
BS10: L (#) G0 = (dom G0) --> (0. V) by BS3, BS5, LMBASE2C;
then aa: dom (L (#) G0) = dom G0 by FUNCOP_1:13;
A51: Sum (L (#) b) = Sum (L (#) (F0 ^ G0)) by EQSUMLF, BS6, BS7, AS
.= Sum ((L (#) F0) ^ (L (#) G0)) by VECTSP_6:13
.= (Sum (L (#) F0)) + (Sum (L (#) G0)) by RLVECT_1:41
.= (Sum (L (#) F0)) + (0. V) by BS10, LMBASE2D, aa
.= Sum L by BS3, VECTSP_6:def 6 ;
A6: Carrier L = {} by AS1, A3, A51, ZA1, VECTSP_7:def 1;
set N = { i where i is Nat : ( i in dom r & r . i <> 0. K ) } ;
for z being object st z in b .: { i where i is Nat : ( i in dom r & r . i <> 0. K ) } holds
z in Carrier L

proof

let z be object ; :: thesis:
assume z in b .: { i where i is Nat : ( i in dom r & r . i <> 0. K ) } ; :: thesis:
then consider x being object such that
D70: ( x in dom b & x in { i where i is Nat : ( i in dom r & r . i <> 0. K ) } & z = b . x ) by FUNCT_1:def 6;
reconsider x = x as Nat by D70;
consider i being Nat such that
A80: ( x = i & i in dom r & r . i <> 0. K ) by D70;
A81: b . i in rng b by A80, DRB, FUNCT_1:3;
then A86: b . i in dom (b ") by AS, FUNCT_1:33;
A83: L . (b . i) = (L | (rng b)) . (b . i) by A80, DRB, FUNCT_1:3, FUNCT_1:49
.= r . ((b ") . (b . i)) by A4, A86, FUNCT_1:13
.= r . i by AS, A80, DRB, FUNCT_1:34 ;
reconsider bi = b . i as Element of V by A81;
L . bi <> 0. K by A83, A80;
hence z in Carrier L by D70, A80; :: thesis:

end;

then A8: b .: { i where i is Nat : ( i in dom r & r . i <> 0. K ) } c= Carrier L ;
for z being object st z in { i where i is Nat : ( i in dom r & r . i <> 0. K ) } holds
z in dom b

proof

let z be object ; :: thesis:
assume z in { i where i is Nat : ( i in dom r & r . i <> 0. K ) } ; :: thesis:
then consider i being Nat such that
A80: ( z = i & i in dom r & r . i <> 0. K ) ;
thus z in dom b by A80, A1, FINSEQ_3:29; :: thesis:

end;

then A9: { i where i is Nat : ( i in dom r & r . i <> 0. K ) } c= dom b ;
A7: { i where i is Nat : ( i in dom r & r . i <> 0. K ) } = {}

proof

per cases ;

suppose rng b = {} ; :: thesis:

then dom b = {} by RELAT_1:42;
then Y2: Seg (len r) = {} by A1, FINSEQ_1:def 3;
thus { i where i is Nat : ( i in dom r & r . i <> 0. K ) } = {} :: thesis:

proof

assume { i where i is Nat : ( i in dom r & r . i <> 0. K ) } <> {} ; :: thesis:
then consider z being object such that
Y3: z in { i where i is Nat : ( i in dom r & r . i <> 0. K ) } by XBOOLE_0:def 1;
ex i being Nat st
( z = i & i in dom r & r . i <> 0. K ) by Y3;
hence contradiction by Y2, FINSEQ_1:def 3; :: thesis:

end;

suppose Y1: rng b <> {} ; :: thesis:

b is Function of (dom b),(rng b) by FUNCT_2:1;
then { i where i is Nat : ( i in dom r & r . i <> 0. K ) } c= {} by A6, A8, A9, Y1;
hence { i where i is Nat : ( i in dom r & r . i <> 0. K ) } = {} ; :: thesis:

end;

for z being object st z in dom r holds
r . z = 0. K

proof

let z be object ; :: thesis:
assume X1: z in dom r ; :: thesis:
assume X2: r . z <> 0. K ; :: thesis:
reconsider i = z as Nat by X1;
i in { i where i is Nat : ( i in dom r & r . i <> 0. K ) } by X1, X2;
hence contradiction by A7; :: thesis:

end;

then r = (dom r) --> (0. K) by FUNCOP_1:11;
hence r = (Seg (len r)) --> (0. K) by FINSEQ_1:def 3; :: thesis:

end;

assume AS2: for r being FinSequence of K
for rb being FinSequence of V st len r = len b & len rb = len b & ( for i being Nat st i in dom rb holds
rb . i = (r /. i) * (b /. i) ) & Sum rb = 0. V holds
r = (Seg (len r)) --> (0. K) ; :: thesis:
for L being Linear_Combination of rng b st ex F being FinSequence of the carrier of V st
( F is one-to-one & rng F = rng b & Sum (L (#) F) = 0. V ) holds
Carrier L = {}

proof

let L be Linear_Combination of rng b; :: thesis:
given F being FinSequence of the carrier of V such that A4: F is one-to-one and
A5: rng F = rng b and
A6: Sum (L (#) F) = 0. V ; :: thesis:
reconsider rb = L (#) b as FinSequence of V ;
rng (L * b) c= the carrier of K ;
then reconsider r = L * b as FinSequence of K by FINSEQ_1:def 4;
B24: len rb = len b by VECTSP_6:def 5;
( rng b c= the carrier of V & dom L = the carrier of V ) by FUNCT_2:def 1;
then X2: dom r = dom b by RELAT_1:27;
then B21: len r = len b by FINSEQ_3:29;
B23: for i being Nat st i in dom rb holds
rb . i = (r /. i) * (b /. i)

proof

let i be Nat; :: thesis:
assume B231: i in dom rb ; :: thesis:
then B233: i in dom b by B24, FINSEQ_3:29;
i in dom r by B231, B24, X2, FINSEQ_3:29;
then r /. i = r . i by PARTFUN1:def 6
.= L . (b . i) by B233, FUNCT_1:13
.= L . (b /. i) by B233, PARTFUN1:def 6 ;
hence rb . i = (r /. i) * (b /. i) by B231, VECTSP_6:def 5; :: thesis:

end;

Sum rb = Sum (L (#) F) by AS, A4, A5, EQSUMLF;
then A5: r = (Seg (len r)) --> (0. K) by A6, AS2, B21, B23, B24;
A6: Carrier L c= rng b by VECTSP_6:def 4;
assume Carrier L <> {} ; :: thesis:
then consider x being object such that
A7: x in Carrier L by XBOOLE_0:def 1;
consider v being Element of V such that
A8: ( x = v & L . v <> 0. K ) by A7;
consider i being object such that
A9: ( i in dom b & v = b . i ) by A6, A7, A8, FUNCT_1:def 3;
A10: r . i <> 0. K by A8, A9, FUNCT_1:13;
i in Seg (len r) by A9, X2, FINSEQ_1:def 3;
hence contradiction by A5, A10, FUNCOP_1:7; :: thesis:

end;

hence rng b is linearly-independent by LMBASE2X; :: thesis: