theorem Th2: :: NDIFF12:2

for E, F, G being RealNormSpace
for f being Lipschitzian BilinearOperator of E,F,G
for z being Point of [:E,F:] holds
( f * (reproj1 z) is Lipschitzian LinearOperator of E,G & f * (reproj2 z) is Lipschitzian LinearOperator of F,G & ex g being Point of (R_NormSpace_of_BoundedBilinearOperators (E,F,G)) st
( f = g & ( for x being VECTOR of E holds ||.((f * (reproj1 z)) . x).|| <= (||.g.|| * ||.(z `2).||) * ||.x.|| ) & ( for y being VECTOR of F holds ||.((f * (reproj2 z)) . y).|| <= (||.g.|| * ||.(z `1).||) * ||.y.|| ) ) )