let f, g, F, G be PartFunc of REAL,REAL; :: thesis: for I being non empty Interval st F is_antiderivative_of f,I & G is_antiderivative_of g,I & ( for x being set st x in I holds
G . x <> 0 ) holds
F / G is_antiderivative_of ((f (#) G) - (F (#) g)) / (G (#) G),I
let I be non empty Interval; :: thesis: ( F is_antiderivative_of f,I & G is_antiderivative_of g,I & ( for x being set st x in I holds
G . x <> 0 ) implies F / G is_antiderivative_of ((f (#) G) - (F (#) g)) / (G (#) G),I )
assume that
A1: F is_antiderivative_of f,I and
A2: G is_antiderivative_of g,I and
A3: for x being set st x in I holds
G . x <> 0 ; :: thesis: F / G is_antiderivative_of ((f (#) G) - (F (#) g)) / (G (#) G),I
A4: ( I c= dom F & I c= dom G ) by A1, A2, FDIFF_12:def 1;
A5: dom (F / G) = (dom F) /\ ((dom G) \ (G " {0})) by RFUNCT_1:def 1;

now :: thesis: for x being set st x in I holds
x in dom (F / G)

let x be set ; :: thesis: ( x in I implies x in dom (F / G) )
assume A6: x in I ; :: thesis: x in dom (F / G)
then G . x <> 0 by A3;
then not G . x in {0} by TARSKI:def 1;
then not x in G " {0} by FUNCT_1:def 7;
then x in (dom G) \ (G " {0}) by A4, A6, XBOOLE_0:def 5;
hence x in dom (F / G) by A4, A5, A6, XBOOLE_0:def 4; :: thesis: verum

end;

then A7: I c= dom (F / G) ;
then A8: (F / G) `\ I = (((F `\ I) (#) G) - ((G `\ I) (#) F)) / (G ^2) by A1, A2, FDIFF_12:25;
( (F `\ I) (#) G = (f (#) G) | I & (G `\ I) (#) F = (g (#) F) | I ) by A1, A2, RFUNCT_1:45;
then ((F `\ I) (#) G) - ((G `\ I) (#) F) = ((f (#) G) - (g (#) F)) | I by RFUNCT_1:47;
hence F / G is_antiderivative_of ((f (#) G) - (F (#) g)) / (G (#) G),I by A7, A8, A1, A2, FDIFF_12:25, RFUNCT_1:48; :: thesis: verum