let S be Subset of V; :: thesis: ( S is empty implies S is linearly-independent )
assume A1: S is empty ; :: thesis: S is linearly-independent
let l be Linear_Combination of S; :: according to VECTSP_7:def 1 :: thesis: ( Sum l = 0. V implies Carrier l = {} )
Carrier l c= {} by A1, VECTSP_6:def 4;
hence ( Sum l = 0. V implies Carrier l = {} ) ; :: thesis: verum