let V be RealLinearSpace; :: thesis: for A being Subset of V holds Z_Lin (Z_Lin A) = Z_Lin A
let A be Subset of V; :: thesis: Z_Lin (Z_Lin A) = Z_Lin A
for x being set st x in A holds
x in Z_Lin A by Th18;
then A c= Z_Lin A by TARSKI:def 3;
then P2: Z_Lin A c= Z_Lin (Z_Lin A) by Th23;
Z_Lin (Z_Lin A) c= Z_Lin A

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Z_Lin (Z_Lin A) or x in Z_Lin A )
assume x in Z_Lin (Z_Lin A) ; :: thesis: x in Z_Lin A
then consider g1, h1 being FinSequence of V, a1 being integer-valued FinSequence such that
P1: ( x = Sum h1 & rng g1 c= Z_Lin A & len g1 = len h1 & len g1 = len a1 & ( for i being Nat st i in Seg (len g1) holds
h1 /. i = (a1 . i) * (g1 /. i) ) ) by LM0450;
thus x in Z_Lin A by P1, SLM0450; :: thesis: verum

end;

hence Z_Lin (Z_Lin A) = Z_Lin A by XBOOLE_0:def 10, P2; :: thesis: verum