let A be non empty closed_interval Subset of REAL; :: thesis: for b being Real
for f, g, h being Function of REAL,REAL st h = (f | ].-infty,b.[) +* (g | [.b,+infty.[) & f . b = g . b holds
( ( b <= lower_bound A implies h | A = g | A ) & ( upper_bound A <= b implies h | A = f | A ) )
let b be Real; :: thesis: for f, g, h being Function of REAL,REAL st h = (f | ].-infty,b.[) +* (g | [.b,+infty.[) & f . b = g . b holds
( ( b <= lower_bound A implies h | A = g | A ) & ( upper_bound A <= b implies h | A = f | A ) )
let f, g, h be Function of REAL,REAL; :: thesis: ( h = (f | ].-infty,b.[) +* (g | [.b,+infty.[) & f . b = g . b implies ( ( b <= lower_bound A implies h | A = g | A ) & ( upper_bound A <= b implies h | A = f | A ) ) )
assume that
A1: h = (f | ].-infty,b.[) +* (g | [.b,+infty.[) and
A2: f . b = g . b ; :: thesis: ( ( b <= lower_bound A implies h | A = g | A ) & ( upper_bound A <= b implies h | A = f | A ) )
XX: ( b <= lower_bound A implies h | A = g | A )

proof

assume A3: b <= lower_bound A ; :: thesis: h | A = g | A
B3: dom (h | A) = A by FUNCT_2:def 1
.= dom (g | A) by FUNCT_2:def 1 ;
for x being object st x in dom (h | A) holds
(h | A) . x = (g | A) . x

proof

let x be object ; :: thesis: ( x in dom (h | A) implies (h | A) . x = (g | A) . x )
assume A4: x in dom (h | A) ; :: thesis: (h | A) . x = (g | A) . x
then reconsider x = x as Real ;
x in A by A4;
then x in [.(lower_bound A),(upper_bound A).] by INTEGRA1:4;
then ( lower_bound A <= x & x <= upper_bound A ) by XXREAL_1:1;
then x in [.b,+infty.[ by XXREAL_1:236, XXREAL_0:2, A3;
then B5: x in dom (g | [.b,+infty.[) by FUNCT_2:def 1;
(h | A) . x = ((f | ].-infty,b.[) +* (g | [.b,+infty.[)) . x by A1, FUNCT_1:47, A4
.= (g | [.b,+infty.[) . x by B5, FUNCT_4:13
.= g . x by FUNCT_1:47, B5 ;
hence (h | A) . x = (g | A) . x by FUNCT_1:49, A4; :: thesis: verum

end;

hence h | A = g | A by B3, FUNCT_1:2; :: thesis: verum

end;

( upper_bound A <= b implies h | A = f | A )

proof

assume A3: upper_bound A <= b ; :: thesis: h | A = f | A
B3: dom (h | A) = A by FUNCT_2:def 1
.= dom (f | A) by FUNCT_2:def 1 ;
for x being object st x in dom (h | A) holds
(h | A) . x = (f | A) . x

proof

let x be object ; :: thesis: ( x in dom (h | A) implies (h | A) . x = (f | A) . x )
assume A4: x in dom (h | A) ; :: thesis: (h | A) . x = (f | A) . x
then reconsider x = x as Real ;
x in A by A4;
then x in [.(lower_bound A),(upper_bound A).] by INTEGRA1:4;
then ( lower_bound A <= x & x <= upper_bound A ) by XXREAL_1:1;
then A10: x <= b by XXREAL_0:2, A3;

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

suppose C1: x = b ; :: thesis: (h | A) . x = (f | A) . x

then x in [.b,+infty.[ by XXREAL_1:236;
then C3: x in dom (g | [.b,+infty.[) by FUNCT_2:def 1;
(h | A) . x = ((f | ].-infty,b.[) +* (g | [.b,+infty.[)) . x by A1, FUNCT_1:47, A4
.= (g | [.b,+infty.[) . x by FUNCT_4:13, C3
.= f . x by C1, A2, FUNCT_1:49, XXREAL_1:236 ;
hence (h | A) . x = (f | A) . x by FUNCT_1:49, A4; :: thesis: verum

end;

suppose x <> b ; :: thesis: (h | A) . x = (f | A) . x

then C4: x < b by A10, XXREAL_0:1;
then C5: not x in dom (g | [.b,+infty.[) by XXREAL_1:236;
(h | A) . x = ((f | ].-infty,b.[) +* (g | [.b,+infty.[)) . x by A1, FUNCT_1:47, A4
.= (f | ].-infty,b.[) . x by C5, FUNCT_4:11
.= f . x by FUNCT_1:49, C4, XXREAL_1:233 ;
hence (h | A) . x = (f | A) . x by FUNCT_1:49, A4; :: thesis: verum

end;

end;

end;

hence h | A = f | A by B3, FUNCT_1:2; :: thesis: verum

end;

hence ( ( b <= lower_bound A implies h | A = g | A ) & ( upper_bound A <= b implies h | A = f | A ) ) by XX; :: thesis: verum