theorem Th3: :: NDIFF12:3

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
( ( for x being Point of E holds ||.((f * (reproj1 z)) . x).|| <= (K * ||.(z `2).||) * ||.x.|| ) & ( for y being Point of F holds ||.((f * (reproj2 z)) . y).|| <= (K * ||.(z `1).||) * ||.y.|| ) ) ) )