theorem Th12: :: NDIFF12:12

for E, F, G being RealNormSpace
for f being Lipschitzian BilinearOperator of E,F,G
for z being Point of [:E,F:]
for dx being Point of E
for dy being Point of F holds (diff (f,z)) . (dx,dy) = ((partdiff`1 (f,z)) . dx) + ((partdiff`2 (f,z)) . dy)