let X be set ; :: thesis: for f, g, F, G being PartFunc of REAL,REAL st ( for x being set st x in X holds
G . x <> 0 ) & F is_integral_of f,X & G is_integral_of g,X holds
F / G is_integral_of ((f (#) G) - (F (#) g)) / (G (#) G),X
let f, g, F, G be PartFunc of REAL,REAL; :: thesis: ( ( for x being set st x in X holds
G . x <> 0 ) & F is_integral_of f,X & G is_integral_of g,X implies F / G is_integral_of ((f (#) G) - (F (#) g)) / (G (#) G),X )
assume that
A1: for x being set st x in X holds
G . x <> 0 and
A2: F is_integral_of f,X and
A3: G is_integral_of g,X ; :: thesis: F / G is_integral_of ((f (#) G) - (F (#) g)) / (G (#) G),X
A4: G is_differentiable_on X by A3, Lm1;
A5: X c= dom F by A2, Th11;
A6: G `| X = g | X by A3, Lm1;
then dom (g | X) = X by A4, FDIFF_1:def 7;
then (dom g) /\ X = X by RELAT_1:61;
then X c= dom g by XBOOLE_1:18;
then X c= (dom F) /\ (dom g) by A5, XBOOLE_1:19;
then A7: X c= dom (F (#) g) by VALUED_1:def 4;
A8: X c= dom G by A3, Th11;
A9: F is_differentiable_on X by A2, Lm1;
then A10: F / G is_differentiable_on X by A1, A4, Th8;
A11: F `| X = f | X by A2, Lm1;
then dom (f | X) = X by A9, FDIFF_1:def 7;
then (dom f) /\ X = X by RELAT_1:61;
then X c= dom f by XBOOLE_1:18;
then X c= (dom f) /\ (dom G) by A8, XBOOLE_1:19;
then X c= dom (f (#) G) by VALUED_1:def 4;
then X c= (dom (f (#) G)) /\ (dom (F (#) g)) by A7, XBOOLE_1:19;
then A12: X c= dom ((f (#) G) - (F (#) g)) by VALUED_1:12;

A13: now :: thesis: for x being Element of REAL st x in dom ((F / G) `| X) holds
((F / G) `| X) . x = ((((f (#) G) - (F (#) g)) / (G (#) G)) | X) . x

let x be Element of REAL ; :: thesis: ( x in dom ((F / G) `| X) implies ((F / G) `| X) . x = ((((f (#) G) - (F (#) g)) / (G (#) G)) | X) . x )
X = (dom G) /\ X by A3, Th11, XBOOLE_1:28;
then A14: X = dom (G | X) by RELAT_1:61;
assume x in dom ((F / G) `| X) ; :: thesis: ((F / G) `| X) . x = ((((f (#) G) - (F (#) g)) / (G (#) G)) | X) . x
then A15: x in X by A10, FDIFF_1:def 7;
then F | X is_differentiable_in x by A9;
then A16: F is_differentiable_in x by A15, Th4;
G | X is_differentiable_in x by A4, A15;
then A17: G is_differentiable_in x by A15, Th4;
G . x = (G | X) . x by A15, FUNCT_1:49;
then A18: (G . x) ^2 = ((G | X) (#) (G | X)) . x by VALUED_1:5;

now :: thesis: for y being set st y in dom (G | X) holds
not y in (G | X) " {0}

let y be set ; :: thesis: ( y in dom (G | X) implies not y in (G | X) " {0} )
assume A19: y in dom (G | X) ; :: thesis: not y in (G | X) " {0}
then y in (dom G) /\ X by RELAT_1:61;
then y in X by XBOOLE_0:def 4;
then A20: G . y <> 0 by A1;
(G | X) . y = G . y by A19, FUNCT_1:47;
then not (G | X) . y in {0} by A20, TARSKI:def 1;
hence not y in (G | X) " {0} by FUNCT_1:def 7; :: thesis: verum

end;

then not x in (G | X) " {0} by A15, A14;
then x in ((dom (G | X)) \ ((G | X) " {0})) /\ ((dom (G | X)) \ ((G | X) " {0})) by A15, A14, XBOOLE_0:def 5;
then x in (dom ((G | X) (#) (G | X))) \ (((G | X) (#) (G | X)) " {0}) by RFUNCT_1:2;
then x in (dom ((f (#) G) - (F (#) g))) /\ ((dom ((G | X) (#) (G | X))) \ (((G | X) (#) (G | X)) " {0})) by A12, A15, XBOOLE_0:def 4;
then A21: x in dom (((f (#) G) - (F (#) g)) / ((G | X) (#) (G | X))) by RFUNCT_1:def 1;
(G `| X) . x = diff (G,x) by A4, A15, FDIFF_1:def 7;
then g . x = diff (G,x) by A6, A15, FUNCT_1:49;
then A22: (F (#) g) . x = (F . x) * (diff (G,x)) by VALUED_1:5;
(F `| X) . x = diff (F,x) by A9, A15, FDIFF_1:def 7;
then f . x = diff (F,x) by A11, A15, FUNCT_1:49;
then (f (#) G) . x = (G . x) * (diff (F,x)) by VALUED_1:5;
then A23: ((f (#) G) - (F (#) g)) . x = ((diff (F,x)) * (G . x)) - ((diff (G,x)) * (F . x)) by A12, A15, A22, VALUED_1:13;
( ((F / G) `| X) . x = diff ((F / G),x) & G . x <> 0 ) by A1, A10, A15, FDIFF_1:def 7;
then ((F / G) `| X) . x = (((diff (F,x)) * (G . x)) - ((diff (G,x)) * (F . x))) / ((G . x) ^2) by A16, A17, FDIFF_2:14;
then ((F / G) `| X) . x = (((f (#) G) - (F (#) g)) / ((G | X) (#) (G | X))) . x by A21, A23, A18, RFUNCT_1:def 1;
then ((F / G) `| X) . x = (((f (#) G) - (F (#) g)) / ((G (#) G) | X)) . x by RFUNCT_1:45;
hence ((F / G) `| X) . x = ((((f (#) G) - (F (#) g)) / (G (#) G)) | X) . x by RFUNCT_1:48; :: thesis: verum

end;

now :: thesis: not (G | X) " {0} <> {}

assume (G | X) " {0} <> {} ; :: thesis: contradiction
then consider y being object such that
A24: y in (G | X) " {0} by XBOOLE_0:def 1;
A25: y in dom (G | X) by A24, FUNCT_1:def 7;
then A26: (G | X) . y = G . y by FUNCT_1:47;
y in (dom G) /\ X by A25, RELAT_1:61;
then y in X by XBOOLE_0:def 4;
then A27: G . y <> 0 by A1;
(G | X) . y in {0} by A24, FUNCT_1:def 7;
hence contradiction by A27, A26, TARSKI:def 1; :: thesis: verum

end;

then ((dom (G | X)) \ ((G | X) " {0})) /\ ((dom (G | X)) \ ((G | X) " {0})) = dom (G | X) ;
then (dom ((G | X) (#) (G | X))) \ (((G | X) (#) (G | X)) " {0}) = dom (G | X) by RFUNCT_1:2;
then (dom ((G | X) (#) (G | X))) \ (((G | X) (#) (G | X)) " {0}) = (dom G) /\ X by RELAT_1:61;
then A28: (dom ((G | X) (#) (G | X))) \ (((G | X) (#) (G | X)) " {0}) = X by A3, Th11, XBOOLE_1:28;
X = dom (((f (#) G) - (F (#) g)) | X) by A12, RELAT_1:62;
then (dom (((f (#) G) - (F (#) g)) | X)) /\ ((dom ((G | X) (#) (G | X))) \ (((G | X) (#) (G | X)) " {0})) = X by A28;
then dom ((((f (#) G) - (F (#) g)) | X) / ((G | X) (#) (G | X))) = X by RFUNCT_1:def 1;
then dom ((((f (#) G) - (F (#) g)) | X) / ((G (#) G) | X)) = X by RFUNCT_1:45;
then dom ((((f (#) G) - (F (#) g)) / (G (#) G)) | X) = X by RFUNCT_1:48;
then dom ((F / G) `| X) = dom ((((f (#) G) - (F (#) g)) / (G (#) G)) | X) by A10, FDIFF_1:def 7;
then (F / G) `| X = (((f (#) G) - (F (#) g)) / (G (#) G)) | X by A13, PARTFUN1:5;
hence F / G is_integral_of ((f (#) G) - (F (#) g)) / (G (#) G),X by A10, Lm1; :: thesis: verum