let X be set ; 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; ( ( 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
; 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 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) . xlet x be
Element of
REAL ;
( 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)
;
((F / G) `| X) . x = ((((f (#) G) - (F (#) g)) / (G (#) G)) | X) . xthen 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;
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;
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; verum