let c be Real; :: thesis: for f, g being Function of REAL,REAL holds (f | ].-infty,c.[) +* (g | [.c,+infty.[) = (f | ].-infty,c.]) +* (g | [.c,+infty.[)
let f, g be Function of REAL,REAL; :: thesis: (f | ].-infty,c.[) +* (g | [.c,+infty.[) = (f | ].-infty,c.]) +* (g | [.c,+infty.[)
set f1 = (f | ].-infty,c.[) +* (g | [.c,+infty.[);
set f2 = (f | ].-infty,c.]) +* (g | [.c,+infty.[);
A4: ( -infty < c & c < +infty ) by XXREAL_0:12, XXREAL_0:9, XREAL_0:def 1;
A2: dom ((f | ].-infty,c.[) +* (g | [.c,+infty.[)) = (dom (f | ].-infty,c.[)) \/ (dom (g | [.c,+infty.[)) by FUNCT_4:def 1
.= ].-infty,c.[ \/ (dom (g | [.c,+infty.[)) by FUNCT_2:def 1
.= ].-infty,c.[ \/ [.c,+infty.[ by FUNCT_2:def 1
.= ].-infty,+infty.[ by XXREAL_1:173, A4
.= ].-infty,c.] \/ [.c,+infty.[ by XXREAL_1:172, A4
.= (dom (f | ].-infty,c.])) \/ [.c,+infty.[ by FUNCT_2:def 1
.= (dom (f | ].-infty,c.])) \/ (dom (g | [.c,+infty.[)) by FUNCT_2:def 1
.= dom ((f | ].-infty,c.]) +* (g | [.c,+infty.[)) by FUNCT_4:def 1 ;
Dg: dom (g | [.c,+infty.[) = [.c,+infty.[ by FUNCT_2:def 1;
for x being object st x in dom ((f | ].-infty,c.[) +* (g | [.c,+infty.[)) holds
((f | ].-infty,c.[) +* (g | [.c,+infty.[)) . x = ((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x

proof

let x be object ; :: thesis: ( x in dom ((f | ].-infty,c.[) +* (g | [.c,+infty.[)) implies ((f | ].-infty,c.[) +* (g | [.c,+infty.[)) . x = ((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x )
assume A3: x in dom ((f | ].-infty,c.[) +* (g | [.c,+infty.[)) ; :: thesis: ((f | ].-infty,c.[) +* (g | [.c,+infty.[)) . x = ((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x
dom ((f | ].-infty,c.[) +* (g | [.c,+infty.[)) = (dom (f | ].-infty,c.[)) \/ (dom (g | [.c,+infty.[)) by FUNCT_4:def 1
.= ].-infty,c.[ \/ (dom (g | [.c,+infty.[)) by FUNCT_2:def 1
.= ].-infty,c.[ \/ [.c,+infty.[ by FUNCT_2:def 1
.= REAL by XXREAL_1:224, XXREAL_1:173, A4 ;
then reconsider x = x as Real by A3;

per cases ( x >= c or x < c ) ;

suppose C1: x >= c ; :: thesis: ((f | ].-infty,c.[) +* (g | [.c,+infty.[)) . x = ((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x

((f | ].-infty,c.[) +* (g | [.c,+infty.[)) . x = (g | [.c,+infty.[) . x by FUNCT_4:13, Dg, C1, XXREAL_1:236;
hence ((f | ].-infty,c.[) +* (g | [.c,+infty.[)) . x = ((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x by FUNCT_4:13, Dg, C1, XXREAL_1:236; :: thesis: verum

end;

suppose C2: x < c ; :: thesis: ((f | ].-infty,c.[) +* (g | [.c,+infty.[)) . x = ((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x

].-infty,c.[ c= ].-infty,c.] by XXREAL_1:21;
then C6: x in ].-infty,c.] by XXREAL_1:233, C2;
C4: not x in dom (g | [.c,+infty.[) by C2, XXREAL_1:236;
((f | ].-infty,c.[) +* (g | [.c,+infty.[)) . x = (f | ].-infty,c.[) . x by FUNCT_4:11, C4
.= f . x by FUNCT_1:49, XXREAL_1:233, C2
.= (f | ].-infty,c.]) . x by FUNCT_1:49, C6 ;
hence ((f | ].-infty,c.[) +* (g | [.c,+infty.[)) . x = ((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x by FUNCT_4:11, C4; :: thesis: verum

end;

end;

end;

hence (f | ].-infty,c.[) +* (g | [.c,+infty.[) = (f | ].-infty,c.]) +* (g | [.c,+infty.[) by FUNCT_1:2, A2; :: thesis: verum