let a, b, c be Real; :: thesis: for f, g being Function of REAL,REAL st a <= c & c <= b holds
(f | [.a,c.[) +* (g | [.c,b.]) = (f | [.a,c.]) +* (g | [.c,b.])
let f, g be Function of REAL,REAL; :: thesis: ( a <= c & c <= b implies (f | [.a,c.[) +* (g | [.c,b.]) = (f | [.a,c.]) +* (g | [.c,b.]) )
assume A4: ( a <= c & c <= b ) ; :: thesis: (f | [.a,c.[) +* (g | [.c,b.]) = (f | [.a,c.]) +* (g | [.c,b.])
set f1 = (f | [.a,c.[) +* (g | [.c,b.]);
set f2 = (f | [.a,c.]) +* (g | [.c,b.]);
A2: dom ((f | [.a,c.[) +* (g | [.c,b.])) = (dom (f | [.a,c.[)) \/ (dom (g | [.c,b.])) by FUNCT_4:def 1
.= [.a,c.[ \/ (dom (g | [.c,b.])) by FUNCT_2:def 1
.= [.a,c.[ \/ [.c,b.] by FUNCT_2:def 1
.= [.a,b.] by XXREAL_1:166, A4
.= [.a,c.] \/ [.c,b.] by XXREAL_1:165, A4
.= (dom (f | [.a,c.])) \/ [.c,b.] by FUNCT_2:def 1
.= (dom (f | [.a,c.])) \/ (dom (g | [.c,b.])) by FUNCT_2:def 1
.= dom ((f | [.a,c.]) +* (g | [.c,b.])) by FUNCT_4:def 1 ;
Dg: dom (g | [.c,b.]) = [.c,b.] by FUNCT_2:def 1;
for x being object st x in dom ((f | [.a,c.[) +* (g | [.c,b.])) holds
((f | [.a,c.[) +* (g | [.c,b.])) . x = ((f | [.a,c.]) +* (g | [.c,b.])) . x

proof

let x be object ; :: thesis: ( x in dom ((f | [.a,c.[) +* (g | [.c,b.])) implies ((f | [.a,c.[) +* (g | [.c,b.])) . x = ((f | [.a,c.]) +* (g | [.c,b.])) . x )
assume A3: x in dom ((f | [.a,c.[) +* (g | [.c,b.])) ; :: thesis: ((f | [.a,c.[) +* (g | [.c,b.])) . x = ((f | [.a,c.]) +* (g | [.c,b.])) . x
A5: dom ((f | [.a,c.[) +* (g | [.c,b.])) = (dom (f | [.a,c.[)) \/ (dom (g | [.c,b.])) by FUNCT_4:def 1
.= [.a,c.[ \/ (dom (g | [.c,b.])) by FUNCT_2:def 1
.= [.a,c.[ \/ [.c,b.] by FUNCT_2:def 1
.= [.a,b.] by XXREAL_1:166, A4 ;
then reconsider x = x as Real by A3;
A6: ( a <= x & x <= b ) by A5, A3, XXREAL_1:1;

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

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

((f | [.a,c.[) +* (g | [.c,b.])) . x = (g | [.c,b.]) . x by FUNCT_4:13, Dg, C1, XXREAL_1:1, A6;
hence ((f | [.a,c.[) +* (g | [.c,b.])) . x = ((f | [.a,c.]) +* (g | [.c,b.])) . x by FUNCT_4:13, Dg, C1, XXREAL_1:1, A6; :: thesis: verum

end;

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

C6: x in [.a,c.] by A6, C2;
C4: not x in dom (g | [.c,b.]) by C2, XXREAL_1:1;
((f | [.a,c.[) +* (g | [.c,b.])) . x = (f | [.a,c.[) . x by FUNCT_4:11, C4
.= f . x by FUNCT_1:49, XXREAL_1:3, A6, C2
.= (f | [.a,c.]) . x by FUNCT_1:49, C6 ;
hence ((f | [.a,c.[) +* (g | [.c,b.])) . x = ((f | [.a,c.]) +* (g | [.c,b.])) . x by FUNCT_4:11, C4; :: thesis: verum

end;

end;

end;

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