theorem Th4: :: NDIFF12:4

for E, F, G being RealNormSpace
for f being Lipschitzian BilinearOperator of E,F,G
for z being Point of [:E,F:] holds
( f is_partial_differentiable_in`1 z & partdiff`1 (f,z) = f * (reproj1 z) & f is_partial_differentiable_in`2 z & partdiff`2 (f,z) = f * (reproj2 z) )