let V be RealLinearSpace; :: thesis: for A being Subset of V holds 0. V in Z_Lin A
let A be Subset of V; :: thesis: 0. V in Z_Lin A
reconsider l = ZeroLC V as Linear_Combination of A by RLVECT_2:34;
P1: Sum l = 0. V by RLVECT_2:48;
rng l c= INT by LM003;
hence 0. V in Z_Lin A by P1; :: thesis: verum