let a, b, c be Real; :: thesis: for f, g being Function of REAL,REAL st a <= b & b <= c holds
((f | ].-infty,b.]) +* (g | [.b,+infty.[)) | [.a,c.] = (f | [.a,b.]) +* (g | [.b,c.])
let f, g be Function of REAL,REAL; :: thesis: ( a <= b & b <= c implies ((f | ].-infty,b.]) +* (g | [.b,+infty.[)) | [.a,c.] = (f | [.a,b.]) +* (g | [.b,c.]) )
assume A1: ( a <= b & b <= c ) ; :: thesis: ((f | ].-infty,b.]) +* (g | [.b,+infty.[)) | [.a,c.] = (f | [.a,b.]) +* (g | [.b,c.])
set F = (f | ].-infty,b.]) +* (g | [.b,+infty.[);
(f | ].-infty,b.]) +* (g | [.b,+infty.[) = (f | ].-infty,b.[) +* (g | [.b,+infty.[) by FUZZY_6:35;
then reconsider F = (f | ].-infty,b.]) +* (g | [.b,+infty.[) as Function of REAL,REAL by FUZZY_6:18;
A3: dom ((f | [.a,b.]) +* (g | [.b,c.])) = (dom (f | [.a,b.])) \/ (dom (g | [.b,c.])) by FUNCT_4:def 1
.= [.a,b.] \/ (dom (g | [.b,c.])) by FUNCT_2:def 1
.= [.a,b.] \/ [.b,c.] by FUNCT_2:def 1
.= [.a,c.] by XXREAL_1:165, A1 ;
A2: dom (F | [.a,c.]) = [.a,c.] by FUNCT_2:def 1;
for x being object st x in dom (((f | ].-infty,b.]) +* (g | [.b,+infty.[)) | [.a,c.]) holds
(((f | ].-infty,b.]) +* (g | [.b,+infty.[)) | [.a,c.]) . x = ((f | [.a,b.]) +* (g | [.b,c.])) . x

proof

let x be object ; :: thesis: ( x in dom (((f | ].-infty,b.]) +* (g | [.b,+infty.[)) | [.a,c.]) implies (((f | ].-infty,b.]) +* (g | [.b,+infty.[)) | [.a,c.]) . x = ((f | [.a,b.]) +* (g | [.b,c.])) . x )
assume A4a: x in dom (((f | ].-infty,b.]) +* (g | [.b,+infty.[)) | [.a,c.]) ; :: thesis: (((f | ].-infty,b.]) +* (g | [.b,+infty.[)) | [.a,c.]) . x = ((f | [.a,b.]) +* (g | [.b,c.])) . x
then reconsider x = x as Real by A2;
A5: ( a <= x & x <= c ) by XXREAL_1:1, A4a, A2;
A7: dom (g | [.b,+infty.[) = [.b,+infty.[ by FUNCT_2:def 1;
A8: dom (g | [.b,c.]) = [.b,c.] by FUNCT_2:def 1;

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

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

(((f | ].-infty,b.]) +* (g | [.b,+infty.[)) | [.a,c.]) . x = ((f | ].-infty,b.]) +* (g | [.b,+infty.[)) . x by FUNCT_1:49, A4a, A2
.= (g | [.b,+infty.[) . x by FUNCT_4:13, A6, XXREAL_1:236, A7
.= g . x by FUNCT_1:49, A6, XXREAL_1:236
.= (g | [.b,c.]) . x by FUNCT_1:49, A6, A5, XXREAL_1:1
.= ((f | [.a,b.]) +* (g | [.b,c.])) . x by FUNCT_4:13, A6, A5, XXREAL_1:1, A8 ;
hence (((f | ].-infty,b.]) +* (g | [.b,+infty.[)) | [.a,c.]) . x = ((f | [.a,b.]) +* (g | [.b,c.])) . x ; :: thesis: verum

end;

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

].-infty,b.[ c= ].-infty,b.] by XXREAL_1:21;
then A10: x in ].-infty,b.] by XXREAL_1:233, B1;
A11: x in [.a,b.] by B1, A5;
A12: not x in [.b,c.] by B1, XXREAL_1:1;
(((f | ].-infty,b.]) +* (g | [.b,+infty.[)) | [.a,c.]) . x = ((f | ].-infty,b.]) +* (g | [.b,+infty.[)) . x by FUNCT_1:49, A4a, A2
.= (f | ].-infty,b.]) . x by FUNCT_4:11, A7, XXREAL_1:236, B1
.= f . x by FUNCT_1:49, A10
.= (f | [.a,b.]) . x by FUNCT_1:49, A11
.= ((f | [.a,b.]) +* (g | [.b,c.])) . x by FUNCT_4:11, A8, A12 ;
hence (((f | ].-infty,b.]) +* (g | [.b,+infty.[)) | [.a,c.]) . x = ((f | [.a,b.]) +* (g | [.b,c.])) . x ; :: thesis: verum

end;

end;

end;

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