defpred S1[ Nat] means for E, F, G being RealNormSpace
for Z being Subset of E
for T being Subset of F
for u being PartFunc of E,F
for v being PartFunc of F,G st u .: Z c= T & u is_differentiable_on $1,Z & v is_differentiable_on $1,T holds
v * u is_differentiable_on $1,Z;
A1:
S1[ 0 ]
proof
let E,
F,
G be
RealNormSpace;
for Z being Subset of E
for T being Subset of F
for u being PartFunc of E,F
for v being PartFunc of F,G st u .: Z c= T & u is_differentiable_on 0 ,Z & v is_differentiable_on 0 ,T holds
v * u is_differentiable_on 0 ,Zlet Z be
Subset of
E;
for T being Subset of F
for u being PartFunc of E,F
for v being PartFunc of F,G st u .: Z c= T & u is_differentiable_on 0 ,Z & v is_differentiable_on 0 ,T holds
v * u is_differentiable_on 0 ,Zlet T be
Subset of
F;
for u being PartFunc of E,F
for v being PartFunc of F,G st u .: Z c= T & u is_differentiable_on 0 ,Z & v is_differentiable_on 0 ,T holds
v * u is_differentiable_on 0 ,Zlet u be
PartFunc of
E,
F;
for v being PartFunc of F,G st u .: Z c= T & u is_differentiable_on 0 ,Z & v is_differentiable_on 0 ,T holds
v * u is_differentiable_on 0 ,Zlet v be
PartFunc of
F,
G;
( u .: Z c= T & u is_differentiable_on 0 ,Z & v is_differentiable_on 0 ,T implies v * u is_differentiable_on 0 ,Z )
assume A2:
(
u .: Z c= T &
u is_differentiable_on 0 ,
Z &
v is_differentiable_on 0 ,
T )
;
v * u is_differentiable_on 0 ,Z
for
x being
object st
x in Z holds
x in dom (v * u)
hence
v * u is_differentiable_on 0 ,
Z
by TARSKI:def 3;
verum
end;
A4:
for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be
Nat;
( S1[i] implies S1[i + 1] )
assume A5:
S1[
i]
;
S1[i + 1]
let E,
F,
G be
RealNormSpace;
for Z being Subset of E
for T being Subset of F
for u being PartFunc of E,F
for v being PartFunc of F,G st u .: Z c= T & u is_differentiable_on i + 1,Z & v is_differentiable_on i + 1,T holds
v * u is_differentiable_on i + 1,Zlet Z be
Subset of
E;
for T being Subset of F
for u being PartFunc of E,F
for v being PartFunc of F,G st u .: Z c= T & u is_differentiable_on i + 1,Z & v is_differentiable_on i + 1,T holds
v * u is_differentiable_on i + 1,Zlet T be
Subset of
F;
for u being PartFunc of E,F
for v being PartFunc of F,G st u .: Z c= T & u is_differentiable_on i + 1,Z & v is_differentiable_on i + 1,T holds
v * u is_differentiable_on i + 1,Zlet u be
PartFunc of
E,
F;
for v being PartFunc of F,G st u .: Z c= T & u is_differentiable_on i + 1,Z & v is_differentiable_on i + 1,T holds
v * u is_differentiable_on i + 1,Zlet v be
PartFunc of
F,
G;
( u .: Z c= T & u is_differentiable_on i + 1,Z & v is_differentiable_on i + 1,T implies v * u is_differentiable_on i + 1,Z )
assume A6:
(
u .: Z c= T &
u is_differentiable_on i + 1,
Z &
v is_differentiable_on i + 1,
T )
;
v * u is_differentiable_on i + 1,Z
0 + i <= i + 1
by XREAL_1:7;
then A7:
(
u is_differentiable_on i,
Z &
v is_differentiable_on i,
T )
by A6, NDIFF_6:17;
0 <= i
by NAT_1:2;
then A8:
(
u is_differentiable_on 0 + 1,
Z &
v is_differentiable_on 0 + 1,
T )
by A6, NDIFF_6:17, XREAL_1:7;
then A9:
u is_differentiable_on Z
by Th3, NDIFF_6:15;
A10:
v is_differentiable_on T
by A8, Th3, NDIFF_6:15;
then A11:
(
v * u is_differentiable_on Z & ( for
x being
Point of
E st
x in Z holds
((v * u) `| Z) /. x = ((v `| T) /. (u /. x)) * ((u `| Z) /. x) ) )
by A6, A9, Th19;
A12:
u `| Z is_differentiable_on i,
Z
by A6, Th36;
A13:
v `| T is_differentiable_on i,
T
by A6, Th36;
set t =
(v `| T) * u;
A14:
(v `| T) * u is_differentiable_on i,
Z
by A5, A6, A7, A13;
consider B being
Lipschitzian BilinearOperator of
(R_NormSpace_of_BoundedLinearOperators (E,F)),
(R_NormSpace_of_BoundedLinearOperators (F,G)),
(R_NormSpace_of_BoundedLinearOperators (E,G)) such that A15:
for
u being
Point of
(R_NormSpace_of_BoundedLinearOperators (E,F)) for
v being
Point of
(R_NormSpace_of_BoundedLinearOperators (F,G)) holds
B . (
u,
v)
= v * u
by Th38;
set w2 =
<:(u `| Z),((v `| T) * u):>;
A16:
dom <:(u `| Z),((v `| T) * u):> =
(dom (u `| Z)) /\ (dom ((v `| T) * u))
by FUNCT_3:def 7
.=
Z /\ (dom ((v `| T) * u))
by A9, NDIFF_1:def 9
.=
Z
by A14, XBOOLE_1:28
;
A17:
rng <:(u `| Z),((v `| T) * u):> c= [:(rng (u `| Z)),(rng ((v `| T) * u)):]
by FUNCT_3:51;
[:(rng (u `| Z)),(rng ((v `| T) * u)):] c= the
carrier of
[:(R_NormSpace_of_BoundedLinearOperators (E,F)),(R_NormSpace_of_BoundedLinearOperators (F,G)):]
by ZFMISC_1:96;
then
rng <:(u `| Z),((v `| T) * u):> c= the
carrier of
[:(R_NormSpace_of_BoundedLinearOperators (E,F)),(R_NormSpace_of_BoundedLinearOperators (F,G)):]
by A17, XBOOLE_1:1;
then reconsider w2 =
<:(u `| Z),((v `| T) * u):> as
PartFunc of
E,
[:(R_NormSpace_of_BoundedLinearOperators (E,F)),(R_NormSpace_of_BoundedLinearOperators (F,G)):] by A16, RELSET_1:4;
reconsider W =
B * w2 as
PartFunc of
E,
(R_NormSpace_of_BoundedLinearOperators (E,G)) ;
A18:
W is_differentiable_on i,
Z
by A12, A14, Th39;
dom B = the
carrier of
[:(R_NormSpace_of_BoundedLinearOperators (E,F)),(R_NormSpace_of_BoundedLinearOperators (F,G)):]
by FUNCT_2:def 1;
then
rng w2 c= dom B
;
then A19:
dom W = Z
by A16, RELAT_1:27;
A20:
dom ((v * u) `| Z) = Z
by A11, NDIFF_1:def 9;
for
x0 being
object st
x0 in dom ((v * u) `| Z) holds
((v * u) `| Z) . x0 = W . x0
proof
let x0 be
object ;
( x0 in dom ((v * u) `| Z) implies ((v * u) `| Z) . x0 = W . x0 )
assume A21:
x0 in dom ((v * u) `| Z)
;
((v * u) `| Z) . x0 = W . x0
then A22:
x0 in Z
by A11, NDIFF_1:def 9;
reconsider x =
x0 as
Point of
E by A21;
A23:
((v * u) `| Z) . x0 =
((v * u) `| Z) /. x
by A21, PARTFUN1:def 6
.=
((v `| T) /. (u /. x)) * ((u `| Z) /. x)
by A6, A9, A10, A22, Th19
.=
B . (
((u `| Z) /. x),
((v `| T) /. (u /. x)))
by A15
.=
B . [((u `| Z) /. x),((v `| T) /. (u /. x))]
by BINOP_1:def 1
;
A24:
dom (u `| Z) = Z
by A9, NDIFF_1:def 9;
A25:
dom (v `| T) = T
by A10, NDIFF_1:def 9;
u /. x = u . x
by A6, A22, PARTFUN1:def 6;
then A26:
u /. x in u .: Z
by A6, A22, FUNCT_1:def 6;
[((u `| Z) /. x),((v `| T) /. (u /. x))] =
[((u `| Z) . x),((v `| T) /. (u /. x))]
by A22, A24, PARTFUN1:def 6
.=
[((u `| Z) . x),((v `| T) . (u /. x))]
by A6, A25, A26, PARTFUN1:def 6
.=
[((u `| Z) . x),((v `| T) . (u . x))]
by A6, A22, PARTFUN1:def 6
.=
[((u `| Z) . x),(((v `| T) * u) . x)]
by A6, A22, FUNCT_1:13
.=
w2 . x
by A16, A22, FUNCT_3:def 7
;
hence
((v * u) `| Z) . x0 = W . x0
by A16, A22, A23, FUNCT_1:13;
verum
end;
then
(v * u) `| Z is_differentiable_on i,
Z
by A18, A19, A20, FUNCT_1:2;
hence
v * u is_differentiable_on i + 1,
Z
by A6, A9, A10, Th19, Th32;
verum
end;
for i being Nat holds S1[i]
from NAT_1:sch 2(A1, A4);
hence
for i being Nat
for E, F, G being RealNormSpace
for Z being Subset of E
for T being Subset of F
for u being PartFunc of E,F
for v being PartFunc of F,G st u .: Z c= T & u is_differentiable_on i,Z & v is_differentiable_on i,T holds
v * u is_differentiable_on i,Z
; verum