let K be Ring; :: thesis: for V being LeftMod of K

for b being FinSequence of V st b is one-to-one holds

( rng b is linearly-independent iff 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) )

let V be LeftMod of K; :: thesis: for b being FinSequence of V st b is one-to-one holds

( rng b is linearly-independent iff 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) )

let b be FinSequence of V; :: thesis: ( b is one-to-one implies ( rng b is linearly-independent iff 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) ) )

assume AS: b is one-to-one ; :: thesis: ( rng b is linearly-independent iff 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) )

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: rng b is linearly-independent

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 = {}

for b being FinSequence of V st b is one-to-one holds

( rng b is linearly-independent iff 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) )

let V be LeftMod of K; :: thesis: for b being FinSequence of V st b is one-to-one holds

( rng b is linearly-independent iff 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) )

let b be FinSequence of V; :: thesis: ( b is one-to-one implies ( rng b is linearly-independent iff 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) ) )

assume AS: b is one-to-one ; :: thesis: ( rng b is linearly-independent iff 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) )

hereby :: thesis: ( ( 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) ) implies rng b is linearly-independent )

assume AS2:
for r being FinSequence of Kfor 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) ) implies rng b is linearly-independent )

assume AS1:
rng b is linearly-independent
; :: thesis: 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)

let r be FinSequence of K; :: thesis: 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)

let rb be FinSequence of V; :: thesis: ( 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 implies r = (Seg (len r)) --> (0. K) )

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: r = (Seg (len r)) --> (0. K)

DRB: dom r = dom b by A1, FINSEQ_3:29;

defpred S_{1}[ 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_{1}[x,y] )

XA5: for x being object st x in the carrier of V holds

S_{1}[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;

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

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

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

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

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

r . z = 0. K

hence r = (Seg (len r)) --> (0. K) by FINSEQ_1:def 3; :: thesis: verum

end;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)

let r be FinSequence of K; :: thesis: 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)

let rb be FinSequence of V; :: thesis: ( 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 implies r = (Seg (len r)) --> (0. K) )

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: r = (Seg (len r)) --> (0. K)

DRB: dom r = dom b by A1, FINSEQ_3:29;

defpred S

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

proof

consider L being Function of the carrier of V, the carrier of K such that
let x be object ; :: thesis: ( x in the carrier of V implies ex y being object st

( y in the carrier of K & S_{1}[x,y] ) )

assume x in the carrier of V ; :: thesis: ex y being object st

( y in the carrier of K & S_{1}[x,y] )

then reconsider x = x as Vector of V ;

