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 object holds
( x in Z_Lin (rng f) iff x in Z_Lin f )

proof

let x be object ; :: 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 INT -valued FinSequence such that
A1: ( 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 Lm2;
rng f c= Z_Lin f by Th31;
hence x in Z_Lin f by A1, Th32, XBOOLE_1:1; :: thesis: verum

end;

assume x in Z_Lin f ; :: thesis: x in Z_Lin (rng f)
then consider g being len f -element FinSequence of RS, a being INT -valued len f -element FinSequence such that
A2: ( x = Sum g & ( for i being Nat st i in Seg (len f) holds
g /. i = (a . i) * (f /. i) ) ) by Th26;
( len f = len g & len a = len f ) by CARD_1:def 7;
hence x in Z_Lin (rng f) by A2, Lm1; :: thesis: verum

end;

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