let E, F, G be RealNormSpace; :: thesis: 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.|| ) ) ) )
let f be Lipschitzian BilinearOperator of E,F,G; :: thesis: 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.|| ) ) ) )
consider K being Real such that
A1: ( 0 <= K & ( for x being VECTOR of E
for y being VECTOR of F holds ||.(f . (x,y)).|| <= (K * ||.x.||) * ||.y.|| ) ) by LOPBAN_9:def 3;
take K ; :: thesis: ( 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.|| ) ) ) )
thus 0 <= K by A1; :: thesis: 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.|| ) )
let z be Point of [:E,F:]; :: thesis: ( ( 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.|| ) )
set L1 = f * (reproj1 z);
set L2 = f * (reproj2 z);
set K1 = K * ||.(z `2).||;
set K2 = K * ||.(z `1).||;
thus for x being VECTOR of E holds ||.((f * (reproj1 z)) . x).|| <= (K * ||.(z `2).||) * ||.x.|| :: thesis: for y being Point of F holds ||.((f * (reproj2 z)) . y).|| <= (K * ||.(z `1).||) * ||.y.||

proof

let x be VECTOR of E; :: thesis: ||.((f * (reproj1 z)) . x).|| <= (K * ||.(z `2).||) * ||.x.||
f . (x,(z `2)) = f . ((reproj1 z) . x) by NDIFF_7:def 1
.= (f * (reproj1 z)) . x by FUNCT_2:15 ;
then ||.((f * (reproj1 z)) . x).|| <= (K * ||.x.||) * ||.(z `2).|| by A1;
hence ||.((f * (reproj1 z)) . x).|| <= (K * ||.(z `2).||) * ||.x.|| ; :: thesis: verum

end;

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