end;( y in the carrier of K & S

assume x in the carrier of V ; :: thesis: ex y being object st

( y in the carrier of K & S

then reconsider x = x as Vector of V ;

per cases
( x in rng b or not x in rng b )
;

end;

suppose XA3:
x in rng b
; :: thesis: ex y being object st

( y in the carrier of K & S_{1}[x,y] )

( y in the carrier of K & S

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_{1}[x,y]
by XA3;

hence ex y being object st

( y in the carrier of K & S_{1}[x,y] )
; :: thesis: verum

end;(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

hence ex y being object st

( y in the carrier of K & S

XA5: for x being object st x in the carrier of V holds

S

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: for x being object st x in Carrier L holds

x in rng b

then
Carrier L c= rng b
;x in rng b

let x be object ; :: thesis: ( x in Carrier L implies x in rng b )

assume that

XA7: x in Carrier L and

XA8: not x in rng b ; :: thesis: contradiction

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: verum

end;assume that

XA7: x in Carrier L and

XA8: not x in rng b ; :: thesis: contradiction

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: verum

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

then A4:
L | (rng b) = r * (b ")
by XA41, XA43, RELAT_1:62;
let i be object ; :: thesis: ( i in dom (L | (rng b)) implies (L | (rng b)) . i = (r * (b ")) . i )

assume ASXA: i in dom (L | (rng b)) ; :: thesis: (L | (rng b)) . i = (r * (b ")) . i

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: verum

end;assume ASXA: i in dom (L | (rng b)) ; :: thesis: (L | (rng b)) . i = (r * (b ")) . i

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: verum

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

then ZA1:
rb = L (#) b
by ZA2, ZA3;
let i be Nat; :: thesis: ( i in dom (L (#) b) implies (L (#) b) . i = rb . i )

assume ZA40: i in dom (L (#) b) ; :: thesis: (L (#) b) . i = rb . i

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: verum

end;assume ZA40: i in dom (L (#) b) ; :: thesis: (L (#) b) . i = rb . i

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: verum

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

then A8:
b .: { i where i is Nat : ( i in dom r & r . i <> 0. K ) } c= Carrier L
;
let z be object ; :: thesis: ( z in b .: { i where i is Nat : ( i in dom r & r . i <> 0. K ) } implies z in Carrier L )

assume z in b .: { i where i is Nat : ( i in dom r & r . i <> 0. K ) } ; :: thesis: z in Carrier L

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: verum

end;assume z in b .: { i where i is Nat : ( i in dom r & r . i <> 0. K ) } ; :: thesis: z in Carrier L

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: verum

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

then A9:
{ i where i is Nat : ( i in dom r & r . i <> 0. K ) } c= dom b
;
let z be object ; :: thesis: ( z in { i where i is Nat : ( i in dom r & r . i <> 0. K ) } implies z in dom b )

assume z in { i where i is Nat : ( i in dom r & r . i <> 0. K ) } ; :: thesis: z in dom b

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: verum

end;assume z in { i where i is Nat : ( i in dom r & r . i <> 0. K ) } ; :: thesis: z in dom b

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: verum

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

proof
end;

for z being object st z in dom r holds per cases
( rng b = {} or rng b <> {} )
;

end;

suppose
rng b = {}
; :: thesis: { i where i is Nat : ( i in dom r & r . i <> 0. K ) } = {}

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: verum

end;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: verum

proof

assume
{ i where i is Nat : ( i in dom r & r . i <> 0. K ) } <> {}
; :: thesis: contradiction

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: verum

end;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: verum

suppose Y1:
rng b <> {}
; :: thesis: { i where i is Nat : ( i in dom r & r . i <> 0. K ) } = {}

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: verum

end;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: verum

r . z = 0. K

proof

then
r = (dom r) --> (0. K)
by FUNCOP_1:11;
let z be object ; :: thesis: ( z in dom r implies r . z = 0. K )

assume X1: z in dom r ; :: thesis: r . z = 0. K

assume X2: r . z <> 0. K ; :: thesis: contradiction

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: verum

end;assume X1: z in dom r ; :: thesis: r . z = 0. K

assume X2: r . z <> 0. K ; :: thesis: contradiction

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: verum

hence r = (Seg (len r)) --> (0. K) by FINSEQ_1:def 3; :: thesis: verum

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: rng b is linearly-independent

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

hence
rng b is linearly-independent
by LMBASE2X; :: thesis: verum
let L be Linear_Combination of rng b; :: thesis: ( ex F being FinSequence of the carrier of V st

( F is one-to-one & rng F = rng b & Sum (L (#) F) = 0. V ) implies Carrier L = {} )

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: Carrier L = {}

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)

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: contradiction

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: verum

end;( F is one-to-one & rng F = rng b & Sum (L (#) F) = 0. V ) implies Carrier L = {} )

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: Carrier L = {}

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

Sum rb = Sum (L (#) F)
by AS, A4, A5, EQSUMLF;
let i be Nat; :: thesis: ( i in dom rb implies rb . i = (r /. i) * (b /. i) )

assume B231: i in dom rb ; :: thesis: rb . i = (r /. i) * (b /. i)

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: verum

end;assume B231: i in dom rb ; :: thesis: rb . i = (r /. i) * (b /. i)

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: verum

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: contradiction

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: verum