let s be Real; :: thesis: for f, g being Function of REAL,REAL holds (f | ].-infty,s.[) +* (g | [.s,+infty.[) is Function of REAL,REAL
let f, g be Function of REAL,REAL; :: thesis: (f | ].-infty,s.[) +* (g | [.s,+infty.[) is Function of REAL,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;
Dg: 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 ;
for x being object st x in REAL holds
((f | ].-infty,s.[) +* (g | [.s,+infty.[)) . x in REAL by XREAL_0:def 1;
hence (f | ].-infty,s.[) +* (g | [.s,+infty.[) is Function of REAL,REAL by FUNCT_2:3, Dg; :: thesis: verum