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 that
A1: f1 is_differentiable_on A and
A2: f2 is_differentiable_on A and
A3: 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) )
A4: A c= dom f1 by A1, FDIFF_1:16;
A5: A c= dom f2 by A2, FDIFF_1:16;
A6: 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 A7: x in A ; :: thesis: x in (dom f2) \ (f2 " {0 })
then reconsider x9 = 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 f2 . x9 in {0 } by A5, A7, FUNCT_1:def 13;
then f2 . x9 = 0 by TARSKI:def 1;
hence contradiction by A3, A7; :: thesis: verum

end;

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

A9: 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 A10: x0 in A ; :: thesis: ( f2 . x0 <> 0 & f1 is_differentiable_in x0 & f2 is_differentiable_in x0 & f1 / f2 is_differentiable_in x0 )
hence A11: f2 . x0 <> 0 by A3; :: thesis: ( f1 is_differentiable_in x0 & f2 is_differentiable_in x0 & f1 / f2 is_differentiable_in x0 )
thus A12: f1 is_differentiable_in x0 by A1, A10, FDIFF_1:16; :: thesis: ( f2 is_differentiable_in x0 & f1 / f2 is_differentiable_in x0 )
thus f2 is_differentiable_in x0 by A2, A10, FDIFF_1:16; :: thesis: f1 / f2 is_differentiable_in x0
hence f1 / f2 is_differentiable_in x0 by A11, A12, Th14; :: thesis: verum

end;

then for x0 being Real st x0 in A holds
f1 / f2 is_differentiable_in x0 ;
hence A13: f1 / f2 is_differentiable_on A by A8, FDIFF_1:16; :: thesis: (f1 / f2) `| A = (((f1 `| A) (#) f2) - ((f2 `| A) (#) f1)) / (f2 (#) f2)
then A14: A = dom ((f1 / f2) `| A) by FDIFF_1:def 8;

A15: 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 A16: x0 in dom ((f1 / f2) `| A) ; :: thesis: ((f1 / f2) `| A) . x0 = ((((f1 `| A) (#) f2) - ((f2 `| A) (#) f1)) / (f2 (#) f2)) . x0
then A17: f1 is_differentiable_in x0 by A9, A14;
dom (f2 `| A) = A by A2, FDIFF_1:def 8;
then x0 in (dom (f2 `| A)) /\ (dom f1) by A4, A14, A16, XBOOLE_0:def 4;
then A18: x0 in dom ((f2 `| A) (#) f1) by VALUED_1:def 4;
dom (f1 `| A) = A by A1, FDIFF_1:def 8;
then x0 in (dom (f1 `| A)) /\ (dom f2) by A5, A14, A16, XBOOLE_0:def 4;
then x0 in dom ((f1 `| A) (#) f2) by VALUED_1:def 4;
then x0 in (dom ((f1 `| A) (#) f2)) /\ (dom ((f2 `| A) (#) f1)) by A18, XBOOLE_0:def 4;
then A19: x0 in dom (((f1 `| A) (#) f2) - ((f2 `| A) (#) f1)) by VALUED_1:12;
A20: f2 . x0 <> 0 by A9, A14, A16;
then (f2 . x0) * (f2 . x0) <> 0 ;
then (f2 (#) f2) . x0 <> 0 by VALUED_1:5;
then not (f2 (#) f2) . x0 in {0 } by TARSKI:def 1;
then A21: not x0 in (f2 (#) f2) " {0 } by FUNCT_1:def 13;
x0 in (dom f2) /\ (dom f2) by A5, A14, A16;
then x0 in dom (f2 (#) f2) by VALUED_1:def 4;
then x0 in (dom (f2 (#) f2)) \ ((f2 (#) f2) " {0 }) by A21, XBOOLE_0:def 5;
then x0 in (dom (((f1 `| A) (#) f2) - ((f2 `| A) (#) f1))) /\ ((dom (f2 (#) f2)) \ ((f2 (#) f2) " {0 })) by A19, XBOOLE_0:def 4;
then A22: x0 in dom ((((f1 `| A) (#) f2) - ((f2 `| A) (#) f1)) / (f2 (#) f2)) by RFUNCT_1:def 4;
A23: f2 is_differentiable_in x0 by A9, A14, A16;
thus ((f1 / f2) `| A) . x0 = diff (f1 / f2),x0 by A13, A14, A16, FDIFF_1:def 8
.= (((diff f1,x0) * (f2 . x0)) - ((diff f2,x0) * (f1 . x0))) / ((f2 . x0) ^2 ) by A20, A17, A23, Th14
.= ((((f1 `| A) . x0) * (f2 . x0)) - ((diff f2,x0) * (f1 . x0))) / ((f2 . x0) ^2 ) by A1, A14, A16, FDIFF_1:def 8
.= ((((f1 `| A) . x0) * (f2 . x0)) - (((f2 `| A) . x0) * (f1 . x0))) / ((f2 . x0) ^2 ) by A2, A14, A16, 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 A19, 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 A22, RFUNCT_1:def 4 ; :: thesis: verum

end;

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 A5, 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 A2, FDIFF_1:def 8
.= (A /\ A) /\ ((dom (f2 (#) f2)) \ ((f2 (#) f2) " {0 })) by A4, 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 A6, A14, XBOOLE_1:28 ;
hence (f1 / f2) `| A = (((f1 `| A) (#) f2) - ((f2 `| A) (#) f1)) / (f2 (#) f2) by A15, PARTFUN1:34; :: thesis: verum