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 Th5;
hence Sum l = 0. V by Th11; :: thesis: verum