let V be non empty right_complementable Abelian add-associative right_zeroed CLSStruct ; :: thesis: for l being C_Linear_Combination of {} the carrier of V holds Sum l = 0. V
let l be C_Linear_Combination of {} the carrier of V; :: thesis: Sum l = 0. V
l = ZeroCLC V by Th35;
hence Sum l = 0. V by Lm2; :: thesis: verum