theorem Th25:
for
E,
F,
G being
RealNormSpace for
Z being
Subset of
E for
u being
PartFunc of
E,
F for
L being
Lipschitzian LinearOperator of
F,
G for
i being
Nat st
u is_differentiable_on i,
Z holds
(
L * u is_differentiable_on i,
Z &
diff (
(L * u),
i,
Z)
= (LTRN (i,L,E)) * (diff (u,i,Z)) )