let RS be RealLinearSpace; :: thesis: for f being non empty FinSequence of RS holds Z_Lin (rng f) = Z_Lin f
let f be non empty FinSequence of RS; :: thesis: Z_Lin (rng f) = Z_Lin f
for x being set holds
( x in Z_Lin (rng f) iff x in Z_Lin f )

proof

let x be set ; :: thesis: ( x in Z_Lin (rng f) iff x in Z_Lin f )

hereby :: thesis: ( x in Z_Lin f implies x in Z_Lin (rng f) )

assume x in Z_Lin (rng f) ; :: thesis: x in Z_Lin f
then consider g, h being FinSequence of RS, a being integer-valued FinSequence such that
P1: ( x = Sum h & rng g c= rng f & len g = len h & len g = len a & ( for i being Nat st i in Seg (len g) holds
h /. i = (a . i) * (g /. i) ) ) by LM0450;
rng f c= Z_Lin f by SLM0300;
hence x in Z_Lin f by P1, XBOOLE_1:1, SLM0400; :: thesis: verum

end;

assume x in Z_Lin f ; :: thesis: x in Z_Lin (rng f)
then consider g being len f -long FinSequence of RS, a being len f -long integer-valued FinSequence such that
P1: ( x = Sum g & ( for i being Nat st i in Seg (len f) holds
g /. i = (a . i) * (f /. i) ) ) by SLM001;
( len f = len g & len a = len f ) by FINSEQ_1:def 18;
hence x in Z_Lin (rng f) by P1, LM0440; :: thesis: verum

end;

hence Z_Lin (rng f) = Z_Lin f by TARSKI:2; :: thesis: verum