now :: thesis: for x being object st x in { (Sum g) where g is len f -element FinSequence of RS : ex a being INT -valued len f -element FinSequence st
for i being Nat st i in Seg (len f) holds
g /. i = (a . i) * (f /. i) } holds
x in the carrier of RS
let x be object ; :: thesis: ( x in { (Sum g) where g is len f -element FinSequence of RS : ex a being INT -valued len f -element FinSequence st
for i being Nat st i in Seg (len f) holds
g /. i = (a . i) * (f /. i) } implies x in the carrier of RS )
assume x in { (Sum g) where g is len f -element FinSequence of RS : ex a being INT -valued len f -element FinSequence st
for i being Nat st i in Seg (len f) holds
g /. i = (a . i) * (f /. i) } ; :: thesis: x in the carrier of RS
then ex g being len f -element FinSequence of RS st
( x = Sum g & ex a being INT -valued len f -element FinSequence st
for i being Nat st i in Seg (len f) holds
g /. i = (a . i) * (f /. i) ) ;
hence x in the carrier of RS ; :: thesis: verum
end;
hence { (Sum g) where g is len f -element FinSequence of RS : ex a being INT -valued len f -element FinSequence st
for i being Nat st i in Seg (len f) holds
g /. i = (a . i) * (f /. i) } is Subset of RS by TARSKI:def 3; :: thesis: verum