let E, F, G be RealNormSpace; :: thesis: for L being Lipschitzian LinearOperator of F,G
for i being Nat holds (LTRN (L,E)) . i is Lipschitzian LinearOperator of (diff_SP (i,E,F)),(diff_SP (i,E,G))
let L be Lipschitzian LinearOperator of F,G; :: thesis: for i being Nat holds (LTRN (L,E)) . i is Lipschitzian LinearOperator of (diff_SP (i,E,F)),(diff_SP (i,E,G))
defpred S₁[ Nat] means (LTRN (L,E)) . $1 is Lipschitzian LinearOperator of (diff_SP ($1,E,F)),(diff_SP ($1,E,G));
A1: diff_SP (0,E,F) = F by NDIFF_6:7;
A2: diff_SP (0,E,G) = G by NDIFF_6:7;
A3: S₁[ 0 ] by A1, A2, Def1;
A4: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume S₁[i] ; :: thesis: S₁[i + 1]
ex K being Lipschitzian LinearOperator of (diff_SP ((i + 1),E,F)),(diff_SP ((i + 1),E,G)) ex M being Lipschitzian LinearOperator of (diff_SP (i,E,F)),(diff_SP (i,E,G)) st
( (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;
hence S₁[i + 1] ; :: thesis: verum

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A3, A4);
hence for i being Nat holds (LTRN (L,E)) . i is Lipschitzian LinearOperator of (diff_SP (i,E,F)),(diff_SP (i,E,G)) ; :: thesis: verum