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
( ||.(partdiff`1 (f,z)).|| <= K * ||.z.|| & ||.(partdiff`2 (f,z)).|| <= K * ||.z.|| ) ) )
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
( ||.(partdiff`1 (f,z)).|| <= K * ||.z.|| & ||.(partdiff`2 (f,z)).|| <= K * ||.z.|| ) ) )
consider K being Real such that
A1: ( 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.|| ) ) ) ) by Th3;
take K ; :: thesis: ( 0 <= K & ( for z being Point of [:E,F:] holds
( ||.(partdiff`1 (f,z)).|| <= K * ||.z.|| & ||.(partdiff`2 (f,z)).|| <= K * ||.z.|| ) ) )
thus 0 <= K by A1; :: thesis: for z being Point of [:E,F:] holds
( ||.(partdiff`1 (f,z)).|| <= K * ||.z.|| & ||.(partdiff`2 (f,z)).|| <= K * ||.z.|| )
let z be Point of [:E,F:]; :: thesis: ( ||.(partdiff`1 (f,z)).|| <= K * ||.z.|| & ||.(partdiff`2 (f,z)).|| <= K * ||.z.|| )
reconsider L1 = f * (reproj1 z) as Lipschitzian LinearOperator of E,G by Th2;
reconsider L2 = f * (reproj2 z) as Lipschitzian LinearOperator of F,G by Th2;
A2: partdiff`1 (f,z) = L1 by Th4;
A3: partdiff`2 (f,z) = L2 by Th4;
A4: z = [(z `1),(z `2)] by Th5;
A5: ( ( for s being Real st s in PreNorms L2 holds
s <= K * ||.z.|| ) implies upper_bound (PreNorms L2) <= K * ||.z.|| ) by SEQ_4:45;

A6: now :: thesis: for t being VECTOR of F st ||.t.|| <= 1 holds
||.(L2 . t).|| <= K * ||.z.||

let t be VECTOR of F; :: thesis: ( ||.t.|| <= 1 implies ||.(L2 . t).|| <= K * ||.z.|| )
assume A7: ||.t.|| <= 1 ; :: thesis: ||.(L2 . t).|| <= K * ||.z.||
A8: ||.(L2 . t).|| <= (K * ||.(z `1).||) * ||.t.|| by A1;
0 <= ||.(z `1).|| by NORMSP_1:4;
then 0 <= K * ||.(z `1).|| by A1, XREAL_1:127;
then (K * ||.(z `1).||) * ||.t.|| <= (K * ||.(z `1).||) * 1 by A7, XREAL_1:64;
then A9: ||.(L2 . t).|| <= K * ||.(z `1).|| by A8, XXREAL_0:2;
K * ||.(z `1).|| <= K * ||.z.|| by A1, A4, LOPBAN_7:15, XREAL_1:64;
hence ||.(L2 . t).|| <= K * ||.z.|| by A9, XXREAL_0:2; :: thesis: verum

end;

A10: now :: thesis: for r being Real st r in PreNorms L2 holds
r <= K * ||.z.||

let r be Real; :: thesis: ( r in PreNorms L2 implies r <= K * ||.z.|| )
assume r in PreNorms L2 ; :: thesis: r <= K * ||.z.||
then ex t being VECTOR of F st
( r = ||.(L2 . t).|| & ||.t.|| <= 1 ) ;
hence r <= K * ||.z.|| by A6; :: thesis: verum

end;

A11: ( ( for s being Real st s in PreNorms L1 holds
s <= K * ||.z.|| ) implies upper_bound (PreNorms L1) <= K * ||.z.|| ) by SEQ_4:45;

A12: now :: thesis: for t being VECTOR of E st ||.t.|| <= 1 holds
||.(L1 . t).|| <= K * ||.z.||

let t be VECTOR of E; :: thesis: ( ||.t.|| <= 1 implies ||.(L1 . t).|| <= K * ||.z.|| )
assume A13: ||.t.|| <= 1 ; :: thesis: ||.(L1 . t).|| <= K * ||.z.||
A14: ||.(L1 . t).|| <= (K * ||.(z `2).||) * ||.t.|| by A1;
0 <= ||.(z `2).|| by NORMSP_1:4;
then 0 <= K * ||.(z `2).|| by A1, XREAL_1:127;
then (K * ||.(z `2).||) * ||.t.|| <= (K * ||.(z `2).||) * 1 by A13, XREAL_1:64;
then A15: ||.(L1 . t).|| <= K * ||.(z `2).|| by A14, XXREAL_0:2;
K * ||.(z `2).|| <= K * ||.z.|| by A1, A4, LOPBAN_7:15, XREAL_1:64;
hence ||.(L1 . t).|| <= K * ||.z.|| by A15, XXREAL_0:2; :: thesis: verum

end;

now :: thesis: for r being Real st r in PreNorms L1 holds
r <= K * ||.z.||

let r be Real; :: thesis: ( r in PreNorms L1 implies r <= K * ||.z.|| )
assume r in PreNorms L1 ; :: thesis: r <= K * ||.z.||
then ex t being VECTOR of E st
( r = ||.(L1 . t).|| & ||.t.|| <= 1 ) ;
hence r <= K * ||.z.|| by A12; :: thesis: verum

end;

hence ( ||.(partdiff`1 (f,z)).|| <= K * ||.z.|| & ||.(partdiff`2 (f,z)).|| <= K * ||.z.|| ) by A2, A3, A5, A10, A11, LOPBAN_1:30; :: thesis: verum