:: deftheorem Def3 defines CTP NDIFF13:def 3 :
for S, E, F being RealNormSpace
for b₄ being Lipschitzian LinearOperator of [:(R_NormSpace_of_BoundedLinearOperators (S,E)),(R_NormSpace_of_BoundedLinearOperators (S,F)):],(R_NormSpace_of_BoundedLinearOperators (S,[:E,F:])) holds
( b₄ = CTP (S,E,F) iff for f being Lipschitzian LinearOperator of S,E
for g being Lipschitzian LinearOperator of S,F holds b₄ . (f,g) = <:f,g:> );