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 object st x in A holds
x in Z_Lin A by Th12;
then A c= Z_Lin A ;
then A1: Z_Lin A c= Z_Lin (Z_Lin A) by Th13;
Z_Lin (Z_Lin A) c= Z_Lin A

proof

let x be object ; :: 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 INT -valued FinSequence such that
A2: ( 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 Lm2;
thus x in Z_Lin A by A2, Th35; :: thesis: verum

end;

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