let p, g be Real; :: thesis:
assume A1: p < g ; :: thesis:
let f1, f2 be PartFunc of REAL ,REAL ; :: thesis:
assume that
A0: ( [.p,g.] c= dom f1 & [.p,g.] c= dom f2 ) and
A2: ( f1 | [.p,g.] is continuous & f1 is_differentiable_on ].p,g.[ ) and
A3: ( f2 | [.p,g.] is continuous & f2 is_differentiable_on ].p,g.[ ) ; :: thesis:
A4: ].p,g.[ c= [.p,g.] by XXREAL_1:25;

now

per cases ;

suppose A5: f2 . p = f2 . g ; :: thesis:

then consider x0 being Real such that
A6: ( x0 in ].p,g.[ & diff f2,x0 = 0 ) by A1, A3, Th1, A0;
take x0 = x0; :: thesis:
thus ( x0 in ].p,g.[ & ((f1 . g) - (f1 . p)) * (diff f2,x0) = ((f2 . g) - (f2 . p)) * (diff f1,x0) ) by A5, A6; :: thesis:

end;

suppose f2 . p <> f2 . g ; :: thesis:

then A7: (f2 . g) - (f2 . p) <> 0 ;
set s = ((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p));
reconsider f3 = [.p,g.] --> ((f1 . p) - ((f2 . p) * (((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))))) as PartFunc of [.p,g.],REAL by FUNCOP_1:57;
reconsider f3 = f3 as PartFunc of REAL ,REAL ;
reconsider Z = ].p,g.[ as open Subset of REAL ;
A8: [.p,g.] = dom f3 by FUNCOP_1:19;
then for x being Real st x in [.p,g.] /\ (dom f3) holds
f3 . x = (f1 . p) - ((f2 . p) * (((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p)))) by FUNCOP_1:13;
then A9: f3 | [.p,g.] is V8() by PARTFUN2:76;
then A10: f3 | [.p,g.] is continuous ;
A11: f3 | ].p,g.[ is V8() by A9, PARTFUN2:57, XXREAL_1:25;
A12: Z c= dom f3 by A4, FUNCOP_1:19;
then A13: ( f3 is_differentiable_on Z & ( for x being Real st x in Z holds
(f3 `| Z) . x = 0 ) ) by A11, FDIFF_1:30;
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;
X: dom ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2) = dom f2 by VALUED_1:def 5;
a: ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2) | [.p,g.] is continuous by A3, A0, FCONT_1:21;
b: [.p,g.] c= (dom f3) /\ (dom ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2)) by A8, X, A0, XBOOLE_1:19;
then U: (f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2)) | [.p,g.] is continuous by A10, a, FCONT_1:19;
[.p,g.] c= dom (f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2)) by b, VALUED_1:def 1;
then I: [.p,g.] c= (dom (f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2))) /\ (dom f1) by A0, XBOOLE_1:19;
then A14: ((f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2)) - f1) | [.p,g.] is continuous by A2, U, FCONT_1:19;
H: [.p,g.] c= dom ((f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2)) - f1) by I, VALUED_1:12;
A15: dom ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2) = dom f2 by VALUED_1:def 5;
A17: Z c= dom ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2) by A0, A4, A15, XBOOLE_1:1;
then A18: ( (((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2 is_differentiable_on Z & ( for x being Real st x in Z holds
(((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2) `| Z) . x = (((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) * (diff f2,x) ) ) by A3, FDIFF_1:28;
Z c= (dom f3) /\ (dom ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2)) by A12, A17, XBOOLE_1:19;
then A19: Z c= dom (f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2)) by VALUED_1:def 1;
then A20: ( f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2) is_differentiable_on Z & ( for x being Real st x in Z holds
((f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2)) `| Z) . x = (diff f3,x) + (diff ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2),x) ) ) by A13, A18, FDIFF_1:26;
Z c= dom f1 by A0, A4, XBOOLE_1:1;
then Z c= (dom (f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2))) /\ (dom f1) by A19, XBOOLE_1:19;
then A22: Z c= dom ((f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2)) - f1) by VALUED_1:12;
then A23: ( (f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2)) - f1 is_differentiable_on Z & ( for x being Real st x in Z holds
(((f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2)) - f1) `| Z) . x = (diff (f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2)),x) - (diff f1,x) ) ) by A2, A20, FDIFF_1:27;
A24: 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 A8, A15, A0, XBOOLE_0:def 4;
then A25: 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 A0, A24, XBOOLE_0:def 4;
then p in dom ((f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2)) - f1) by VALUED_1:12;
then A26: ((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 A25, VALUED_1:def 1
.= ((f3 . p) + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) * (f2 . p))) - (f1 . p) by A15, A0, A24, 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 A24, FUNCOP_1:13
.= 0 ;
A27: 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 A8, A15, A0, XBOOLE_0:def 4;
then A28: 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 A0, A27, XBOOLE_0:def 4;
then g in dom ((f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2)) - f1) by VALUED_1:12;
then ((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 A28, VALUED_1:def 1
.= ((f3 . g) + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) * (f2 . g))) - (f1 . g) by A15, A0, A27, 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 A27, FUNCOP_1:13
.= (- (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 A7, XCMPLX_1:88
.= ((f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2)) - f1) . p by A26 ;
then consider x0 being Real such that
A29: ( x0 in ].p,g.[ & diff ((f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2)) - f1),x0 = 0 ) by A1, A14, A23, Th1, H;
take x0 = x0; :: thesis:
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 A23, A29, FDIFF_1:def 8
.= (diff (f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2)),x0) - (diff f1,x0) by A2, A20, A22, A29, FDIFF_1:27
.= (((f3 + ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2)) `| Z) . x0) - (diff f1,x0) by A20, A29, FDIFF_1:def 8
.= ((diff f3,x0) + (diff ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2),x0)) - (diff f1,x0) by A13, A18, A19, A29, FDIFF_1:26
.= (((f3 `| Z) . x0) + (diff ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2),x0)) - (diff f1,x0) by A13, A29, FDIFF_1:def 8
.= (0 + (diff ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2),x0)) - (diff f1,x0) by A11, A12, A29, FDIFF_1:30
.= ((((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) (#) f2) `| Z) . x0) - (diff f1,x0) by A18, A29, FDIFF_1:def 8
.= ((((f1 . g) - (f1 . p)) / ((f2 . g) - (f2 . p))) * (diff f2,x0)) - (diff f1,x0) by A3, A17, A29, FDIFF_1:28 ;
then (((diff f2,x0) * ((f1 . g) - (f1 . p))) / ((f2 . g) - (f2 . p))) * ((f2 . g) - (f2 . p)) = (diff f1,x0) * ((f2 . g) - (f2 . p)) by A29, XCMPLX_1:15;
hence ( x0 in ].p,g.[ & ((f1 . g) - (f1 . p)) * (diff f2,x0) = ((f2 . g) - (f2 . p)) * (diff f1,x0) ) by A7, A29, XCMPLX_1:88; :: thesis:

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) ) ; :: thesis: