let S, E, F be RealNormSpace; :: thesis: for i being Nat holds CTP (S,(diff_SP (i,S,E)),(diff_SP (i,S,F))) is Lipschitzian LinearOperator of [:(diff_SP ((i + 1),S,E)),(diff_SP ((i + 1),S,F)):],(R_NormSpace_of_BoundedLinearOperators (S,[:(diff_SP (i,S,E)),(diff_SP (i,S,F)):]))
let i be Nat; :: thesis: CTP (S,(diff_SP (i,S,E)),(diff_SP (i,S,F))) is Lipschitzian LinearOperator of [:(diff_SP ((i + 1),S,E)),(diff_SP ((i + 1),S,F)):],(R_NormSpace_of_BoundedLinearOperators (S,[:(diff_SP (i,S,E)),(diff_SP (i,S,F)):]))
set E1 = diff_SP (i,S,E);
set F1 = diff_SP (i,S,F);
A1: R_NormSpace_of_BoundedLinearOperators (S,(diff_SP (i,S,E))) = diff_SP ((i + 1),S,E) by NDIFF_6:10;
R_NormSpace_of_BoundedLinearOperators (S,(diff_SP (i,S,F))) = diff_SP ((i + 1),S,F) by NDIFF_6:10;
hence CTP (S,(diff_SP (i,S,E)),(diff_SP (i,S,F))) is Lipschitzian LinearOperator of [:(diff_SP ((i + 1),S,E)),(diff_SP ((i + 1),S,F)):],(R_NormSpace_of_BoundedLinearOperators (S,[:(diff_SP (i,S,E)),(diff_SP (i,S,F)):])) by A1; :: thesis: verum