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:39;
hence r * I is affinely-independent ; :: thesis: verum

end;

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

now

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 by RLVECT_1:23 ;
A5: ( Carrier ((r " ) (*) L) = (r " ) * (Carrier L) & Carrier L c= r * I ) by A1, Th23, RLVECT_2:def 8;
(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 8;
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 7;
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 7; :: thesis: verum

end;

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

end;

end;