let V be RealLinearSpace; :: thesis: for l being Linear_Combination of {} the carrier of V holds Sum l = 0. V

let l be Linear_Combination of {} the carrier of V; :: thesis: Sum l = 0. V

l = ZeroLC V by Th23;

hence Sum l = 0. V by Lm2; :: thesis: verum

let l be Linear_Combination of {} the carrier of V; :: thesis: Sum l = 0. V

l = ZeroLC V by Th23;

hence Sum l = 0. V by Lm2; :: thesis: verum