for x being object holds -infty < (F * G) . x

proof

let x be object ; :: thesis: -infty < (F * G) . x

per cases ( x in dom (F * G) or not x in dom (F * G) ) ;

suppose x in dom (F * G) ; :: thesis: -infty < (F * G) . x

then (F * G) . x = F . (G . x) by FUNCT_1:12;
hence -infty < (F * G) . x by MESFUNC5:def 5; :: thesis: verum

end;

suppose not x in dom (F * G) ; :: thesis: -infty < (F * G) . x

hence -infty < (F * G) . x by FUNCT_1:def 2; :: thesis: verum

end;

end;

end;

hence for b₁ being Function of X,ExtREAL st b₁ = F * G holds
b₁ is without-infty by MESFUNC5:def 5; :: thesis: verum