let c be Real; :: thesis: for f, g being PartFunc of REAL,REAL st ].-infty,c.] c= dom f & [.c,+infty.[ c= dom g holds
(f | ].-infty,c.[) +* (g | [.c,+infty.[) = (f | ].-infty,c.]) +* (g | [.c,+infty.[)
let f, g be PartFunc of REAL,REAL; :: thesis: ( ].-infty,c.] c= dom f & [.c,+infty.[ c= dom g implies (f | ].-infty,c.[) +* (g | [.c,+infty.[) = (f | ].-infty,c.]) +* (g | [.c,+infty.[) )
assume A1: ( ].-infty,c.] c= dom f & [.c,+infty.[ c= dom g ) ; :: 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;
].-infty,c.[ c= ].-infty,c.] by XXREAL_1:21;
then a1: ].-infty,c.[ c= dom f by A1;
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 RELAT_1:62, a1
.= ].-infty,c.[ \/ [.c,+infty.[ by RELAT_1:62, A1
.= ].-infty,+infty.[ by XXREAL_1:173, A4
.= ].-infty,c.] \/ [.c,+infty.[ by XXREAL_1:172, A4
.= (dom (f | ].-infty,c.])) \/ [.c,+infty.[ by RELAT_1:62, A1
.= (dom (f | ].-infty,c.])) \/ (dom (g | [.c,+infty.[)) by RELAT_1:62, A1
.= dom ((f | ].-infty,c.]) +* (g | [.c,+infty.[)) by FUNCT_4:def 1 ;
Dg: dom (g | [.c,+infty.[) = [.c,+infty.[ by RELAT_1:62, A1;
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 x in dom ((f | ].-infty,c.[) +* (g | [.c,+infty.[)) ; :: thesis: ((f | ].-infty,c.[) +* (g | [.c,+infty.[)) . x = ((f | ].-infty,c.]) +* (g | [.c,+infty.[)) . x
then reconsider x = x as Real ;

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

then ((f | ].-infty,c.[) +* (g | [.c,+infty.[)) . x = (g | [.c,+infty.[) . x by FUNCT_4:13, Dg, 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;
not x in [.c,+infty.[ by C2, XXREAL_1:236;
then C4: not x in dom (g | [.c,+infty.[) by RELAT_1:62, A1;
then ((f | ].-infty,c.[) +* (g | [.c,+infty.[)) . x = (f | ].-infty,c.[) . x by FUNCT_4:11
.= 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