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:22;
A1: Sum l = 0. V by RLVECT_2:30;
rng l c= INT by Th7;
hence 0. V in Z_Lin A by A1; :: thesis: verum