:: deftheorem Def1 defines LTRN NDIFF13:def 1 :
for E, F, G being RealNormSpace
for L being Lipschitzian LinearOperator of F,G
for b₅ being Function holds
( b₅ = LTRN (L,E) iff ( dom b₅ = NAT & b₅ . 0 = L & ( for i being Nat 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
( b₅ . (i + 1) = K & In ((b₅ . 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 ) ) ) ) );