theorem Th6: :: NDIFF12:6

for E, F, G being RealNormSpace
for f being Lipschitzian BilinearOperator of E,F,G ex K being Real st
( 0 <= K & ( for z being Point of [:E,F:] holds
( ||.(partdiff`1 (f,z)).|| <= K * ||.z.|| & ||.(partdiff`2 (f,z)).|| <= K * ||.z.|| ) ) )