let V be RealLinearSpace; :: thesis: {} the carrier of V is linearly-independent

let l be Linear_Combination of {} the carrier of V; :: according to RLVECT_3:def 1 :: thesis: ( Sum l = 0. V implies Carrier l = {} )

Carrier l c= {} by RLVECT_2:def 6;

hence ( Sum l = 0. V implies Carrier l = {} ) ; :: thesis: verum

let l be Linear_Combination of {} the carrier of V; :: according to RLVECT_3:def 1 :: thesis: ( Sum l = 0. V implies Carrier l = {} )

Carrier l c= {} by RLVECT_2:def 6;

hence ( Sum l = 0. V implies Carrier l = {} ) ; :: thesis: verum