let F, G be FinSequence of ExtREAL ; :: thesis: ( ( F is V339() & G is V339() implies F ^ G is V339() ) & ( F is V340() & G is V340() implies F ^ G is V340() ) )
hereby :: thesis: ( F is V340() & G is V340() implies F ^ G is V340() )
assume ( F is V339() & G is V339() ) ; :: thesis: F ^ G is V339()
then A1: ( not -infty in rng F & not -infty in rng G ) by MESFUNC5:def 3;
rng (F ^ G) = (rng F) \/ (rng G) by FINSEQ_1:31;
then not -infty in rng (F ^ G) by A1, XBOOLE_0:def 3;
hence F ^ G is V339() by MESFUNC5:def 3; :: thesis: verum
end;
assume ( F is V340() & G is V340() ) ; :: thesis: F ^ G is V340()
then A2: ( not +infty in rng F & not +infty in rng G ) by MESFUNC5:def 4;
rng (F ^ G) = (rng F) \/ (rng G) by FINSEQ_1:31;
then not +infty in rng (F ^ G) by A2, XBOOLE_0:def 3;
hence F ^ G is V340() by MESFUNC5:def 4; :: thesis: verum