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 & diff (u,$1,Z) is_continuous_on Z & v is_differentiable_on $1,T & diff (v,$1,T) is_continuous_on T holds
( v * u is_differentiable_on $1,Z & diff ((v * u),$1,Z) is_continuous_on 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 & diff (u,0,Z) is_continuous_on Z & v is_differentiable_on 0 ,T & diff (v,0,T) is_continuous_on T holds
( v * u is_differentiable_on 0 ,Z & diff ((v * u),0,Z) is_continuous_on Z )let 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 & diff (u,0,Z) is_continuous_on Z & v is_differentiable_on 0 ,T & diff (v,0,T) is_continuous_on T holds
( v * u is_differentiable_on 0 ,Z & diff ((v * u),0,Z) is_continuous_on Z )let 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 & diff (u,0,Z) is_continuous_on Z & v is_differentiable_on 0 ,T & diff (v,0,T) is_continuous_on T holds
( v * u is_differentiable_on 0 ,Z & diff ((v * u),0,Z) is_continuous_on Z )let u be
PartFunc of
E,
F;
for v being PartFunc of F,G st u .: Z c= T & u is_differentiable_on 0 ,Z & diff (u,0,Z) is_continuous_on Z & v is_differentiable_on 0 ,T & diff (v,0,T) is_continuous_on T holds
( v * u is_differentiable_on 0 ,Z & diff ((v * u),0,Z) is_continuous_on Z )let v be
PartFunc of
F,
G;
( u .: Z c= T & u is_differentiable_on 0 ,Z & diff (u,0,Z) is_continuous_on Z & v is_differentiable_on 0 ,T & diff (v,0,T) is_continuous_on T implies ( v * u is_differentiable_on 0 ,Z & diff ((v * u),0,Z) is_continuous_on Z ) )
assume A2:
(
u .: Z c= T &
u is_differentiable_on 0 ,
Z &
diff (
u,
0,
Z)
is_continuous_on Z &
v is_differentiable_on 0 ,
T &
diff (
v,
0,
T)
is_continuous_on T )
;
( v * u is_differentiable_on 0 ,Z & diff ((v * u),0,Z) is_continuous_on Z )
hence
v * u is_differentiable_on 0 ,
Z
by Th43;
diff ((v * u),0,Z) is_continuous_on Z
A3:
diff_SP (
0,
E,
F)
= F
by NDIFF_6:7;
diff (
u,
0,
Z)
= u | Z
by NDIFF_6:11;
then A4:
u is_continuous_on Z
by A2, A3, NFCONT_1:21;
A5:
diff_SP (
0,
F,
G)
= G
by NDIFF_6:7;
diff (
v,
0,
T)
= v | T
by NDIFF_6:11;
then
v is_continuous_on T
by A2, A5, NFCONT_1:21;
then A6:
v * u is_continuous_on Z
by A2, A4, Th16;
A7:
diff (
(v * u),
0,
Z)
= (v * u) | Z
by NDIFF_6:11;
diff_SP (
0,
E,
G)
= G
by NDIFF_6:7;
hence
diff (
(v * u),
0,
Z)
is_continuous_on Z
by A6, A7, NFCONT_1:21;
verum
end;
A8:
for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be
Nat;
( S1[i] implies S1[i + 1] )
assume A9:
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 & diff (u,(i + 1),Z) is_continuous_on Z & v is_differentiable_on i + 1,T & diff (v,(i + 1),T) is_continuous_on T holds
( v * u is_differentiable_on i + 1,Z & diff ((v * u),(i + 1),Z) is_continuous_on Z )let 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 & diff (u,(i + 1),Z) is_continuous_on Z & v is_differentiable_on i + 1,T & diff (v,(i + 1),T) is_continuous_on T holds
( v * u is_differentiable_on i + 1,Z & diff ((v * u),(i + 1),Z) is_continuous_on Z )let 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 & diff (u,(i + 1),Z) is_continuous_on Z & v is_differentiable_on i + 1,T & diff (v,(i + 1),T) is_continuous_on T holds
( v * u is_differentiable_on i + 1,Z & diff ((v * u),(i + 1),Z) is_continuous_on Z )let 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 & diff (u,(i + 1),Z) is_continuous_on Z & v is_differentiable_on i + 1,T & diff (v,(i + 1),T) is_continuous_on T holds
( v * u is_differentiable_on i + 1,Z & diff ((v * u),(i + 1),Z) is_continuous_on Z )let v be
PartFunc of
F,
G;
( u .: Z c= T & u is_differentiable_on i + 1,Z & diff (u,(i + 1),Z) is_continuous_on Z & v is_differentiable_on i + 1,T & diff (v,(i + 1),T) is_continuous_on T implies ( v * u is_differentiable_on i + 1,Z & diff ((v * u),(i + 1),Z) is_continuous_on Z ) )
assume A10:
(
u .: Z c= T &
u is_differentiable_on i + 1,
Z &
diff (
u,
(i + 1),
Z)
is_continuous_on Z &
v is_differentiable_on i + 1,
T &
diff (
v,
(i + 1),
T)
is_continuous_on T )
;
( v * u is_differentiable_on i + 1,Z & diff ((v * u),(i + 1),Z) is_continuous_on Z )
0 + i <= i + 1
by XREAL_1:7;
then A11:
(
u is_differentiable_on i,
Z &
v is_differentiable_on i,
T )
by A10, NDIFF_6:17;
A12:
diff (
u,
i,
Z)
is_continuous_on Z
by A10, NDIFF_1:45, NDIFF_6:14;
0 <= i
by NAT_1:2;
then A13:
(
u is_differentiable_on 0 + 1,
Z &
v is_differentiable_on 0 + 1,
T )
by A10, XREAL_1:7, NDIFF_6:17;
then A14:
u is_differentiable_on Z
by Th3, NDIFF_6:15;
A15:
v is_differentiable_on T
by A13, Th3, NDIFF_6:15;
then A16:
(
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 A10, A14, Th19;
A17:
(
u `| Z is_differentiable_on i,
Z &
diff (
(u `| Z),
i,
Z)
is_continuous_on Z )
by A10, Th37;
A18:
(
v `| T is_differentiable_on i,
T &
diff (
(v `| T),
i,
T)
is_continuous_on T )
by A10, Th37;
set t =
(v `| T) * u;
A19:
(
(v `| T) * u is_differentiable_on i,
Z &
diff (
((v `| T) * u),
i,
Z)
is_continuous_on Z )
by A9, A10, A11, A12, A18;
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 A20:
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):>;
A21:
dom <:(u `| Z),((v `| T) * u):> =
(dom (u `| Z)) /\ (dom ((v `| T) * u))
by FUNCT_3:def 7
.=
Z /\ (dom ((v `| T) * u))
by A14, NDIFF_1:def 9
.=
Z
by A19, XBOOLE_1:28
;
A22:
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)), the carrier of (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 A22, 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 A21, RELSET_1:4;
reconsider W =
B * w2 as
PartFunc of
E,
(R_NormSpace_of_BoundedLinearOperators (E,G)) ;
A23:
(
W is_differentiable_on i,
Z &
diff (
W,
i,
Z)
is_continuous_on Z )
by A17, A19, Th42;
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 A24:
dom W = Z
by A21, RELAT_1:27;
A25:
dom ((v * u) `| Z) = Z
by A16, 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 A26:
x0 in dom ((v * u) `| Z)
;
((v * u) `| Z) . x0 = W . x0
then reconsider x =
x0 as
Point of
E ;
A27:
((v * u) `| Z) . x0 =
((v * u) `| Z) /. x
by A26, PARTFUN1:def 6
.=
((v `| T) /. (u /. x)) * ((u `| Z) /. x)
by A10, A14, A15, A25, A26, Th19
.=
B . (
((u `| Z) /. x),
((v `| T) /. (u /. x)))
by A20
.=
B . [((u `| Z) /. x),((v `| T) /. (u /. x))]
by BINOP_1:def 1
;
A28:
dom (u `| Z) = Z
by A14, NDIFF_1:def 9;
A29:
dom (v `| T) = T
by A15, NDIFF_1:def 9;
u /. x = u . x
by A10, A25, A26, PARTFUN1:def 6;
then A30:
u /. x in u .: Z
by A10, A25, A26, FUNCT_1:def 6;
[((u `| Z) /. x),((v `| T) /. (u /. x))] =
[((u `| Z) . x),((v `| T) /. (u /. x))]
by A25, A26, A28, PARTFUN1:def 6
.=
[((u `| Z) . x),((v `| T) . (u /. x))]
by A10, A29, A30, PARTFUN1:def 6
.=
[((u `| Z) . x),((v `| T) . (u . x))]
by A10, A25, A26, PARTFUN1:def 6
.=
[((u `| Z) . x),(((v `| T) * u) . x)]
by A10, A25, A26, FUNCT_1:13
.=
w2 . x
by A21, A25, A26, FUNCT_3:def 7
;
hence
((v * u) `| Z) . x0 = W . x0
by A21, A25, A26, A27, FUNCT_1:13;
verum
end;
then A31:
(
(v * u) `| Z is_differentiable_on i,
Z &
diff (
((v * u) `| Z),
i,
Z)
is_continuous_on Z )
by A23, A24, A25, FUNCT_1:2;
v * u is_differentiable_on Z
by A10, A14, A15, Th19;
hence
(
v * u is_differentiable_on i + 1,
Z &
diff (
(v * u),
(i + 1),
Z)
is_continuous_on Z )
by A31, Th33;
verum
end;
for i being Nat holds S1[i]
from NAT_1:sch 2(A1, A8);
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 & diff (u,i,Z) is_continuous_on Z & v is_differentiable_on i,T & diff (v,i,T) is_continuous_on T holds
( v * u is_differentiable_on i,Z & diff ((v * u),i,Z) is_continuous_on Z )
; verum