let V be RealLinearSpace; :: thesis: for A being Subset of V holds Lin (Z_Lin A) = Lin A
let A be Subset of V; :: thesis: Lin (Z_Lin A) = Lin A
for x being object st x in A holds
x in Z_Lin A by Th12;
then A c= Z_Lin A ;
then A1: Lin A is Subspace of Lin (Z_Lin A) by RLVECT_3:20;
reconsider W = the carrier of (Lin A) as Subset of V by RLSUB_1:def 2;
Lin (Z_Lin A) is Subspace of Lin W by Th8, RLVECT_3:20;
then Lin (Z_Lin A) is Subspace of Lin A by RLVECT_3:18;
hence Lin (Z_Lin A) = Lin A by A1, RLSUB_1:26; :: thesis: verum