theorem Th22:
for
E,
F,
G being
RealNormSpace for
L being
Lipschitzian LinearOperator of
F,
G holds
(
LTRN (
0,
L,
E)
= L & ( for
i being
Nat for
V being
Lipschitzian LinearOperator of
E,
(diff_SP (i,E,F)) holds
(LTRN ((i + 1),L,E)) . V = (LTRN (i,L,E)) * V ) )