now

let x be set ; :: thesis: ( x in { (Sum g) where g is len f -long FinSequence of RS : ex a being len f -long integer-valued 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 -long FinSequence of RS : ex a being len f -long integer-valued 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 -long FinSequence of RS st
( x = Sum g & ex a being len f -long integer-valued 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 -long FinSequence of RS : ex a being len f -long integer-valued 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