let RS be RealLinearSpace; :: thesis: for f being FinSequence of RS
for x being set holds
( x in Z_Lin f iff ex g being len b₁ -element FinSequence of RS ex a being INT -valued len b₁ -element FinSequence st
( x = Sum g & ( for i being Nat st i in Seg (len f) holds
g /. i = (a . i) * (f /. i) ) ) )
let f be FinSequence of RS; :: thesis: for x being set holds
( x in Z_Lin f iff ex g being len f -element FinSequence of RS ex a being INT -valued len f -element FinSequence st
( x = Sum g & ( for i being Nat st i in Seg (len f) holds
g /. i = (a . i) * (f /. i) ) ) )
let x be set ; :: thesis: ( x in Z_Lin f iff ex g being len f -element FinSequence of RS ex a being INT -valued len f -element FinSequence st
( x = Sum g & ( for i being Nat st i in Seg (len f) holds
g /. i = (a . i) * (f /. i) ) ) )

hereby :: thesis: ( ex g being len f -element FinSequence of RS ex a being INT -valued len f -element FinSequence st
( x = Sum g & ( for i being Nat st i in Seg (len f) holds
g /. i = (a . i) * (f /. i) ) ) implies x in Z_Lin f )

assume x in Z_Lin f ; :: thesis: ex g being len f -element FinSequence of RS ex s being INT -valued len f -element FinSequence st
( x = Sum g & ( for i being Nat st i in Seg (len f) holds
g /. i = (s . i) * (f /. i) ) )
then consider g being len f -element FinSequence of RS such that
A1: ( x = Sum g & ex s being INT -valued len f -element FinSequence st
for i being Nat st i in Seg (len f) holds
g /. i = (s . i) * (f /. i) ) ;
consider s being INT -valued len f -element FinSequence such that
A2: for i being Nat st i in Seg (len f) holds
g /. i = (s . i) * (f /. i) by A1;
take g = g; :: thesis: ex s being INT -valued len f -element FinSequence st
( x = Sum g & ( for i being Nat st i in Seg (len f) holds
g /. i = (s . i) * (f /. i) ) )
take s = s; :: thesis: ( x = Sum g & ( for i being Nat st i in Seg (len f) holds
g /. i = (s . i) * (f /. i) ) )
thus ( x = Sum g & ( for i being Nat st i in Seg (len f) holds
g /. i = (s . i) * (f /. i) ) ) by A1, A2; :: thesis: verum

end;

assume ex g being len f -element FinSequence of RS ex a being INT -valued len f -element FinSequence st
( x = Sum g & ( for i being Nat st i in Seg (len f) holds
g /. i = (a . i) * (f /. i) ) ) ; :: thesis: x in Z_Lin f
hence x in Z_Lin f ; :: thesis: verum