for F, G being FinSequence of ExtREAL holds
( ( F is V339() & G is V339() implies F ^ G is V339() ) & ( F is V340() & G is V340() implies F ^ G is V340() ) )