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

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;

hence v + I is affinely-independent by Th42; :: thesis: verum