let E, F, G be RealNormSpace; :: thesis: 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 ) )
let L be Lipschitzian LinearOperator of F,G; :: thesis: ( 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 ) )
thus LTRN (0,L,E) = L by Def1; :: thesis: 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
let i be Nat; :: thesis: for V being Lipschitzian LinearOperator of E,(diff_SP (i,E,F)) holds (LTRN ((i + 1),L,E)) . V = (LTRN (i,L,E)) * V
consider K being Lipschitzian LinearOperator of (diff_SP ((i + 1),E,F)),(diff_SP ((i + 1),E,G)), M being Lipschitzian LinearOperator of (diff_SP (i,E,F)),(diff_SP (i,E,G)) such that
A1: ( (LTRN (L,E)) . (i + 1) = K & In (((LTRN (L,E)) . i),(R_NormSpace_of_BoundedLinearOperators ((diff_SP (i,E,F)),(diff_SP (i,E,G))))) = M & ( for V being Lipschitzian LinearOperator of E,(diff_SP (i,E,F)) holds K . V = M * V ) ) by Def1;
LTRN (i,L,E) in the carrier of (R_NormSpace_of_BoundedLinearOperators ((diff_SP (i,E,F)),(diff_SP (i,E,G)))) by LOPBAN_1:def 9;
then M = LTRN (i,L,E) by A1, SUBSET_1:def 8;
hence for V being Lipschitzian LinearOperator of E,(diff_SP (i,E,F)) holds (LTRN ((i + 1),L,E)) . V = (LTRN (i,L,E)) * V by A1; :: thesis: verum