theorem Th14: :: NDIFF12:14

for E, F, G being RealNormSpace
for f being Lipschitzian BilinearOperator of E,F,G
for Z being Subset of [:E,F:] st Z is open holds
( f is_differentiable_on Z & f `| Z is_continuous_on Z )