let F, G be FinSequence of ExtREAL ; :: thesis: ( ( F is without-infty & G is without-infty implies F ^ G is without-infty ) & ( F is without+infty & G is without+infty implies F ^ G is without+infty ) )

hereby :: thesis: ( F is without+infty & G is without+infty implies F ^ G is without+infty )

assume ( F is without-infty & G is without-infty ) ; :: thesis: F ^ G is without-infty
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 without-infty by MESFUNC5:def 3; :: thesis: verum

end;

assume ( F is without+infty & G is without+infty ) ; :: thesis: F ^ G is without+infty
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 without+infty by MESFUNC5:def 4; :: thesis: verum