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 b1 being Function of X,ExtREAL st b1 = F * G holds
b1 is without-infty by MESFUNC5:def 5; :: thesis: verum