theorem :: MEASURE9:34

for F being FinSequence of ExtREAL
for G being ExtREAL_sequence st ( for i being Nat holds F . i = G . i ) holds
( F is nonnegative iff G is nonnegative )