let E, F, G be RealNormSpace; :: thesis:
let f be Lipschitzian BilinearOperator of E,F,G; :: thesis:
consider K0 being Real such that
A1: ( 0 <= K0 & ( for x being VECTOR of E
for y being VECTOR of F holds ||.(f . (x,y)).|| <= (K0 * ||.x.||) * ||.y.|| ) ) by LOPBAN_9:def 3;
consider K being Real such that
A2: ( 0 <= K & ( for z being Point of [:E,F:] ex L being Lipschitzian LinearOperator of [:E,F:],G st
for dx being Point of E
for dy being Point of F holds
( L . (dx,dy) = (f . (dx,(z `2))) + (f . ((z `1),dy)) & ( for s being Point of [:E,F:] holds ||.(L . s).|| <= (K * ||.z.||) * ||.s.|| ) ) ) ) by Th10;
take K ; :: thesis:
thus 0 <= K by A2; :: thesis:
let z be Point of [:E,F:]; :: thesis:
consider L being Lipschitzian LinearOperator of [:E,F:],G such that
A3: for dx being Point of E
for dy being Point of F holds L . (dx,dy) = (f . (dx,(z `2))) + (f . ((z `1),dy)) and
A4: for s being Point of [:E,F:] holds ||.(L . s).|| <= (K * ||.z.||) * ||.s.|| by A2;
reconsider L0 = L as Point of (R_NormSpace_of_BoundedLinearOperators ([:E,F:],G)) by LOPBAN_1:def 9;
deffunc H₁( Element of E, Element of F) -> Element of the carrier of G = f . ($1,$2);
consider R being Function of [: the carrier of E, the carrier of F:], the carrier of G such that
A5: for dx being Element of the carrier of E
for dy being Element of the carrier of F holds R . (dx,dy) = H₁(dx,dy) from BINOP_1:sch 4();
reconsider R = R as Function of [:E,F:],G ;
A6: dom R = the carrier of [:E,F:] by FUNCT_2:def 1;
for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for w being Point of [:E,F:] st w <> 0. [:E,F:] & ||.w.|| < d holds
(||.w.|| ") * ||.(R /. w).|| < r ) )

let r be Real; :: thesis:
assume A7: r > 0 ; :: thesis:
A8: 0 + 0 < K0 + 1 by A1, XREAL_1:8;
set d = r / (K0 + 1);
take r / (K0 + 1) ; :: thesis:
thus 0 < r / (K0 + 1) by A7, A8, XREAL_1:139; :: thesis:
let w be Point of [:E,F:]; :: thesis:
assume A9: ( w <> 0. [:E,F:] & ||.w.|| < r / (K0 + 1) ) ; :: thesis:
then A10: 0 <> ||.w.|| by NORMSP_0:def 5;
0 <= ||.w.|| by NORMSP_1:4;
then A11: 0 < ||.w.|| by A9, NORMSP_0:def 5, XXREAL_0:1;
consider x being Point of E, y being Point of F such that
A12: w = [x,y] by PRVECT_3:18;
R /. w = R . (x,y) by A12
.= f . (x,y) by A5 ;
then A13: ||.(R /. w).|| <= (K0 * ||.x.||) * ||.y.|| by A1;
A14: ( ||.x.|| <= ||.w.|| & ||.y.|| <= ||.w.|| ) by A12, LOPBAN_7:15;
( 0 <= ||.x.|| & 0 <= ||.y.|| ) by NORMSP_1:4;
then ||.x.|| * ||.y.|| <= ||.w.|| * ||.w.|| by A14, XREAL_1:66;
then K0 * (||.x.|| * ||.y.||) <= K0 * (||.w.|| * ||.w.||) by A1, XREAL_1:64;
then A15: ||.(R /. w).|| <= K0 * (||.w.|| * ||.w.||) by A13, XXREAL_0:2;
A16: 0 < ||.w.|| " by A11, XREAL_1:122;
(||.w.|| ") * (K0 * (||.w.|| * ||.w.||)) = (((||.w.|| ") * ||.w.||) * K0) * ||.w.||
.= (1 * K0) * ||.w.|| by A10, XCMPLX_0:def 7 ;
then A17: (||.w.|| ") * ||.(R /. w).|| <= K0 * ||.w.|| by A15, A16, XREAL_1:64;
K0 + 0 < K0 + 1 by XREAL_1:8;
then A18: K0 * ||.w.|| < (K0 + 1) * ||.w.|| by A11, XREAL_1:68;
(K0 + 1) * ||.w.|| < (K0 + 1) * (r / (K0 + 1)) by A8, A9, XREAL_1:68;
then (K0 + 1) * ||.w.|| < r by A8, XCMPLX_1:87;
then K0 * ||.w.|| < r by A18, XXREAL_0:2;
hence (||.w.|| ") * ||.(R /. w).|| < r by A17, XXREAL_0:2; :: thesis:

end;

then reconsider R = R as RestFunc of [:E,F:],G by NDIFF_1:23;
set N = the Neighbourhood of z;
A19: for w being Point of [:E,F:] st w in the Neighbourhood of z holds
(f /. w) - (f /. z) = (L0 . (w - z)) + (R /. (w - z))

proof

let w be Point of [:E,F:]; :: thesis:
consider w1 being Point of E, w2 being Point of F such that
A20: w = [w1,w2] by PRVECT_3:18;
consider z1 being Point of E, z2 being Point of F such that
A21: z = [z1,z2] by PRVECT_3:18;
set dx = w1 - z1;
set dy = w2 - z2;
A22: w2 = (w2 - z2) + z2 by RLVECT_4:1;
f /. w = f . (((w1 - z1) + z1),((w2 - z2) + z2)) by A20, A22, RLVECT_4:1
.= (f . ((w1 - z1),((w2 - z2) + z2))) + (f . (z1,((w2 - z2) + z2))) by LOPBAN_8:12
.= ((f . ((w1 - z1),(w2 - z2))) + (f . ((w1 - z1),z2))) + (f . (z1,((w2 - z2) + z2))) by LOPBAN_8:12
.= ((f . ((w1 - z1),(w2 - z2))) + (f . ((w1 - z1),z2))) + ((f . (z1,(w2 - z2))) + (f . (z1,z2))) by LOPBAN_8:12
.= (((f . ((w1 - z1),(w2 - z2))) + (f . ((w1 - z1),z2))) + (f . (z1,(w2 - z2)))) + (f . (z1,z2)) by RLVECT_1:def 3 ;
then A24: (f /. w) - (f /. z) = ((f . ((w1 - z1),(w2 - z2))) + (f . ((w1 - z1),z2))) + (f . (z1,(w2 - z2))) by A21, RLVECT_4:1
.= ((f . ((w1 - z1),z2)) + (f . (z1,(w2 - z2)))) + (f . ((w1 - z1),(w2 - z2))) by RLVECT_1:def 3
.= (L . ((w1 - z1),(w2 - z2))) + (f . ((w1 - z1),(w2 - z2))) by A3, A21 ;
AA: - z = [(- z1),(- z2)] by A21, PRVECT_3:18;
then w - z = [(w1 - z1),(w2 - z2)] by A20, PRVECT_3:18;
then R /. (w - z) = R . ((w1 - z1),(w2 - z2)) by A6, PARTFUN1:def 6
.= f . ((w1 - z1),(w2 - z2)) by A5 ;
hence ( w in the Neighbourhood of z implies (f /. w) - (f /. z) = (L0 . (w - z)) + (R /. (w - z)) ) by A24, AA, A20, PRVECT_3:18; :: thesis:

end;

A28: dom f = the carrier of [:E,F:] by FUNCT_2:def 1;
hence f is_differentiable_in z by A19; :: thesis:
then A29: diff (f,z) = L0 by A19, A28, NDIFF_1:def 7;
hence for dx being Point of E
for dy being Point of F holds (diff (f,z)) . (dx,dy) = (f . (dx,(z `2))) + (f . ((z `1),dy)) by A3; :: thesis:
A30: ( ( for s being Real st s in PreNorms L holds
s <= K * ||.z.|| ) implies upper_bound (PreNorms L) <= K * ||.z.|| ) by SEQ_4:45;

A31: now :: thesis:

let t be VECTOR of [:E,F:]; :: thesis:
assume A32: ||.t.|| <= 1 ; :: thesis:
A33: ||.(L . t).|| <= (K * ||.z.||) * ||.t.|| by A4;
0 <= ||.z.|| by NORMSP_1:4;
then 0 <= K * ||.z.|| by A2, XREAL_1:127;
then (K * ||.z.||) * ||.t.|| <= (K * ||.z.||) * 1 by A32, XREAL_1:64;
hence ||.(L . t).|| <= K * ||.z.|| by A33, XXREAL_0:2; :: thesis:

end;

now :: thesis:

let r be Real; :: thesis:
assume r in PreNorms L ; :: thesis:
then ex t being VECTOR of [:E,F:] st
( r = ||.(L . t).|| & ||.t.|| <= 1 ) ;
hence r <= K * ||.z.|| by A31; :: thesis:

end;

hence ||.(diff (f,z)).|| <= K * ||.z.|| by A29, A30, LOPBAN_1:30; :: thesis: