theorem Th46: :: NDIFF13:45

for E, F being RealNormSpace ex L10 being Lipschitzian LinearOperator of E,[:E,F:] st
for dx being Point of E holds L10 . dx = [dx,(0. F)]