let A be open Subset of REAL ; :: thesis: for f1, f2 being PartFunc of REAL ,REAL st f1 is_differentiable_on A & f2 is_differentiable_on A & ( for x0 being Real st x0 in A holds
f2 . x0 <> 0 ) holds
( f1 / f2 is_differentiable_on A & (f1 / f2) `| A = (((f1 `| A) (#) f2) - ((f2 `| A) (#) f1)) / (f2 (#) f2) )
let f1, f2 be PartFunc of REAL ,REAL ; :: thesis: ( f1 is_differentiable_on A & f2 is_differentiable_on A & ( for x0 being Real st x0 in A holds
f2 . x0 <> 0 ) implies ( f1 / f2 is_differentiable_on A & (f1 / f2) `| A = (((f1 `| A) (#) f2) - ((f2 `| A) (#) f1)) / (f2 (#) f2) ) )
assume A1: ( f1 is_differentiable_on A & f2 is_differentiable_on A & ( for x0 being Real st x0 in A holds
f2 . x0 <> 0 ) ) ; :: thesis: ( f1 / f2 is_differentiable_on A & (f1 / f2) `| A = (((f1 `| A) (#) f2) - ((f2 `| A) (#) f1)) / (f2 (#) f2) )
then A2: A c= dom f1 by FDIFF_1:16;
A3: A c= dom f2 by A1, FDIFF_1:16;
A4: A c= (dom f2) \ (f2 " {0 })

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in (dom f2) \ (f2 " {0 }) )
assume A5: x in A ; :: thesis: x in (dom f2) \ (f2 " {0 })
then reconsider x' = x as Real ;
assume not x in (dom f2) \ (f2 " {0 }) ; :: thesis: contradiction
then ( not x in dom f2 or x in f2 " {0 } ) by XBOOLE_0:def 5;
then ( x' in dom f2 & f2 . x' in {0 } ) by A3, A5, FUNCT_1:def 13;
then f2 . x' = 0 by TARSKI:def 1;
hence contradiction by A1, A5; :: thesis: verum

end;

then A c= (dom f1) /\ ((dom f2) \ (f2 " {0 })) by A2, XBOOLE_1:19;
then A6: A c= dom (f1 / f2) by RFUNCT_1:def 4;

A7: now

let x0 be Real; :: thesis: ( x0 in A implies ( f2 . x0 <> 0 & f1 is_differentiable_in x0 & f2 is_differentiable_in x0 & f1 / f2 is_differentiable_in x0 ) )
assume A8: x0 in A ; :: thesis: ( f2 . x0 <> 0 & f1 is_differentiable_in x0 & f2 is_differentiable_in x0 & f1 / f2 is_differentiable_in x0 )
hence A9: f2 . x0 <> 0 by A1; :: thesis: ( f1 is_differentiable_in x0 & f2 is_differentiable_in x0 & f1 / f2 is_differentiable_in x0 )
thus A10: f1 is_differentiable_in x0 by A1, A8, FDIFF_1:16; :: thesis: ( f2 is_differentiable_in x0 & f1 / f2 is_differentiable_in x0 )
thus f2 is_differentiable_in x0 by A1, A8, FDIFF_1:16; :: thesis: f1 / f2 is_differentiable_in x0
hence f1 / f2 is_differentiable_in x0 by A9, A10, Th14; :: thesis: verum

end;

then for x0 being Real st x0 in A holds
f1 / f2 is_differentiable_in x0 ;
hence A11: f1 / f2 is_differentiable_on A by A6, FDIFF_1:16; :: thesis: (f1 / f2) `| A = (((f1 `| A) (#) f2) - ((f2 `| A) (#) f1)) / (f2 (#) f2)
then A12: A = dom ((f1 / f2) `| A) by FDIFF_1:def 8;
A13: dom ((((f1 `| A) (#) f2) - ((f2 `| A) (#) f1)) / (f2 (#) f2)) = (dom (((f1 `| A) (#) f2) - ((f2 `| A) (#) f1))) /\ ((dom (f2 (#) f2)) \ ((f2 (#) f2) " {0 })) by RFUNCT_1:def 4
.= ((dom ((f1 `| A) (#) f2)) /\ (dom ((f2 `| A) (#) f1))) /\ ((dom (f2 (#) f2)) \ ((f2 (#) f2) " {0 })) by VALUED_1:12
.= (((dom (f1 `| A)) /\ (dom f2)) /\ (dom ((f2 `| A) (#) f1))) /\ ((dom (f2 (#) f2)) \ ((f2 (#) f2) " {0 })) by VALUED_1:def 4
.= ((A /\ (dom f2)) /\ (dom ((f2 `| A) (#) f1))) /\ ((dom (f2 (#) f2)) \ ((f2 (#) f2) " {0 })) by A1, FDIFF_1:def 8
.= (A /\ (dom ((f2 `| A) (#) f1))) /\ ((dom (f2 (#) f2)) \ ((f2 (#) f2) " {0 })) by A3, XBOOLE_1:28
.= (A /\ ((dom (f2 `| A)) /\ (dom f1))) /\ ((dom (f2 (#) f2)) \ ((f2 (#) f2) " {0 })) by VALUED_1:def 4
.= (A /\ (A /\ (dom f1))) /\ ((dom (f2 (#) f2)) \ ((f2 (#) f2) " {0 })) by A1, FDIFF_1:def 8
.= (A /\ A) /\ ((dom (f2 (#) f2)) \ ((f2 (#) f2) " {0 })) by A2, XBOOLE_1:28
.= A /\ (((dom f2) /\ (dom f2)) \ ((f2 (#) f2) " {0 })) by VALUED_1:def 4
.= A /\ ((dom f2) \ (f2 " {0 })) by Lm3
.= dom ((f1 / f2) `| A) by A4, A12, XBOOLE_1:28 ;

now

let x0 be Real; :: thesis: ( x0 in dom ((f1 / f2) `| A) implies ((f1 / f2) `| A) . x0 = ((((f1 `| A) (#) f2) - ((f2 `| A) (#) f1)) / (f2 (#) f2)) . x0 )
assume A14: x0 in dom ((f1 / f2) `| A) ; :: thesis: ((f1 / f2) `| A) . x0 = ((((f1 `| A) (#) f2) - ((f2 `| A) (#) f1)) / (f2 (#) f2)) . x0
then A15: ( f2 . x0 <> 0 & f1 is_differentiable_in x0 & f2 is_differentiable_in x0 ) by A7, A12;
dom (f1 `| A) = A by A1, FDIFF_1:def 8;
then x0 in (dom (f1 `| A)) /\ (dom f2) by A3, A12, A14, XBOOLE_0:def 4;
then A16: x0 in dom ((f1 `| A) (#) f2) by VALUED_1:def 4;
dom (f2 `| A) = A by A1, FDIFF_1:def 8;
then x0 in (dom (f2 `| A)) /\ (dom f1) by A2, A12, A14, XBOOLE_0:def 4;
then x0 in dom ((f2 `| A) (#) f1) by VALUED_1:def 4;
then x0 in (dom ((f1 `| A) (#) f2)) /\ (dom ((f2 `| A) (#) f1)) by A16, XBOOLE_0:def 4;
then A17: x0 in dom (((f1 `| A) (#) f2) - ((f2 `| A) (#) f1)) by VALUED_1:12;
x0 in (dom f2) /\ (dom f2) by A3, A12, A14;
then A18: x0 in dom (f2 (#) f2) by VALUED_1:def 4;
(f2 . x0) * (f2 . x0) <> 0 by A15;
then (f2 (#) f2) . x0 <> 0 by VALUED_1:5;
then not (f2 (#) f2) . x0 in {0 } by TARSKI:def 1;
then not x0 in (f2 (#) f2) " {0 } by FUNCT_1:def 13;
then x0 in (dom (f2 (#) f2)) \ ((f2 (#) f2) " {0 }) by A18, XBOOLE_0:def 5;
then x0 in (dom (((f1 `| A) (#) f2) - ((f2 `| A) (#) f1))) /\ ((dom (f2 (#) f2)) \ ((f2 (#) f2) " {0 })) by A17, XBOOLE_0:def 4;
then A19: x0 in dom ((((f1 `| A) (#) f2) - ((f2 `| A) (#) f1)) / (f2 (#) f2)) by RFUNCT_1:def 4;
thus ((f1 / f2) `| A) . x0 = diff (f1 / f2),x0 by A11, A12, A14, FDIFF_1:def 8
.= (((diff f1,x0) * (f2 . x0)) - ((diff f2,x0) * (f1 . x0))) / ((f2 . x0) ^2 ) by A15, Th14
.= ((((f1 `| A) . x0) * (f2 . x0)) - ((diff f2,x0) * (f1 . x0))) / ((f2 . x0) ^2 ) by A1, A12, A14, FDIFF_1:def 8
.= ((((f1 `| A) . x0) * (f2 . x0)) - (((f2 `| A) . x0) * (f1 . x0))) / ((f2 . x0) ^2 ) by A1, A12, A14, FDIFF_1:def 8
.= ((((f1 `| A) (#) f2) . x0) - (((f2 `| A) . x0) * (f1 . x0))) / ((f2 . x0) ^2 ) by VALUED_1:5
.= ((((f1 `| A) (#) f2) . x0) - (((f2 `| A) (#) f1) . x0)) / ((f2 . x0) ^2 ) by VALUED_1:5
.= ((((f1 `| A) (#) f2) - ((f2 `| A) (#) f1)) . x0) / ((f2 . x0) * (f2 . x0)) by A17, VALUED_1:13
.= ((((f1 `| A) (#) f2) - ((f2 `| A) (#) f1)) . x0) / ((f2 (#) f2) . x0) by VALUED_1:5
.= ((((f1 `| A) (#) f2) - ((f2 `| A) (#) f1)) . x0) * (((f2 (#) f2) . x0) " ) by XCMPLX_0:def 9
.= ((((f1 `| A) (#) f2) - ((f2 `| A) (#) f1)) / (f2 (#) f2)) . x0 by A19, RFUNCT_1:def 4 ; :: thesis: verum

end;

hence (f1 / f2) `| A = (((f1 `| A) (#) f2) - ((f2 `| A) (#) f1)) / (f2 (#) f2) by A13, PARTFUN1:34; :: thesis: verum