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

end;

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;then ( r * I = {} V or r * I = {(0. V)} ) by ZFMISC_1:33;

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

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

end;

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

Carrier L = {}

hence
r * I is affinely-independent
by Th42; :: thesis: verumCarrier 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;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