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
(f | ].-infty,s.]) +* (g | [.s,+infty.[) = (f | ].-infty,s.[) +* (g | [.s,+infty.[) by FUZZY_6:35;
hence (f | ].-infty,s.]) +* (g | [.s,+infty.[) is Function of REAL,REAL by FUZZY_6:18; :: thesis: verum