theorem Th47: :: NDIFF13:46

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