theorem Th34: :: MEASURE9:36

for F being FinSequence of ExtREAL
for k being Nat holds
( ( F is V251() implies F | k is V251() ) & ( F is V252() implies F | k is V252() ) )