let V be RealLinearSpace; :: thesis: for A being Subset of V holds Z_Lin A c= the carrier of (Lin A)
let A be Subset of V; :: thesis: Z_Lin A c= the carrier of (Lin A)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Z_Lin A or x in the carrier of (Lin A) )
assume x in Z_Lin A ; :: thesis: x in the carrier of (Lin A)
then consider l1 being Linear_Combination of A such that
A1: ( x = Sum l1 & rng l1 c= INT ) ;
x in Lin A by A1, RLVECT_3:14;
hence x in the carrier of (Lin A) by STRUCT_0:def 5; :: thesis: verum