theorem LM100: :: PRSUBSET:6

for x being real-valued FinSequence
for I being set st x is positive & I c= dom x & I <> {} holds
( Seq (x,I) is positive & Seq (x,I) <> {} )