let A be Subset of V; :: thesis: ( A is linearly-independent implies A is affinely-independent )

assume A is linearly-independent ; :: thesis: A is affinely-independent

then for L being Linear_Combination of A st Sum L = 0. V & sum L = 0 holds

Carrier L = {} ;

hence A is affinely-independent by Th42; :: thesis: verum

assume A is linearly-independent ; :: thesis: A is affinely-independent

then for L being Linear_Combination of A st Sum L = 0. V & sum L = 0 holds

Carrier L = {} ;

hence A is affinely-independent by Th42; :: thesis: verum