set vI = v + I;

now :: thesis: for L being Linear_Combination of v + I st Sum L = 0. V & sum L = 0 holds

Carrier L = {}

hence
v + I is affinely-independent
by Th42; :: thesis: verumCarrier L = {}

let L be Linear_Combination of v + I; :: thesis: ( Sum L = 0. V & sum L = 0 implies Carrier L = {} )

assume that

A1: Sum L = 0. V and

A2: sum L = 0 ; :: thesis: Carrier L = {}

set vL = (- v) + L;

A3: sum ((- v) + L) = 0 by A2, Th37;

A4: ( Carrier ((- v) + L) = (- v) + (Carrier L) & Carrier L c= v + I ) by Th16, RLVECT_2:def 6;

(- v) + (v + I) = ((- v) + v) + I by Th5

.= (0. V) + I by RLVECT_1:5

.= I by Th6 ;

then Carrier ((- v) + L) c= I by A4, RLTOPSP1:8;

then A5: (- v) + L is Linear_Combination of I by RLVECT_2:def 6;

Sum ((- v) + L) = (0 * (- v)) + (0. V) by A1, A2, Th39

.= (0. V) + (0. V) by RLVECT_1:10

.= 0. V ;

then Carrier ((- v) + L) = {} by A3, A5, Th42;

then A6: (- v) + L = ZeroLC V by RLVECT_2:def 5;

L = (0. V) + L by Th21

.= (v + (- v)) + L by RLVECT_1:5

.= v + (ZeroLC V) by A6, Th19

.= ZeroLC V by Th20 ;

hence Carrier L = {} by RLVECT_2:def 5; :: thesis: verum

end;assume that

A1: Sum L = 0. V and

A2: sum L = 0 ; :: thesis: Carrier L = {}

set vL = (- v) + L;

A3: sum ((- v) + L) = 0 by A2, Th37;

A4: ( Carrier ((- v) + L) = (- v) + (Carrier L) & Carrier L c= v + I ) by Th16, RLVECT_2:def 6;

(- v) + (v + I) = ((- v) + v) + I by Th5

.= (0. V) + I by RLVECT_1:5

.= I by Th6 ;

then Carrier ((- v) + L) c= I by A4, RLTOPSP1:8;

then A5: (- v) + L is Linear_Combination of I by RLVECT_2:def 6;

Sum ((- v) + L) = (0 * (- v)) + (0. V) by A1, A2, Th39

.= (0. V) + (0. V) by RLVECT_1:10

.= 0. V ;

then Carrier ((- v) + L) = {} by A3, A5, Th42;

then A6: (- v) + L = ZeroLC V by RLVECT_2:def 5;

L = (0. V) + L by Th21

.= (v + (- v)) + L by RLVECT_1:5

.= v + (ZeroLC V) by A6, Th19

.= ZeroLC V by Th20 ;

hence Carrier L = {} by RLVECT_2:def 5; :: thesis: verum