for F being FinSequence of ExtREAL
for k being Nat holds
( ( F is V339() implies F /^ k is V339() ) & ( F is V340() implies F /^ k is V340() ) )