let S, T be RealNormSpace; for x0 being Real
for g being PartFunc of REAL, the carrier of S st g is_differentiable_in x0 holds
for f being PartFunc of the carrier of S, the carrier of T st f is_differentiable_in g /. x0 holds
( f * g is_differentiable_in x0 & diff ((f * g),x0) = (diff (f,(g /. x0))) . (diff (g,x0)) )
let x0 be Real; for g being PartFunc of REAL, the carrier of S st g is_differentiable_in x0 holds
for f being PartFunc of the carrier of S, the carrier of T st f is_differentiable_in g /. x0 holds
( f * g is_differentiable_in x0 & diff ((f * g),x0) = (diff (f,(g /. x0))) . (diff (g,x0)) )
let g be PartFunc of REAL, the carrier of S; ( g is_differentiable_in x0 implies for f being PartFunc of the carrier of S, the carrier of T st f is_differentiable_in g /. x0 holds
( f * g is_differentiable_in x0 & diff ((f * g),x0) = (diff (f,(g /. x0))) . (diff (g,x0)) ) )
assume A1:
g is_differentiable_in x0
; for f being PartFunc of the carrier of S, the carrier of T st f is_differentiable_in g /. x0 holds
( f * g is_differentiable_in x0 & diff ((f * g),x0) = (diff (f,(g /. x0))) . (diff (g,x0)) )
consider N1 being Neighbourhood of x0 such that
A2:
N1 c= dom g
and
A3:
ex L1 being LinearFunc of S ex R1 being RestFunc of S st
( diff (g,x0) = L1 /. 1 & ( for x being Real st x in N1 holds
(g /. x) - (g /. x0) = (L1 /. (x - x0)) + (R1 /. (x - x0)) ) )
by A1, NDIFF_3:def 4;
let f be PartFunc of the carrier of S, the carrier of T; ( f is_differentiable_in g /. x0 implies ( f * g is_differentiable_in x0 & diff ((f * g),x0) = (diff (f,(g /. x0))) . (diff (g,x0)) ) )
assume
f is_differentiable_in g /. x0
; ( f * g is_differentiable_in x0 & diff ((f * g),x0) = (diff (f,(g /. x0))) . (diff (g,x0)) )
then consider N2 being Neighbourhood of g /. x0 such that
A4:
N2 c= dom f
and
A5:
ex R2 being RestFunc of S,T st
( R2 /. (0. S) = 0. T & R2 is_continuous_in 0. S & ( for y being Point of S st y in N2 holds
(f /. y) - (f /. (g /. x0)) = ((diff (f,(g /. x0))) . (y - (g /. x0))) + (R2 /. (y - (g /. x0))) ) )
by NDIFF_1:47;
consider R2 being RestFunc of S,T such that
A6:
R2 /. (0. S) = 0. T
and
A7:
for y being Point of S st y in N2 holds
(f /. y) - (f /. (g /. x0)) = ((diff (f,(g /. x0))) . (y - (g /. x0))) + (R2 /. (y - (g /. x0)))
by A5;
reconsider L2 = diff (f,(g /. x0)) as Lipschitzian LinearOperator of S,T by LOPBAN_1:def 9;
consider L1 being LinearFunc of S, R1 being RestFunc of S such that
A8:
( diff (g,x0) = L1 /. 1 & ( for x being Real st x in N1 holds
(g /. x) - (g /. x0) = (L1 /. (x - x0)) + (R1 /. (x - x0)) ) )
by A3;
consider r being Point of S such that
A9:
for p being Real holds L1 /. p = p * r
by NDIFF_3:def 2;
reconsider p0 = 0 as Element of REAL by XREAL_0:def 1;
(g /. x0) - (g /. x0) = (L1 /. (x0 - x0)) + (R1 /. (x0 - x0))
by A8, RCOMP_1:16;
then
0. S = (L1 /. 0) + (R1 /. 0)
by RLVECT_1:15;
then
0. S = (p0 * r) + (R1 /. 0)
by A9;
then
0. S = (0. S) + (R1 /. 0)
by RLVECT_1:10;
then
R1 /. 0 = 0. S
by RLVECT_1:4;
then reconsider R0 = (L2 * R1) + (R2 * (L1 + R1)) as RestFunc of T by A6, Th5;
A10:
dom (L2 * L1) = REAL
by FUNCT_2:def 1;
reconsider q = L2 . r as Point of T ;
then reconsider L0 = L2 * L1 as LinearFunc of T by NDIFF_3:def 2;
g is_continuous_in x0
by A1, NDIFF_3:22;
then consider N3 being Neighbourhood of x0 such that
A11:
g .: N3 c= N2
by NFCONT_3:10;
consider N being Neighbourhood of x0 such that
A12:
N c= N1
and
A13:
N c= N3
by RCOMP_1:17;
A14:
dom L2 = the carrier of S
by FUNCT_2:def 1;
then A15:
rng R1 c= dom L2
;
A16:
rng L1 c= dom L2
by A14;
then A19:
N c= dom (f * g)
;
A20:
now for x being Real st x in N holds
((f * g) /. x) - ((f * g) /. x0) = (L0 /. (x - x0)) + (R0 /. (x - x0))let x be
Real;
( x in N implies ((f * g) /. x) - ((f * g) /. x0) = (L0 /. (x - x0)) + (R0 /. (x - x0)) )assume A21:
x in N
;
((f * g) /. x) - ((f * g) /. x0) = (L0 /. (x - x0)) + (R0 /. (x - x0))A22:
(g /. x) - (g /. x0) = (L1 /. (x - x0)) + (R1 /. (x - x0))
by A8, A12, A21;
x in N1
by A12, A21;
then
g . x in g .: N3
by A2, A13, A21, FUNCT_1:def 6;
then
g . x in N2
by A11;
then A24:
g /. x in N2
by A2, A12, A21, PARTFUN1:def 6;
A25:
x0 in N
by RCOMP_1:16;
A26:
R1 is
total
by NDIFF_3:def 1;
then A27:
dom R1 = REAL
by PARTFUN1:def 2;
A28:
dom (L2 * R1) = REAL
by A26, PARTFUN1:def 2;
L1 + R1 is
total
by A26, VFUNCT_1:32;
then A29:
dom (L1 + R1) = REAL
by PARTFUN1:def 2;
R2 is
total
by NDIFF_1:def 5;
then
dom R2 = the
carrier of
S
by PARTFUN1:def 2;
then A30:
rng (L1 + R1) c= dom R2
;
then
dom (R2 * (L1 + R1)) = dom (L1 + R1)
by RELAT_1:27;
then A31:
dom ((L2 * R1) + (R2 * (L1 + R1))) = REAL /\ REAL
by A28, A29, VFUNCT_1:def 1;
reconsider dxx0 =
x - x0 as
Element of
REAL by XREAL_0:def 1;
L2 . (R1 /. (x - x0)) = L2 /. (R1 /. (x - x0))
;
then A32:
L2 . (R1 /. (x - x0)) = (L2 * R1) /. dxx0
by A27, A15, PARTFUN2:5;
A33:
R2 /. ((L1 /. (x - x0)) + (R1 /. (x - x0))) =
R2 /. ((L1 + R1) /. dxx0)
by A29, VFUNCT_1:def 1
.=
(R2 * (L1 + R1)) /. dxx0
by A29, A30, PARTFUN2:5
;
A34:
dom L1 = REAL
by FUNCT_2:def 1;
A35:
(L2 * L1) /. (x - x0) = L2 /. (L1 /. dxx0)
by PARTFUN2:5, A34, A16;
thus ((f * g) /. x) - ((f * g) /. x0) =
(f /. (g /. x)) - ((f * g) /. x0)
by A19, A21, PARTFUN2:3
.=
(f /. (g /. x)) - (f /. (g /. x0))
by A19, A25, PARTFUN2:3
.=
((diff (f,(g /. x0))) . ((g /. x) - (g /. x0))) + (R2 /. ((g /. x) - (g /. x0)))
by A7, A24
.=
((L2 . (L1 /. (x - x0))) + (L2 . (R1 /. (x - x0)))) + ((R2 * (L1 + R1)) /. (x - x0))
by A22, A33, VECTSP_1:def 20
.=
(L2 . (L1 /. (x - x0))) + (((L2 * R1) /. (x - x0)) + ((R2 * (L1 + R1)) /. (x - x0)))
by A32, RLVECT_1:def 3
.=
(L0 /. (x - x0)) + (R0 /. (x - x0))
by A35, A31, VFUNCT_1:def 1
;
verum end;
hence A36:
f * g is_differentiable_in x0
by A19, NDIFF_3:def 3; diff ((f * g),x0) = (diff (f,(g /. x0))) . (diff (g,x0))
dom L1 = REAL
by FUNCT_2:def 1;
then (L2 * L1) /. 1 =
L2 /. (L1 /. jj)
by PARTFUN2:5, A16
.=
(diff (f,(g /. x0))) . (diff (g,x0))
by A8
;
hence
diff ((f * g),x0) = (diff (f,(g /. x0))) . (diff (g,x0))
by A36, A19, A20, NDIFF_3:def 4; verum