let E, F, G be RealNormSpace; :: thesis:
let f be Lipschitzian BilinearOperator of E,F,G; :: thesis:
let z be Point of [:E,F:]; :: thesis:
reconsider g = f as Point of (R_NormSpace_of_BoundedBilinearOperators (E,F,G)) by LOPBAN_9:def 4;
set K = ||.g.||;
A1: ( 0 <= ||.g.|| & ( for x being VECTOR of E
for y being VECTOR of F holds ||.(f . (x,y)).|| <= (||.g.|| * ||.x.||) * ||.y.|| ) ) by LOPBAN_9:16, LOPBAN_9:17;
reconsider L1 = f * (reproj1 z) as LinearOperator of E,G by Th1;
reconsider L2 = f * (reproj2 z) as LinearOperator of F,G by Th1;
set K1 = ||.g.|| * ||.(z `2).||;
set K2 = ||.g.|| * ||.(z `1).||;
A2: 0 <= ||.(z `2).|| by NORMSP_1:4;
A3: for x being VECTOR of E holds ||.(L1 . x).|| <= (||.g.|| * ||.(z `2).||) * ||.x.||

end;

let y be VECTOR of F; :: thesis:
f . ((z `1),y) = f . ((reproj2 z) . y) by NDIFF_7:def 2
.= L2 . y by FUNCT_2:15 ;
hence ||.(L2 . y).|| <= (||.g.|| * ||.(z `1).||) * ||.y.|| by LOPBAN_9:16; :: thesis:

end;