let p, g be Real; ( p < g implies for f1, f2 being PartFunc of REAL,REAL st [.p,g.] c= dom f1 & [.p,g.] c= dom f2 & f1 | [.p,g.] is continuous & f1 is_differentiable_on ].p,g.[ & f2 | [.p,g.] is continuous & f2 is_differentiable_on ].p,g.[ holds
ex x0 being Real st
( x0 in ].p,g.[ & ((f1 . g) - (f1 . p)) * (diff (f2,x0)) = ((f2 . g) - (f2 . p)) * (diff (f1,x0)) ) )
assume A1:
p < g
; for f1, f2 being PartFunc of REAL,REAL st [.p,g.] c= dom f1 & [.p,g.] c= dom f2 & f1 | [.p,g.] is continuous & f1 is_differentiable_on ].p,g.[ & f2 | [.p,g.] is continuous & f2 is_differentiable_on ].p,g.[ holds
ex x0 being Real st
( x0 in ].p,g.[ & ((f1 . g) - (f1 . p)) * (diff (f2,x0)) = ((f2 . g) - (f2 . p)) * (diff (f1,x0)) )
let f1, f2 be PartFunc of REAL,REAL; ( [.p,g.] c= dom f1 & [.p,g.] c= dom f2 & f1 | [.p,g.] is continuous & f1 is_differentiable_on ].p,g.[ & f2 | [.p,g.] is continuous & f2 is_differentiable_on ].p,g.[ implies ex x0 being Real st
( x0 in ].p,g.[ & ((f1 . g) - (f1 . p)) * (diff (f2,x0)) = ((f2 . g) - (f2 . p)) * (diff (f1,x0)) ) )
assume that
A2:
[.p,g.] c= dom f1
and
A3:
[.p,g.] c= dom f2
and
A4:
f1 | [.p,g.] is continuous
and
A5:
f1 is_differentiable_on ].p,g.[
and
A6:
f2 | [.p,g.] is continuous
and
A7:
f2 is_differentiable_on ].p,g.[
; ex x0 being Real st
( x0 in ].p,g.[ & ((f1 . g) - (f1 . p)) * (diff (f2,x0)) = ((f2 . g) - (f2 . p)) * (diff (f1,x0)) )
A8:
].p,g.[ c= [.p,g.]
by XXREAL_1:25;
now ex x0 being Real st
( x0 in ].p,g.[ & ((f1 . g) - (f1 . p)) * (diff (f2,x0)) = ((f2 . g) - (f2 . p)) * (diff (f1,x0)) )per cases
( f2 . p = f2 . g or f2 . p <> f2 . g )
;
suppose A9:
f2 . p = f2 . g
;
ex x0 being Real st
( x0 in ].p,g.[ & ((f1 . g) - (f1 . p)) * (diff (f2,x0)) = ((f2 . g) - (f2 . p)) * (diff (f1,x0)) )then consider x0 being
Real such that A10:
(
x0 in ].p,g.[ &
diff (
f2,
x0)
= 0 )
by A1, A3, A6, A7, Th1;
take x0 =
x0;
( x0 in ].p,g.[ & ((f1 . g) - (f1 . p)) * (diff (f2,x0)) = ((f2 . g) - (f2 . p)) * (diff (f1,x0)) )thus
(
x0 in ].p,g.[ &
((f1 . g) - (f1 . p)) * (diff (f2,x0)) = ((f2 . g) - (f2 . p)) * (diff (f1,x0)) )
by A9, A10;
verum end; suppose
f2 . p <> f2 . g
;
ex x0 being Real st
( x0 in ].p,g.[ & ((f1 . g) - (f1 . p)) * (diff (f2,x0)) = ((f2 . g) - (f2 . p)) * (diff (f1,x0)) )then A11:
(f2 . g) - (f2 . p) <> 0
;
reconsider Z =
].p,g.[ as
open Subset of
REAL ;
set s =
((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p));
reconsider fp =
(f1 . p) - ((f2 . p) * (((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p)))) as
Element of
REAL by XREAL_0:def 1;
reconsider f3 =
[.p,g.] --> fp as
PartFunc of
[.p,g.],
REAL by FUNCOP_1:45;
reconsider f3 =
f3 as
PartFunc of
REAL,
REAL ;
set f4 =
(((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2;
set f5 =
f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2);
set f =
(f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2)) - f1;
A12:
Z c= dom f3
by A8, FUNCOP_1:13;
A13:
dom ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2) = dom f2
by VALUED_1:def 5;
then A14:
Z c= dom ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2)
by A3, A8;
then
Z c= (dom f3) /\ (dom ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2))
by A12, XBOOLE_1:19;
then A15:
Z c= dom (f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2))
by VALUED_1:def 1;
reconsider f1pf2p =
(f1 . p) - ((f2 . p) * (((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p)))) as
Element of
REAL by XREAL_0:def 1;
A16:
[.p,g.] = dom f3
by FUNCOP_1:13;
then
for
x being
Element of
REAL st
x in [.p,g.] /\ (dom f3) holds
f3 . x = f1pf2p
by FUNCOP_1:7;
then A17:
f3 | [.p,g.] is
constant
by PARTFUN2:57;
then A18:
f3 | ].p,g.[ is
constant
by PARTFUN2:38, XXREAL_1:25;
then A19:
f3 is_differentiable_on Z
by A12, FDIFF_1:22;
A20:
p in [.p,g.]
by A1, XXREAL_1:1;
then
p in (dom f3) /\ (dom ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2))
by A3, A16, A13, XBOOLE_0:def 4;
then A21:
p in dom (f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2))
by VALUED_1:def 1;
then
p in (dom (f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2))) /\ (dom f1)
by A2, A20, XBOOLE_0:def 4;
then
p in dom ((f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2)) - f1)
by VALUED_1:12;
then A22:
((f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2)) - f1) . p =
((f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2)) . p) - (f1 . p)
by VALUED_1:13
.=
((f3 . p) + (((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2) . p)) - (f1 . p)
by A21, VALUED_1:def 1
.=
((f3 . p) + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) * (f2 . p))) - (f1 . p)
by A3, A13, A20, VALUED_1:def 5
.=
(((f1 . p) - ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) * (f2 . p))) + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) * (f2 . p))) - (f1 . p)
by A20, FUNCOP_1:7
.=
0
;
A23:
g in [.p,g.]
by A1, XXREAL_1:1;
then
g in (dom f3) /\ (dom ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2))
by A3, A16, A13, XBOOLE_0:def 4;
then A24:
g in dom (f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2))
by VALUED_1:def 1;
then
g in (dom (f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2))) /\ (dom f1)
by A2, A23, XBOOLE_0:def 4;
then
g in dom ((f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2)) - f1)
by VALUED_1:12;
then A25:
((f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2)) - f1) . g =
((f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2)) . g) - (f1 . g)
by VALUED_1:13
.=
((f3 . g) + (((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2) . g)) - (f1 . g)
by A24, VALUED_1:def 1
.=
((f3 . g) + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) * (f2 . g))) - (f1 . g)
by A3, A13, A23, VALUED_1:def 5
.=
(((f1 . p) - ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) * (f2 . p))) + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) * (f2 . g))) - (f1 . g)
by A23, FUNCOP_1:7
.=
(- (f1 . g)) + ((f1 . p) - (((- ((f1 . g) - (f1 . p))) / ((f2 . g) - (f2 . p))) * ((f2 . g) - (f2 . p))))
.=
(- (f1 . g)) + ((f1 . p) - ((f1 . p) - (f1 . g)))
by A11, XCMPLX_1:87
.=
((f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2)) - f1) . p
by A22
;
Z c= dom f1
by A2, A8;
then
Z c= (dom (f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2))) /\ (dom f1)
by A15, XBOOLE_1:19;
then A26:
Z c= dom ((f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2)) - f1)
by VALUED_1:12;
dom ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2) = dom f2
by VALUED_1:def 5;
then A27:
[.p,g.] c= (dom f3) /\ (dom ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2))
by A3, A16, XBOOLE_1:19;
then
[.p,g.] c= dom (f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2))
by VALUED_1:def 1;
then A28:
[.p,g.] c= (dom (f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2))) /\ (dom f1)
by A2, XBOOLE_1:19;
((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2) | [.p,g.] is
continuous
by A3, A6, FCONT_1:20;
then
(f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2)) | [.p,g.] is
continuous
by A17, A27, FCONT_1:18;
then A29:
((f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2)) - f1) | [.p,g.] is
continuous
by A4, A28, FCONT_1:18;
A30:
(((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2 is_differentiable_on Z
by A7, A14, FDIFF_1:20;
then A31:
f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2) is_differentiable_on Z
by A19, A15, FDIFF_1:18;
[.p,g.] c= dom ((f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2)) - f1)
by A28, VALUED_1:12;
then consider x0 being
Real such that A32:
x0 in ].p,g.[
and A33:
diff (
((f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2)) - f1),
x0)
= 0
by A1, A5, A29, A31, A26, A25, Th1, FDIFF_1:19;
take x0 =
x0;
( x0 in ].p,g.[ & ((f1 . g) - (f1 . p)) * (diff (f2,x0)) = ((f2 . g) - (f2 . p)) * (diff (f1,x0)) )
(f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2)) - f1 is_differentiable_on Z
by A5, A31, A26, FDIFF_1:19;
then diff (
((f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2)) - f1),
x0) =
(((f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2)) - f1) `| Z) . x0
by A32, FDIFF_1:def 7
.=
(diff ((f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2)),x0)) - (diff (f1,x0))
by A5, A31, A26, A32, FDIFF_1:19
.=
(((f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2)) `| Z) . x0) - (diff (f1,x0))
by A31, A32, FDIFF_1:def 7
.=
((diff (f3,x0)) + (diff (((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2),x0))) - (diff (f1,x0))
by A19, A30, A15, A32, FDIFF_1:18
.=
(((f3 `| Z) . x0) + (diff (((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2),x0))) - (diff (f1,x0))
by A19, A32, FDIFF_1:def 7
.=
(0 + (diff (((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2),x0))) - (diff (f1,x0))
by A18, A12, A32, FDIFF_1:22
.=
((((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2) `| Z) . x0) - (diff (f1,x0))
by A30, A32, FDIFF_1:def 7
.=
((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) * (diff (f2,x0))) - (diff (f1,x0))
by A7, A14, A32, FDIFF_1:20
;
then
(((diff (f2,x0)) * ((f1 . g) - (f1 . p))) / ((f2 . g) - (f2 . p))) * ((f2 . g) - (f2 . p)) = (diff (f1,x0)) * ((f2 . g) - (f2 . p))
by A33, XCMPLX_1:15;
hence
(
x0 in ].p,g.[ &
((f1 . g) - (f1 . p)) * (diff (f2,x0)) = ((f2 . g) - (f2 . p)) * (diff (f1,x0)) )
by A11, A32, XCMPLX_1:87;
verum end;
hence
ex x0 being Real st
( x0 in ].p,g.[ & ((f1 . g) - (f1 . p)) * (diff (f2,x0)) = ((f2 . g) - (f2 . p)) * (diff (f1,x0)) )
; verum