let s be Real; :: thesis: for f, g being Function of REAL,REAL holds
( dom ((f | ].-infty,s.]) +* (g | [.s,+infty.[)) = REAL & dom ((f | ].-infty,s.[) +* (g | [.s,+infty.[)) = REAL )
let f, g be Function of REAL,REAL; :: thesis: ( dom ((f | ].-infty,s.]) +* (g | [.s,+infty.[)) = REAL & dom ((f | ].-infty,s.[) +* (g | [.s,+infty.[)) = REAL )
set F = (f | ].-infty,s.[) +* (g | [.s,+infty.[);
set g1 = f | ].-infty,s.[;
set g2 = g | [.s,+infty.[;
D3: ( -infty < s & s < +infty ) by XXREAL_0:9, XXREAL_0:12, XREAL_0:def 1;
dom ((f | ].-infty,s.[) +* (g | [.s,+infty.[)) = (dom (f | ].-infty,s.[)) \/ (dom (g | [.s,+infty.[)) by FUNCT_4:def 1
.= ].-infty,s.[ \/ (dom (g | [.s,+infty.[)) by FUNCT_2:def 1
.= ].-infty,s.[ \/ [.s,+infty.[ by FUNCT_2:def 1
.= REAL by XXREAL_1:224, XXREAL_1:173, D3 ;
hence ( dom ((f | ].-infty,s.]) +* (g | [.s,+infty.[)) = REAL & dom ((f | ].-infty,s.[) +* (g | [.s,+infty.[)) = REAL ) by FUZZY_6:35; :: thesis: verum