per cases ( r = 0 or r <> 0 ) ;

suppose r = 0 ; :: thesis: r * I is affinely-independent

then r * I c= {(0. V)} by Th12;
then ( r * I = {} V or r * I = {(0. V)} ) by ZFMISC_1:33;
hence r * I is affinely-independent ; :: thesis: verum

end;

suppose A1: r <> 0 ; :: thesis: r * I is affinely-independent

now :: thesis: for L being Linear_Combination of r * I st Sum L = 0. V & sum L = 0 holds
Carrier L = {}

let L be Linear_Combination of r * I; :: thesis: ( Sum L = 0. V & sum L = 0 implies Carrier L = {} )
assume that
A2: Sum L = 0. V and
A3: sum L = 0 ; :: thesis: Carrier L = {}
set rL = (r ") (*) L;
A4: Sum ((r ") (*) L) = (r ") * (0. V) by A2, Th40
.= 0. V ;
A5: ( Carrier ((r ") (*) L) = (r ") * (Carrier L) & Carrier L c= r * I ) by A1, Th23, RLVECT_2:def 6;
(r ") * (r * I) = ((r ") * r) * I by Th10
.= 1 * I by A1, XCMPLX_0:def 7
.= I by Th11 ;
then Carrier ((r ") (*) L) c= I by A5, Th9;
then A6: (r ") (*) L is Linear_Combination of I by RLVECT_2:def 6;
sum ((r ") (*) L) = 0 by A1, A3, Th38;
then Carrier ((r ") (*) L) = {} by A4, A6, Th42;
then A7: (r ") (*) L = ZeroLC V by RLVECT_2:def 5;
L = 1 (*) L by Th28
.= (r * (r ")) (*) L by A1, XCMPLX_0:def 7
.= r (*) (ZeroLC V) by A7, Th27
.= ZeroLC V by Th26 ;
hence Carrier L = {} by RLVECT_2:def 5; :: thesis: verum

end;

hence r * I is affinely-independent by Th42; :: thesis: verum

end;

end;