let a, b, c be Real; :: thesis: for f, g, h being Function of REAL,REAL st a <= c & h | [.a,c.] = (f | [.a,b.]) +* (g | [.b,c.]) & f . b = g . b holds
( ( b <= a implies h | [.a,c.] = g | [.a,c.] ) & ( c <= b implies h | [.a,c.] = f | [.a,c.] ) )
let f, g, h be Function of REAL,REAL; :: thesis: ( a <= c & h | [.a,c.] = (f | [.a,b.]) +* (g | [.b,c.]) & f . b = g . b implies ( ( b <= a implies h | [.a,c.] = g | [.a,c.] ) & ( c <= b implies h | [.a,c.] = f | [.a,c.] ) ) )
assume that
A1: a <= c and
A2: h | [.a,c.] = (f | [.a,b.]) +* (g | [.b,c.]) and
A3: f . b = g . b ; :: thesis: ( ( b <= a implies h | [.a,c.] = g | [.a,c.] ) & ( c <= b implies h | [.a,c.] = f | [.a,c.] ) )
A4: ( b <= a implies h | [.a,c.] = g | [.a,c.] )

proof

assume A5X: b <= a ; :: thesis: h | [.a,c.] = g | [.a,c.]
then A5: [.a,c.] c= [.b,c.] by XXREAL_1:34;
h | [.a,c.] = (h | [.b,c.]) | [.a,c.] by XXREAL_1:34, A5X, RELAT_1:74;
then reconsider H = (h | [.b,c.]) | [.a,c.] as Function of [.a,c.],REAL ;
(h | [.b,c.]) | [.a,c.] = g | [.a,c.]

proof

A6: dom H = [.a,c.] by FUNCT_2:def 1
.= dom (g | [.a,c.]) by FUNCT_2:def 1 ;
for x being object st x in dom (g | [.a,c.]) holds
((h | [.b,c.]) | [.a,c.]) . x = (g | [.a,c.]) . x

proof

let x be object ; :: thesis: ( x in dom (g | [.a,c.]) implies ((h | [.b,c.]) | [.a,c.]) . x = (g | [.a,c.]) . x )
assume Dg: x in dom (g | [.a,c.]) ; :: thesis: ((h | [.b,c.]) | [.a,c.]) . x = (g | [.a,c.]) . x
A8: x in [.b,c.] by A5, Dg;
A9: x in dom (g | [.b,c.]) by FUNCT_2:def 1, A8;
((h | [.b,c.]) | [.a,c.]) . x = (h | [.b,c.]) . x by FUNCT_1:49, Dg
.= h . x by FUNCT_1:49, A5, Dg
.= ((f | [.a,b.]) +* (g | [.b,c.])) . x by A2, FUNCT_1:49, Dg
.= (g | [.b,c.]) . x by A9, FUNCT_4:13
.= g . x by FUNCT_1:49, A5, Dg ;
hence ((h | [.b,c.]) | [.a,c.]) . x = (g | [.a,c.]) . x by FUNCT_1:49, Dg; :: thesis: verum

end;

hence (h | [.b,c.]) | [.a,c.] = g | [.a,c.] by FUNCT_1:2, A6; :: thesis: verum

end;

hence h | [.a,c.] = g | [.a,c.] by RELAT_1:74, A5X, XXREAL_1:34; :: thesis: verum

end;

( c <= b implies h | [.a,c.] = f | [.a,c.] )

proof

assume A10: c <= b ; :: thesis: h | [.a,c.] = f | [.a,c.]
then A5: [.a,c.] c= [.a,b.] by XXREAL_1:34;
reconsider H1 = h | [.a,c.] as Function of [.a,c.],REAL ;
reconsider F1 = f | [.a,c.] as Function of [.a,c.],REAL ;
for x being object st x in [.a,c.] holds
H1 . x = F1 . x

proof

let x be object ; :: thesis: ( x in [.a,c.] implies H1 . x = F1 . x )
assume B2: x in [.a,c.] ; :: thesis: H1 . x = F1 . x
then B3: x in [.a,b.] by A5;

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

suppose B5: c = b ; :: thesis: H1 . x = F1 . x

B6: x in dom (f | [.a,b.]) by FUNCT_2:def 1, B3;
TO: for x being object st x in (dom (f | [.a,b.])) /\ (dom (g | [.b,c.])) holds
(f | [.a,b.]) . x = (g | [.b,c.]) . x

proof

let x be object ; :: thesis: ( x in (dom (f | [.a,b.])) /\ (dom (g | [.b,c.])) implies (f | [.a,b.]) . x = (g | [.b,c.]) . x )
assume B8: x in (dom (f | [.a,b.])) /\ (dom (g | [.b,c.])) ; :: thesis: (f | [.a,b.]) . x = (g | [.b,c.]) . x
DX: (dom (f | [.a,b.])) /\ (dom (g | [.b,c.])) = (dom (f | [.a,b.])) /\ [.b,c.] by FUNCT_2:def 1
.= [.a,b.] /\ [.b,b.] by B5, FUNCT_2:def 1
.= {b} by XXREAL_1:418, B5, A1 ;
C1: x = b by TARSKI:def 1, DX, B8;
(f | [.a,b.]) . x = g . x by A3, FUNCT_1:49, C1, XXREAL_1:1, B5, A1;
hence (f | [.a,b.]) . x = (g | [.b,c.]) . x by FUNCT_1:49, B8; :: thesis: verum

end;

(h | [.a,c.]) . x = (f | [.a,b.]) . x by B6, FUNCT_4:15, PARTFUN1:def 4, TO, A2
.= f . x by FUNCT_1:49, B2, A5 ;
hence H1 . x = F1 . x by FUNCT_1:49, B2; :: thesis: verum

end;

suppose c <> b ; :: thesis: H1 . x = F1 . x

then c < b by A10, XXREAL_0:1;
then B4: {} = [.b,c.] by XXREAL_1:29
.= dom (g | [.b,c.]) by FUNCT_2:def 1 ;
(h | [.a,c.]) . x = (f | [.a,b.]) . x by B4, FUNCT_4:11, A2
.= f . x by FUNCT_1:49, B2, A5 ;
hence H1 . x = F1 . x by FUNCT_1:49, B2; :: thesis: verum

end;

end;

end;

hence h | [.a,c.] = f | [.a,c.] by FUNCT_2:12; :: thesis: verum

end;

hence ( ( b <= a implies h | [.a,c.] = g | [.a,c.] ) & ( c <= b implies h | [.a,c.] = f | [.a,c.] ) ) by A4; :: thesis: verum