lopban_8.miz



    begin

    reserve S,T,W,Y for RealNormSpace;

    reserve f,f1,f2 for PartFunc of S, T;

    reserve Z for Subset of S;

    reserve i,n for Nat;

    theorem :: LOPBAN_8:1

    

     Th020: for E,F be RealNormSpace, E1 be Subset of E, f be PartFunc of E, F st E1 is dense & F is complete & ( dom f) = E1 & f is_uniformly_continuous_on E1 holds (ex g be Function of E, F st (g | E1) = f & g is_uniformly_continuous_on the carrier of E & (for x be Point of E holds ex seq be sequence of E st ( rng seq) c= E1 & seq is convergent & ( lim seq) = x & (f /* seq) is convergent & (g . x) = ( lim (f /* seq))) & (for x be Point of E, seq be sequence of E st ( rng seq) c= E1 & seq is convergent & ( lim seq) = x holds (f /* seq) is convergent & (g . x) = ( lim (f /* seq)))) & (for g1,g2 be Function of E, F st (g1 | E1) = f & g1 is_continuous_on the carrier of E & (g2 | E1) = f & g2 is_continuous_on the carrier of E holds g1 = g2)

    proof

      let E,F be RealNormSpace, E1 be Subset of E, f be PartFunc of E, F;

      assume that

       A1: E1 is dense and

       A2: F is complete and

       A3: ( dom f) = E1 and

       A4: f is_uniformly_continuous_on E1;

      

       A6: for x be Point of E, seq be sequence of E st ( rng seq) c= E1 & seq is convergent holds for s be Real st 0 < s holds ex n be Nat st for m be Nat st n <= m holds ||.(((f /* seq) . m) - ((f /* seq) . n)).|| < s

      proof

        let x be Point of E, seq be sequence of E;

        assume that

         A7: ( rng seq) c= E1 and

         A8: seq is convergent;

        set fseq = (f /* seq);

        let r be Real;

        assume 0 < r;

        then

        consider s be Real such that

         A10: 0 < s & for x1,x2 be Point of E st x1 in E1 & x2 in E1 & ||.(x1 - x2).|| < s holds ||.((f /. x1) - (f /. x2)).|| < r by A4, NFCONT_2:def 1;

        consider n be Nat such that

         A11: for m be Nat st n <= m holds ||.((seq . m) - (seq . n)).|| < s by A8, A10, LOPBAN_3: 4;

        take n;

        let m be Nat;

        assume n <= m;

        then

         A13: ||.((seq . m) - (seq . n)).|| < s by A11;

        

         A14: n in NAT & m in NAT by ORDINAL1:def 12;

        

         B14: (seq . m) in ( rng seq) & (seq . n) in ( rng seq) by FUNCT_2: 4, ORDINAL1:def 12;

        (f /. (seq . m)) = (fseq . m) & (f /. (seq . n)) = (fseq . n) by A3, A7, A14, FUNCT_2: 109;

        hence ||.((fseq . m) - (fseq . n)).|| < r by A7, A10, A13, B14;

      end;

      

       A16: for x be Point of E, seq be sequence of E st ( rng seq) c= E1 & seq is convergent holds (f /* seq) is convergent

      proof

        let x be Point of E, seq be sequence of E;

        assume that

         A17: ( rng seq) c= E1 and

         A18: seq is convergent;

        for s be Real st 0 < s holds ex n be Nat st for m be Nat st n <= m holds ||.(((f /* seq) . m) - ((f /* seq) . n)).|| < s by A6, A17, A18;

        hence thesis by A2, LOPBAN_1:def 15, LOPBAN_3: 5;

      end;

      

       A19: for x be Point of E, seq1,seq2 be sequence of E st ( rng seq1) c= E1 & seq1 is convergent & ( lim seq1) = x & ( rng seq2) c= E1 & seq2 is convergent & ( lim seq2) = x holds ( lim (f /* seq1)) = ( lim (f /* seq2))

      proof

        let x be Point of E, seq1,seq2 be sequence of E;

        assume that

         A20: ( rng seq1) c= E1 & seq1 is convergent & ( lim seq1) = x and

         A21: ( rng seq2) c= E1 & seq2 is convergent & ( lim seq2) = x;

        deffunc F2( Nat) = (seq1 . $1);

        deffunc F3( Nat) = (seq2 . $1);

        consider s be sequence of the carrier of E such that

         A22: for n be Nat holds (s . (2 * n)) = F2(n) & (s . ((2 * n) + 1)) = F3(n) from INTEGR20:sch 1;

         B23:

        now

          let y be object;

          assume y in ( rng s);

          then

          consider i be object such that

           A23: i in NAT & y = (s . i) by FUNCT_2: 11;

          reconsider i as Nat by A23;

          consider k be Nat such that

           A24: i = (2 * k) or i = ((2 * k) + 1) by INTEGR20: 14;

          reconsider k1 = k, i1 = i as Element of NAT by ORDINAL1:def 12;

          per cases by A24;

            suppose i = (2 * k1);

            then (s . i) = (seq1 . k1) by A22;

            then (s . i) in ( rng seq1) by FUNCT_2: 4;

            hence y in E1 by A20, A23;

          end;

            suppose i = ((2 * k1) + 1);

            then (s . i) = (seq2 . k1) by A22;

            then (s . i) in ( rng seq2) by FUNCT_2: 4;

            hence y in E1 by A21, A23;

          end;

        end;

        then

         A28: ( rng s) c= E1 by TARSKI:def 3;

        now

          let p be Real;

          assume

           A30: 0 < p;

          then

          consider n1 be Nat such that

           A31: for m be Nat st n1 <= m holds ||.((seq1 . m) - x).|| < p by A20, NORMSP_1:def 7;

          consider n2 be Nat such that

           A32: for m be Nat st n2 <= m holds ||.((seq2 . m) - x).|| < p by A21, A30, NORMSP_1:def 7;

          reconsider n3 = ( max (n1,n2)) as Nat by TARSKI: 1;

          

           A33: n1 <= n3 & n2 <= n3 by XXREAL_0: 25;

          reconsider n = ((2 * n3) + 1) as Nat;

          take n;

          let m be Nat;

          assume

           A34: n <= m;

          consider k be Nat such that

           A35: m = (2 * k) or m = ((2 * k) + 1) by INTEGR20: 14;

          reconsider k1 = k, m1 = m as Element of NAT by ORDINAL1:def 12;

          per cases by A35;

            suppose

             A36: m = (2 * k1);

            then

             A37: (s . m) = (seq1 . k1) by A22;

            

             A38: (2 * n3) <= ((2 * k) - 1) by A34, A36, XREAL_1: 19;

            ((2 * k) - 1) < (((2 * k) - 1) + 1) by XREAL_1: 145;

            then (2 * n3) <= (2 * k) by A38, XXREAL_0: 2;

            then ((2 * n3) / 2) <= ((2 * k) / 2) by XREAL_1: 72;

            then n1 <= k by A33, XXREAL_0: 2;

            hence ||.((s . m) - x).|| < p by A31, A37;

          end;

            suppose

             A39: m = ((2 * k) + 1);

            then

             A40: (s . m1) = (seq2 . k1) by A22;

            (((2 * n3) + 1) - 1) <= (((2 * k) + 1) - 1) by A34, A39, XREAL_1: 13;

            then ((2 * n3) / 2) <= ((2 * k) / 2) by XREAL_1: 72;

            then n2 <= k by A33, XXREAL_0: 2;

            hence ||.((s . m) - x).|| < p by A32, A40;

          end;

        end;

        then

         A42: (f /* s) is convergent by A16, A28, NORMSP_1:def 6;

        for i be Nat holds ((f /* s) . (2 * i)) = ((f /* seq1) . i) & ((f /* s) . ((2 * i) + 1)) = ((f /* seq2) . i)

        proof

          let i be Nat;

          

           A43: i in NAT by ORDINAL1:def 12;

          (2 * i) in NAT by ORDINAL1:def 12;

          

          hence ((f /* s) . (2 * i)) = (f /. (s . (2 * i))) by A3, B23, FUNCT_2: 109, TARSKI:def 3

          .= (f /. (seq1 . i)) by A22

          .= ((f /* seq1) . i) by A3, A20, A43, FUNCT_2: 109;

          

          thus ((f /* s) . ((2 * i) + 1)) = (f /. (s . ((2 * i) + 1))) by A3, B23, FUNCT_2: 109, TARSKI:def 3

          .= (f /. (seq2 . i)) by A22

          .= ((f /* seq2) . i) by A3, A21, A43, FUNCT_2: 109;

        end;

        then ( lim (f /* seq1)) = ( lim (f /* s)) & ( lim (f /* seq2)) = ( lim (f /* s)) by A42, INTEGR20: 18;

        hence thesis;

      end;

      defpred P1[ object, object] means ex seq be sequence of E st ( rng seq) c= E1 & seq is convergent & ( lim seq) = $1 & (f /* seq) is convergent & $2 = ( lim (f /* seq));

      

       A46: for x be Element of E holds ex y be Element of F st P1[x, y]

      proof

        let x be Element of E;

        consider seq be sequence of E such that

         A47: ( rng seq) c= E1 & seq is convergent & ( lim seq) = x by A1, NORMSP_3: 14;

        take y = ( lim (f /* seq));

        thus thesis by A16, A47;

      end;

      consider g be Function of E, F such that

       A49: for x be Element of E holds P1[x, (g . x)] from FUNCT_2:sch 3( A46);

      

       A50: ( dom g) = the carrier of E by FUNCT_2:def 1;

      

       A51: ( dom f) = (the carrier of E /\ E1) by A3, XBOOLE_1: 28

      .= (( dom g) /\ E1) by FUNCT_2:def 1;

      

       A52: f is_continuous_on E1 by A4, NFCONT_2: 7;

      for x be object st x in ( dom f) holds (f . x) = (g . x)

      proof

        let x0 be object;

        assume

         A53: x0 in ( dom f);

        then

         A54: x0 in ( dom g) & x0 in E1 by A51, XBOOLE_0:def 4;

        reconsider x = x0 as Point of E by A53;

        reconsider seq1 = ( NAT --> x) as sequence of E;

        for n be Nat holds (seq1 . n) = x by FUNCOP_1: 7, ORDINAL1:def 12;

        then

         A56: seq1 is convergent & ( lim seq1) = x by NORMSP_3: 23;

        

         A58: ( rng seq1) c= E1

        proof

          let y be object;

          assume y in ( rng seq1);

          then

          consider i be object such that

           A57: i in NAT & y = (seq1 . i) by FUNCT_2: 11;

          reconsider i as Nat by A57;

          thus y in E1 by A54, A57, FUNCOP_1: 7;

        end;

        then (f /* seq1) is convergent & ( lim (f /* seq1)) = (f /. ( lim seq1)) by A52, A54, A56, NFCONT_1: 18;

        then

         A59: ( lim (f /* seq1)) = (f . x) by A53, A56, PARTFUN1:def 6;

        consider seq2 be sequence of E such that

         A60: ( rng seq2) c= E1 & seq2 is convergent & ( lim seq2) = x & (f /* seq2) is convergent & (g . x) = ( lim (f /* seq2)) by A49;

        thus thesis by A19, A56, A58, A59, A60;

      end;

      then

       A61: (g | E1) = f by A51, FUNCT_1: 46;

      

       A62: for x be Point of E, seq be sequence of E st ( rng seq) c= E1 & seq is convergent & ( lim seq) = x holds (f /* seq) is convergent & (g . x) = ( lim (f /* seq))

      proof

        let x be Point of E, seq be sequence of E;

        assume

         A63: ( rng seq) c= E1 & seq is convergent & ( lim seq) = x;

        consider seq1 be sequence of E such that

         A64: ( rng seq1) c= E1 & seq1 is convergent & ( lim seq1) = x & (f /* seq1) is convergent & (g . x) = ( lim (f /* seq1)) by A49;

        thus (f /* seq) is convergent by A16, A63;

        thus thesis by A19, A63, A64;

      end;

      for r be Real st 0 < r holds ex s be Real st 0 < s & for x1,x2 be Point of E st x1 in the carrier of E & x2 in the carrier of E & ||.(x1 - x2).|| < s holds ||.((g /. x1) - (g /. x2)).|| < r

      proof

        let r0 be Real;

        assume

         A65: 0 < r0;

        set r1 = (r0 / 2);

        

         A66: 0 < r1 & r1 < r0 by A65, XREAL_1: 215, XREAL_1: 216;

        set r = (r1 / 3);

        

         A67: 0 < r & r < r1 by A66, XREAL_1: 221, XREAL_1: 222;

        consider s0 be Real such that

         A68: 0 < s0 & for x1,x2 be Point of E st x1 in E1 & x2 in E1 & ||.(x1 - x2).|| < s0 holds ||.((f /. x1) - (f /. x2)).|| < r by A4, A66, NFCONT_2:def 1, XREAL_1: 222;

        set s = (s0 / 3);

        

         A69: 0 < s & s < s0 by A68, XREAL_1: 221, XREAL_1: 222;

        take s;

        thus 0 < s by A68, XREAL_1: 222;

        let x1,x2 be Point of E;

        assume

         A70: x1 in the carrier of E & x2 in the carrier of E & ||.(x1 - x2).|| < s;

        consider seq1 be sequence of E such that

         A71: ( rng seq1) c= E1 & seq1 is convergent & ( lim seq1) = x1 & (f /* seq1) is convergent & (g . x1) = ( lim (f /* seq1)) by A49;

        consider M10 be Nat such that

         A72: for n be Nat st M10 <= n holds ||.((seq1 . n) - x1).|| < s by A69, A71, NORMSP_1:def 7;

        consider M11 be Nat such that

         A73: for n be Nat st M11 <= n holds ||.(((f /* seq1) . n) - (g . x1)).|| < r by A67, A71, NORMSP_1:def 7;

        set M1 = (M10 + M11);

        

         A74: (M10 + 0 ) <= M1 & (M11 + 0 ) <= M1 by XREAL_1: 7;

        consider seq2 be sequence of E such that

         A75: ( rng seq2) c= E1 & seq2 is convergent & ( lim seq2) = x2 & (f /* seq2) is convergent & (g . x2) = ( lim (f /* seq2)) by A49;

        consider M20 be Nat such that

         A76: for n be Nat st M20 <= n holds ||.((seq2 . n) - x2).|| < s by A69, A75, NORMSP_1:def 7;

        consider M21 be Nat such that

         A77: for n be Nat st M21 <= n holds ||.(((f /* seq2) . n) - (g . x2)).|| < r by A67, A75, NORMSP_1:def 7;

        set M2 = (M20 + M21);

        

         A78: (M20 + 0 ) <= M2 & (M21 + 0 ) <= M2 by XREAL_1: 7;

        set n = (M1 + M2);

        

         A82: ||.((seq1 . n) - x1).|| < s & ||.(((f /* seq1) . n) - (g . x1)).|| < r by A72, A73, A74, XREAL_1: 7;

        

         A83: ||.((seq2 . n) - x2).|| < s & ||.(((f /* seq2) . n) - (g . x2)).|| < r by A76, A77, A78, XREAL_1: 7;

        ((seq2 . n) - (seq1 . n)) = ((((seq2 . n) - x2) + x2) - (seq1 . n)) by RLVECT_4: 1

        .= ((((seq2 . n) - x2) + ((x2 - x1) + x1)) - (seq1 . n)) by RLVECT_4: 1

        .= (((((seq2 . n) - x2) + (x2 - x1)) + x1) - (seq1 . n)) by RLVECT_1:def 3

        .= ((((seq2 . n) - x2) + (x2 - x1)) + (x1 - (seq1 . n))) by RLVECT_1: 28;

        then

         A84: ||.((seq2 . n) - (seq1 . n)).|| <= ( ||.(((seq2 . n) - x2) + (x2 - x1)).|| + ||.(x1 - (seq1 . n)).||) by NORMSP_1:def 1;

         ||.(((seq2 . n) - x2) + (x2 - x1)).|| <= ( ||.((seq2 . n) - x2).|| + ||.(x2 - x1).||) by NORMSP_1:def 1;

        then ( ||.(((seq2 . n) - x2) + (x2 - x1)).|| + ||.(x1 - (seq1 . n)).||) <= (( ||.((seq2 . n) - x2).|| + ||.(x2 - x1).||) + ||.(x1 - (seq1 . n)).||) by XREAL_1: 7;

        then

         A85: ||.((seq2 . n) - (seq1 . n)).|| <= (( ||.((seq2 . n) - x2).|| + ||.(x2 - x1).||) + ||.(x1 - (seq1 . n)).||) by A84, XXREAL_0: 2;

         ||.(x2 - x1).|| < s by A70, NORMSP_1: 7;

        then

         A86: ( ||.((seq2 . n) - x2).|| + ||.(x2 - x1).||) < (s + s) by A83, XREAL_1: 8;

         ||.(x1 - (seq1 . n)).|| < s by A82, NORMSP_1: 7;

        then (( ||.((seq2 . n) - x2).|| + ||.(x2 - x1).||) + ||.(x1 - (seq1 . n)).||) < ((s + s) + s) by A86, XREAL_1: 8;

        then ||.((seq2 . n) - (seq1 . n)).|| < ((s + s) + s) by A85, XXREAL_0: 2;

        then

         A87: ||.((seq1 . n) - (seq2 . n)).|| < ((s + s) + s) by NORMSP_1: 7;

        

         A88: n in NAT by ORDINAL1:def 12;

        (seq2 . n) in ( rng seq2) & (seq1 . n) in ( rng seq1) by FUNCT_2: 4, ORDINAL1:def 12;

        then

         A89: ||.((f /. (seq1 . n)) - (f /. (seq2 . n))).|| < r by A68, A71, A75, A87;

        ((g /. x1) - (g /. x2)) = ((((g /. x1) - (f /. (seq1 . n))) + (f /. (seq1 . n))) - (g /. x2)) by RLVECT_4: 1

        .= ((((g /. x1) - (f /. (seq1 . n))) + (((f /. (seq1 . n)) - (f /. (seq2 . n))) + (f /. (seq2 . n)))) - (g /. x2)) by RLVECT_4: 1

        .= (((((g /. x1) - (f /. (seq1 . n))) + ((f /. (seq1 . n)) - (f /. (seq2 . n)))) + (f /. (seq2 . n))) - (g /. x2)) by RLVECT_1:def 3

        .= ((((g /. x1) - (f /. (seq1 . n))) + ((f /. (seq1 . n)) - (f /. (seq2 . n)))) + ((f /. (seq2 . n)) - (g /. x2))) by RLVECT_1: 28;

        then

         A90: ||.((g /. x1) - (g /. x2)).|| <= ( ||.(((g /. x1) - (f /. (seq1 . n))) + ((f /. (seq1 . n)) - (f /. (seq2 . n)))).|| + ||.((f /. (seq2 . n)) - (g /. x2)).||) by NORMSP_1:def 1;

         ||.(((g /. x1) - (f /. (seq1 . n))) + ((f /. (seq1 . n)) - (f /. (seq2 . n)))).|| <= ( ||.((g /. x1) - (f /. (seq1 . n))).|| + ||.((f /. (seq1 . n)) - (f /. (seq2 . n))).||) by NORMSP_1:def 1;

        then ( ||.(((g /. x1) - (f /. (seq1 . n))) + ((f /. (seq1 . n)) - (f /. (seq2 . n)))).|| + ||.((f /. (seq2 . n)) - (g /. x2)).||) <= (( ||.((g /. x1) - (f /. (seq1 . n))).|| + ||.((f /. (seq1 . n)) - (f /. (seq2 . n))).||) + ||.((f /. (seq2 . n)) - (g /. x2)).||) by XREAL_1: 7;

        then

         A91: ||.((g /. x1) - (g /. x2)).|| <= (( ||.((g /. x1) - (f /. (seq1 . n))).|| + ||.((f /. (seq1 . n)) - (f /. (seq2 . n))).||) + ||.((f /. (seq2 . n)) - (g /. x2)).||) by A90, XXREAL_0: 2;

        

         A92: ||.((g /. x1) - (f /. (seq1 . n))).|| = ||.((f /. (seq1 . n)) - (g . x1)).|| by NORMSP_1: 7

        .= ||.(((f /* seq1) . n) - (g . x1)).|| by A3, A71, A88, FUNCT_2: 109;

        

         A93: ||.((f /. (seq2 . n)) - (g /. x2)).|| = ||.(((f /* seq2) . n) - (g . x2)).|| by A3, A75, A88, FUNCT_2: 109;

        ( ||.((g /. x1) - (f /. (seq1 . n))).|| + ||.((f /. (seq1 . n)) - (f /. (seq2 . n))).||) <= (r + r) by A82, A89, A92, XREAL_1: 7;

        then (( ||.((g /. x1) - (f /. (seq1 . n))).|| + ||.((f /. (seq1 . n)) - (f /. (seq2 . n))).||) + ||.((f /. (seq2 . n)) - (g /. x2)).||) < ((r + r) + r) by A83, A93, XREAL_1: 8;

        then ||.((g /. x1) - (g /. x2)).|| < ((r + r) + r) by A91, XXREAL_0: 2;

        hence ||.((g /. x1) - (g /. x2)).|| < r0 by A66, XXREAL_0: 2;

      end;

      hence ex g be Function of E, F st (g | E1) = f & g is_uniformly_continuous_on the carrier of E & (for x be Point of E holds ex seq be sequence of E st ( rng seq) c= E1 & seq is convergent & ( lim seq) = x & (f /* seq) is convergent & (g . x) = ( lim (f /* seq))) & (for x be Point of E, seq be sequence of E st ( rng seq) c= E1 & seq is convergent & ( lim seq) = x holds (f /* seq) is convergent & (g . x) = ( lim (f /* seq))) by A49, A50, A61, A62, NFCONT_2:def 1;

      let g1,g2 be Function of E, F such that

       A95: (g1 | E1) = f & g1 is_continuous_on the carrier of E and

       A96: (g2 | E1) = f & g2 is_continuous_on the carrier of E;

      for x be Element of E holds (g1 . x) = (g2 . x)

      proof

        let x be Element of E;

        consider seq be sequence of E such that

         A97: ( rng seq) c= E1 & seq is convergent & ( lim seq) = x by A1, NORMSP_3: 14;

        

         A106: (g1 /* seq) = (f /* seq) by A3, A95, A97, FUNCT_2: 117

        .= (g2 /* seq) by A3, A96, A97, FUNCT_2: 117;

        

        thus (g1 . x) = (g1 /. ( lim seq)) by A97

        .= ( lim (g2 /* seq)) by A95, A97, A106, NFCONT_1: 18

        .= (g2 /. x) by A96, A97, NFCONT_1: 18

        .= (g2 . x);

      end;

      hence g1 = g2 by FUNCT_2:def 8;

    end;

    theorem :: LOPBAN_8:2

    for E,F,G be RealNormSpace, f be Point of ( R_NormSpace_of_BoundedLinearOperators (E,F)), g be Point of ( R_NormSpace_of_BoundedLinearOperators (F,G)) holds ex h be Point of ( R_NormSpace_of_BoundedLinearOperators (E,G)) st h = (g * f) & ||.h.|| <= ( ||.g.|| * ||.f.||)

    proof

      let E,F,G be RealNormSpace, f be Point of ( R_NormSpace_of_BoundedLinearOperators (E,F)), g be Point of ( R_NormSpace_of_BoundedLinearOperators (F,G));

      reconsider Lf = f as Lipschitzian LinearOperator of E, F by LOPBAN_1:def 9;

      reconsider Lg = g as Lipschitzian LinearOperator of F, G by LOPBAN_1:def 9;

      set Lh = (Lg * Lf);

      reconsider Lh as Lipschitzian LinearOperator of E, G by LOPBAN_2: 2;

      reconsider h = Lh as Point of ( R_NormSpace_of_BoundedLinearOperators (E,G)) by LOPBAN_1:def 9;

      take h;

      thus h = (g * f);

      

       A8: ||.h.|| = ( upper_bound ( PreNorms ( modetrans (h,E,G)))) by LOPBAN_1:def 13

      .= ( upper_bound ( PreNorms Lh)) by LOPBAN_1: 29;

      for t be Real st t in ( PreNorms Lh) holds t <= ( ||.g.|| * ||.f.||)

      proof

        let t be Real;

        assume t in ( PreNorms Lh);

        then

        consider w be Point of E such that

         A9: t = ||.(Lh . w).|| & ||.w.|| <= 1;

        

         A10: ||.(Lh . w).|| = ||.(Lg . (Lf . w)).|| by FUNCT_2: 15;

        

         A11: ||.(Lf . w).|| <= ( ||.f.|| * ||.w.||) by LOPBAN_1: 32;

        ( ||.f.|| * ||.w.||) <= ( ||.f.|| * 1) by A9, XREAL_1: 64;

        then

         A12: ||.(Lf . w).|| <= ||.f.|| by A11, XXREAL_0: 2;

        

         A13: ||.(Lg . (Lf . w)).|| <= ( ||.g.|| * ||.(Lf . w).||) by LOPBAN_1: 32;

        ( ||.g.|| * ||.(Lf . w).||) <= ( ||.g.|| * ||.f.||) by A12, XREAL_1: 64;

        hence thesis by A9, A10, A13, XXREAL_0: 2;

      end;

      hence ||.h.|| <= ( ||.g.|| * ||.f.||) by A8, SEQ_4: 45;

    end;

    theorem :: LOPBAN_8:3

    

     LMCONT1: for E,F be RealNormSpace, L be Lipschitzian LinearOperator of E, F holds L is_Lipschitzian_on the carrier of E & L is_uniformly_continuous_on the carrier of E

    proof

      let E,F be RealNormSpace, L be Lipschitzian LinearOperator of E, F;

      consider K be Real such that

       A2: 0 <= K & for x be VECTOR of E holds ||.(L . x).|| <= (K * ||.x.||) by LOPBAN_1:def 8;

      set r = (K + 1);

      

       A3: (K + 0 ) < r by XREAL_1: 8;

      set E0 = the carrier of E;

      for x1,x2 be Point of E st x1 in E0 & x2 in E0 holds ||.((L /. x1) - (L /. x2)).|| <= (r * ||.(x1 - x2).||)

      proof

        let x1,x2 be Point of E;

        ((L /. x1) - (L /. x2)) = ((L . x1) + (( - 1) * (L . x2))) by RLVECT_1: 16

        .= ((L . x1) + (L . (( - 1) * x2))) by LOPBAN_1:def 5

        .= (L . (x1 + (( - 1) * x2))) by VECTSP_1:def 20

        .= (L . (x1 - x2)) by RLVECT_1: 16;

        then

         A8: ||.((L /. x1) - (L /. x2)).|| <= (K * ||.(x1 - x2).||) by A2;

        (K * ||.(x1 - x2).||) <= (r * ||.(x1 - x2).||) by A3, XREAL_1: 64;

        hence thesis by A8, XXREAL_0: 2;

      end;

      hence L is_Lipschitzian_on E0 by A2, FUNCT_2:def 1;

      hence L is_uniformly_continuous_on E0 by NFCONT_2: 9;

    end;

    theorem :: LOPBAN_8:4

    for E,F be RealNormSpace, E1 be SubRealNormSpace of E, f be Point of ( R_NormSpace_of_BoundedLinearOperators (E1,F)) st F is complete & ex E0 be Subset of E st E0 = the carrier of E1 & E0 is dense holds (ex g be Point of ( R_NormSpace_of_BoundedLinearOperators (E,F)) st ( dom g) = the carrier of E & (g | the carrier of E1) = f & ||.g.|| = ||.f.|| & ex Lf be PartFunc of E, F st Lf = f & (for x be Point of E holds ex seq be sequence of E st ( rng seq) c= the carrier of E1 & seq is convergent & ( lim seq) = x & (Lf /* seq) is convergent & (g . x) = ( lim (Lf /* seq))) & (for x be Point of E, seq be sequence of E st ( rng seq) c= the carrier of E1 & seq is convergent & ( lim seq) = x holds (Lf /* seq) is convergent & (g . x) = ( lim (Lf /* seq)))) & (for g1,g2 be Point of ( R_NormSpace_of_BoundedLinearOperators (E,F)) st (g1 | the carrier of E1) = f & (g2 | the carrier of E1) = f holds g1 = g2)

    proof

      let E,F be RealNormSpace, E1 be SubRealNormSpace of E, f be Point of ( R_NormSpace_of_BoundedLinearOperators (E1,F));

      assume that

       A1: F is complete and

       A2: ex E0 be Subset of E st E0 = the carrier of E1 & E0 is dense;

      consider E0 be Subset of E such that

       A3: E0 = the carrier of E1 & E0 is dense by A2;

      reconsider L = f as Lipschitzian LinearOperator of E1, F by LOPBAN_1:def 9;

      

       A4: ( dom L) = the carrier of E1 & ( rng L) c= the carrier of F by FUNCT_2:def 1;

      then L in ( PFuncs (the carrier of E,the carrier of F)) by A3, PARTFUN1:def 3;

      then

      reconsider Lf = L as PartFunc of E, F by PARTFUN1: 46;

      

       A5: ( dom Lf) = E0 by A3, FUNCT_2:def 1;

      consider K be Real such that

       A6: 0 <= K & for x be VECTOR of E1 holds ||.(L . x).|| <= (K * ||.x.||) by LOPBAN_1:def 8;

      set r = (K + 1);

      

       A7: (K + 0 ) < r by XREAL_1: 8;

      for x1,x2 be Point of E st x1 in E0 & x2 in E0 holds ||.((Lf /. x1) - (Lf /. x2)).|| <= (r * ||.(x1 - x2).||)

      proof

        let x1,x2 be Point of E;

        assume x1 in E0 & x2 in E0;

        then

        reconsider xx1 = x1, xx2 = x2 as Point of E1 by A3;

        

         A10: (( - 1) * x2) = (( - 1) * xx2) by NORMSP_3: 28;

        

         A11: (x1 - x2) = (x1 + (( - 1) * x2)) by RLVECT_1: 16

        .= (xx1 + (( - 1) * xx2)) by A10, NORMSP_3: 28

        .= (xx1 - xx2) by RLVECT_1: 16;

        

         A12: (Lf /. x1) = (L . xx1) by A4, PARTFUN1:def 6;

        (Lf /. x2) = (L . xx2) by A4, PARTFUN1:def 6;

        

        then ((Lf /. x1) - (Lf /. x2)) = ((L . xx1) + (( - 1) * (L . xx2))) by A12, RLVECT_1: 16

        .= ((L . xx1) + (L . (( - 1) * xx2))) by LOPBAN_1:def 5

        .= (L . (xx1 + (( - 1) * xx2))) by VECTSP_1:def 20

        .= (L . (xx1 - xx2)) by RLVECT_1: 16;

        then ||.((Lf /. x1) - (Lf /. x2)).|| <= (K * ||.(xx1 - xx2).||) by A6;

        then

         A14: ||.((Lf /. x1) - (Lf /. x2)).|| <= (K * ||.(x1 - x2).||) by A11, NORMSP_3: 28;

        (K * ||.(x1 - x2).||) <= (r * ||.(x1 - x2).||) by A7, XREAL_1: 64;

        hence thesis by A14, XXREAL_0: 2;

      end;

      then Lf is_Lipschitzian_on E0 by A3, A6, FUNCT_2:def 1;

      then

       A15: Lf is_uniformly_continuous_on E0 by NFCONT_2: 9;

      

       A16: (ex Pg be Function of E, F st (Pg | E0) = Lf & Pg is_uniformly_continuous_on the carrier of E & (for x be Point of E holds ex seq be sequence of E st ( rng seq) c= E0 & seq is convergent & ( lim seq) = x & (Lf /* seq) is convergent & (Pg . x) = ( lim (Lf /* seq))) & (for x be Point of E, seq be sequence of E st ( rng seq) c= E0 & seq is convergent & ( lim seq) = x holds (Lf /* seq) is convergent & (Pg . x) = ( lim (Lf /* seq)))) & (for Pg1,Pg2 be Function of E, F st (Pg1 | E0) = Lf & Pg1 is_continuous_on the carrier of E & (Pg2 | E0) = Lf & Pg2 is_continuous_on the carrier of E holds Pg1 = Pg2) by A1, A3, A5, A15, Th020;

      consider Pg be Function of E, F such that

       A17: (Pg | E0) = Lf and

       A18: Pg is_uniformly_continuous_on the carrier of E and

       A19: for x be Point of E holds ex seq be sequence of E st ( rng seq) c= E0 & seq is convergent & ( lim seq) = x & (Lf /* seq) is convergent & (Pg . x) = ( lim (Lf /* seq)) and

       A20: for x be Point of E, seq be sequence of E st ( rng seq) c= E0 & seq is convergent & ( lim seq) = x holds (Lf /* seq) is convergent & (Pg . x) = ( lim (Lf /* seq)) and

       A21: for x be Point of E holds ex seq be sequence of E st ( rng seq) c= E0 & seq is convergent & ( lim seq) = x & (Lf /* seq) is convergent & (Pg . x) = ( lim (Lf /* seq)) and

       A22: for x be Point of E, seq be sequence of E st ( rng seq) c= E0 & seq is convergent & ( lim seq) = x holds (Lf /* seq) is convergent & (Pg . x) = ( lim (Lf /* seq)) by A16;

      

       A23: for x,y be Point of E holds (Pg . (x + y)) = ((Pg . x) + (Pg . y))

      proof

        let x,y be Point of E;

        consider xseq be sequence of E such that

         A24: ( rng xseq) c= E0 & xseq is convergent & ( lim xseq) = x & (Lf /* xseq) is convergent & (Pg . x) = ( lim (Lf /* xseq)) by A19;

        consider yseq be sequence of E such that

         A25: ( rng yseq) c= E0 & yseq is convergent & ( lim yseq) = y & (Lf /* yseq) is convergent & (Pg . y) = ( lim (Lf /* yseq)) by A19;

        

         A29: ( rng (xseq + yseq)) c= E0

        proof

          let y be object;

          assume y in ( rng (xseq + yseq));

          then

          consider n be Element of NAT such that

           A26: y = ((xseq + yseq) . n) by FUNCT_2: 113;

          (xseq . n) in ( rng xseq) & (yseq . n) in ( rng yseq) by FUNCT_2: 4;

          then

          reconsider xn = (xseq . n), yn = (yseq . n) as Point of E1 by A3, A24, A25;

          ((xseq . n) + (yseq . n)) = (xn + yn) by NORMSP_3: 28;

          then ((xseq . n) + (yseq . n)) in E0 by A3;

          hence y in E0 by A26, NORMSP_1:def 2;

        end;

        

         A30: (xseq + yseq) is convergent by A24, A25, NORMSP_1: 19;

        

         A31: ( lim (xseq + yseq)) = (x + y) by A24, A25, NORMSP_1: 25;

        

         A32: ( rng (xseq + yseq)) c= ( dom Lf) by A3, A29, FUNCT_2:def 1;

        

         A33: ( rng xseq) c= ( dom Lf) by A3, A24, FUNCT_2:def 1;

        

         A34: ( rng yseq) c= ( dom Lf) by A3, A25, FUNCT_2:def 1;

        

         B34: for n be Nat holds ((Lf /* (xseq + yseq)) . n) = (((Lf /* xseq) . n) + ((Lf /* yseq) . n))

        proof

          let n be Nat;

          

           A35: n in NAT by ORDINAL1:def 12;

          (xseq . n) in ( rng xseq) & (yseq . n) in ( rng yseq) by FUNCT_2: 4, ORDINAL1:def 12;

          then

          reconsider xn = (xseq . n), yn = (yseq . n) as Point of E1 by A3, A24, A25;

          

           A37: ((xseq . n) + (yseq . n)) = (xn + yn) by NORMSP_3: 28;

          then ((xseq . n) + (yseq . n)) in the carrier of E1;

          then

           A39: ((xseq . n) + (yseq . n)) in ( dom L) by FUNCT_2:def 1;

          

          thus ((Lf /* (xseq + yseq)) . n) = (Lf /. ((xseq + yseq) . n)) by A32, A35, FUNCT_2: 109

          .= (Lf /. ((xseq . n) + (yseq . n))) by NORMSP_1:def 2

          .= (L . (xn + yn)) by A37, A39, PARTFUN1:def 6

          .= ((L /. xn) + (L /. yn)) by VECTSP_1:def 20

          .= (((Lf /* xseq) . n) + (Lf /. (yseq . n))) by A33, A35, FUNCT_2: 109

          .= (((Lf /* xseq) . n) + ((Lf /* yseq) . n)) by A34, A35, FUNCT_2: 109;

        end;

        

         A41: ( lim (Lf /* (xseq + yseq))) = ( lim ((Lf /* xseq) + (Lf /* yseq))) by B34, NORMSP_1:def 2

        .= (( lim (Lf /* xseq)) + ( lim (Lf /* yseq))) by A24, A25, NORMSP_1: 25;

        thus (Pg . (x + y)) = ((Pg . x) + (Pg . y)) by A20, A24, A25, A29, A30, A31, A41;

      end;

      for x be Point of E, a be Real holds (Pg . (a * x)) = (a * (Pg . x))

      proof

        let x be Point of E, a be Real;

        consider xseq be sequence of E such that

         A42: ( rng xseq) c= E0 & xseq is convergent & ( lim xseq) = x & (Lf /* xseq) is convergent & (Pg . x) = ( lim (Lf /* xseq)) by A19;

        

         A46: ( rng (a * xseq)) c= E0

        proof

          let y be object;

          assume y in ( rng (a * xseq));

          then

          consider n be Element of NAT such that

           A43: y = ((a * xseq) . n) by FUNCT_2: 113;

          (xseq . n) in ( rng xseq) by FUNCT_2: 4;

          then

          reconsider xn = (xseq . n) as Point of E1 by A3, A42;

          (a * (xseq . n)) = (a * xn) by NORMSP_3: 28;

          then (a * (xseq . n)) in E0 by A3;

          hence y in E0 by A43, NORMSP_1:def 5;

        end;

        

         A47: (a * xseq) is convergent by A42, NORMSP_1: 22;

        

         A48: ( lim (a * xseq)) = (a * x) by A42, NORMSP_1: 28;

        

         A49: ( rng (a * xseq)) c= ( dom Lf) by A3, A46, FUNCT_2:def 1;

        

         A50: ( rng xseq) c= ( dom Lf) by A3, A42, FUNCT_2:def 1;

        

         B50: for n be Nat holds ((Lf /* (a * xseq)) . n) = (a * ((Lf /* xseq) . n))

        proof

          let n be Nat;

          

           A51: n in NAT by ORDINAL1:def 12;

          (xseq . n) in ( rng xseq) by FUNCT_2: 4, ORDINAL1:def 12;

          then

          reconsider xn = (xseq . n) as Point of E1 by A3, A42;

          

           A53: (a * (xseq . n)) = (a * xn) by NORMSP_3: 28;

          then (a * (xseq . n)) in the carrier of E1;

          then

           A55: (a * (xseq . n)) in ( dom L) by FUNCT_2:def 1;

          

          thus ((Lf /* (a * xseq)) . n) = (Lf /. ((a * xseq) . n)) by A49, A51, FUNCT_2: 109

          .= (Lf /. (a * (xseq . n))) by NORMSP_1:def 5

          .= (L . (a * xn)) by A53, A55, PARTFUN1:def 6

          .= (a * (L /. xn)) by LOPBAN_1:def 5

          .= (a * ((Lf /* xseq) . n)) by A50, A51, FUNCT_2: 109;

        end;

        ( lim (Lf /* (a * xseq))) = ( lim (a * (Lf /* xseq))) by B50, NORMSP_1:def 5

        .= (a * ( lim (Lf /* xseq))) by A42, NORMSP_1: 28;

        hence (Pg . (a * x)) = (a * (Pg . x)) by A20, A42, A46, A47, A48;

      end;

      then

      reconsider Pg as LinearOperator of E, F by A23, LOPBAN_1:def 5, VECTSP_1:def 20;

      reconsider Pg as Lipschitzian LinearOperator of E, F by A18, NFCONT_2: 7, LOPBAN_7: 6;

      reconsider g = Pg as Point of ( R_NormSpace_of_BoundedLinearOperators (E,F)) by LOPBAN_1:def 9;

      

       A58: ( dom g) = the carrier of E by FUNCT_2:def 1;

      

       A61: ||.f.|| = ( upper_bound ( PreNorms ( modetrans (f,E1,F)))) by LOPBAN_1:def 13

      .= ( upper_bound ( PreNorms L)) by LOPBAN_1: 29;

      

       A63: ||.g.|| = ( upper_bound ( PreNorms ( modetrans (g,E,F)))) by LOPBAN_1:def 13

      .= ( upper_bound ( PreNorms Pg)) by LOPBAN_1: 29;

      for t be Real st t in ( PreNorms L) holds t <= ||.g.||

      proof

        let t be Real;

        assume t in ( PreNorms L);

        then

        consider w be Point of E1 such that

         A64: t = ||.(L . w).|| & ||.w.|| <= 1;

        

         A65: the carrier of E1 c= the carrier of E by DUALSP01:def 16;

        w in the carrier of E1;

        then

        reconsider w1 = w as Point of E by A65;

        

         A67: ||.w1.|| <= 1 by A64, NORMSP_3: 28;

        

         A68: not ( PreNorms Pg) is empty & ( PreNorms Pg) is bounded_above by LOPBAN_1: 27;

        (L . w) = (Pg . w1) by A3, A17, FUNCT_1: 49;

        then t in ( PreNorms Pg) by A64, A67;

        hence t <= ||.g.|| by A63, A68, SEQ_4:def 1;

      end;

      then

       A69: ||.f.|| <= ||.g.|| by A61, SEQ_4: 45;

      for t be Real st t in ( PreNorms Pg) holds t <= ||.f.||

      proof

        let t be Real;

        assume t in ( PreNorms Pg);

        then

        consider x be Point of E such that

         A70: t = ||.(Pg . x).|| & ||.x.|| <= 1;

        consider xseq be sequence of E such that

         A71: ( rng xseq) c= E0 & xseq is convergent & ( lim xseq) = x & (Lf /* xseq) is convergent & (Pg . x) = ( lim (Lf /* xseq)) by A19;

        

         A72: ||.(Pg . x).|| = ( lim ||.(Lf /* xseq).||) by A71, LOPBAN_1: 20;

        

         A73: ||.xseq.|| is convergent & ( lim ||.xseq.||) = ||.( lim xseq).|| by A71, LOPBAN_1: 20;

        

         A74: ||.(Lf /* xseq).|| is convergent by A71, NORMSP_1: 23;

        

         A75: ( ||.f.|| (#) ||.xseq.||) is convergent by A71, LOPBAN_1: 20, SEQ_2: 7;

        for n be Nat holds ( ||.(Lf /* xseq).|| . n) <= (( ||.f.|| (#) ||.xseq.||) . n)

        proof

          let n be Nat;

          

           A77: n in NAT by ORDINAL1:def 12;

          

           A78: ( rng xseq) c= ( dom Lf) by A3, A71, FUNCT_2:def 1;

          (xseq . n) in ( rng xseq) by FUNCT_2: 4, ORDINAL1:def 12;

          then

          reconsider xn = (xseq . n) as Point of E1 by A3, A71;

          

           A80: ( dom Lf) = the carrier of E1 by FUNCT_2:def 1;

          

           A81: ( ||.(Lf /* xseq).|| . n) = ||.((Lf /* xseq) . n).|| by NORMSP_0:def 4

          .= ||.(Lf /. (xseq . n)).|| by A77, A78, FUNCT_2: 109

          .= ||.(L . xn).|| by A80, PARTFUN1:def 6;

           ||.(L . xn).|| <= ( ||.f.|| * ||.xn.||) by LOPBAN_1: 32;

          then ||.(L . xn).|| <= ( ||.f.|| * ||.(xseq . n).||) by NORMSP_3: 28;

          then ||.(L . xn).|| <= ( ||.f.|| * ( ||.xseq.|| . n)) by NORMSP_0:def 4;

          hence thesis by A81, VALUED_1: 6;

        end;

        then ( lim ||.(Lf /* xseq).||) <= ( lim ( ||.f.|| (#) ||.xseq.||)) by A74, A75, SEQ_2: 18;

        then

         A82: ( lim ||.(Lf /* xseq).||) <= ( ||.f.|| * ||.x.||) by A71, A73, SEQ_2: 8;

        ( ||.f.|| * ||.x.||) <= ( ||.f.|| * 1) by A70, XREAL_1: 64;

        hence t <= ||.f.|| by A70, A72, A82, XXREAL_0: 2;

      end;

      then ||.g.|| <= ||.f.|| by A63, SEQ_4: 45;

      hence ex g be Point of ( R_NormSpace_of_BoundedLinearOperators (E,F)) st ( dom g) = the carrier of E & (g | the carrier of E1) = f & ||.g.|| = ||.f.|| & ex Lf be PartFunc of E, F st Lf = f & (for x be Point of E holds ex seq be sequence of E st ( rng seq) c= the carrier of E1 & seq is convergent & ( lim seq) = x & (Lf /* seq) is convergent & (g . x) = ( lim (Lf /* seq))) & (for x be Point of E, seq be sequence of E st ( rng seq) c= the carrier of E1 & seq is convergent & ( lim seq) = x holds (Lf /* seq) is convergent & (g . x) = ( lim (Lf /* seq))) by A3, A17, A21, A22, A58, A69, XXREAL_0: 1;

      thus for g1,g2 be Point of ( R_NormSpace_of_BoundedLinearOperators (E,F)) st (g1 | the carrier of E1) = f & (g2 | the carrier of E1) = f holds g1 = g2

      proof

        let g1,g2 be Point of ( R_NormSpace_of_BoundedLinearOperators (E,F));

        assume

         A84: (g1 | the carrier of E1) = f & (g2 | the carrier of E1) = f;

        reconsider Pg1 = g1, Pg2 = g2 as Lipschitzian LinearOperator of E, F by LOPBAN_1:def 9;

        

         A85: Pg1 is_continuous_on the carrier of E by LMCONT1, NFCONT_2: 7;

        Pg2 is_continuous_on the carrier of E by LMCONT1, NFCONT_2: 7;

        hence thesis by A1, A3, A5, A15, A84, A85, Th020;

      end;

    end;

    begin

    theorem :: LOPBAN_8:5

    for E,F,G be non empty set, f be Function of [:E, F:], G, x be object st x in E holds (( curry f) . x) is Function of F, G

    proof

      let E,F,G be non empty set, f be Function of [:E, F:], G, x be object;

      assume

       A1: x in E;

      ( dom f) = [:E, F:] by FUNCT_2:def 1;

      then

      consider g be Function such that

       A4: (( curry f) . x) = g & ( dom g) = F & ( rng g) c= ( rng f) & for y be object st y in F holds (g . y) = (f . (x,y)) by A1, FUNCT_5: 29, ZFMISC_1: 90;

      thus (( curry f) . x) is Function of F, G by A4, XBOOLE_1: 1, FUNCT_2: 2;

    end;

    theorem :: LOPBAN_8:6

    for E,F,G be non empty set, f be Function of [:E, F:], G, y be object st y in F holds (( curry' f) . y) is Function of E, G

    proof

      let E,F,G be non empty set, f be Function of [:E, F:], G, y be object;

      assume

       A1: y in F;

      ( dom f) = [:E, F:] by FUNCT_2:def 1;

      then ex g be Function st (( curry' f) . y) = g & ( dom g) = E & ( rng g) c= ( rng f) & for x be object st x in E holds (g . x) = (f . (x,y)) by A1, FUNCT_5: 32, ZFMISC_1: 90;

      hence (( curry' f) . y) is Function of E, G by XBOOLE_1: 1, FUNCT_2: 2;

    end;

    theorem :: LOPBAN_8:7

    

     LM4: for E,F,G be non empty set, f be Function of [:E, F:], G, x,y be object st x in E & y in F holds ((( curry f) . x) . y) = (f . (x,y))

    proof

      let E,F,G be non empty set, f be Function of [:E, F:], G, x,y be object;

      assume that

       A1: x in E and

       A2: y in F;

      ( dom f) = [:E, F:] by FUNCT_2:def 1;

      then ex g be Function st (( curry f) . x) = g & ( dom g) = F & ( rng g) c= ( rng f) & for y be object st y in F holds (g . y) = (f . (x,y)) by A1, FUNCT_5: 29, ZFMISC_1: 90;

      hence ((( curry f) . x) . y) = (f . (x,y)) by A2;

    end;

    theorem :: LOPBAN_8:8

    

     LM5: for E,F,G be non empty set, f be Function of [:E, F:], G, x,y be object st x in E & y in F holds ((( curry' f) . y) . x) = (f . (x,y))

    proof

      let E,F,G be non empty set, f be Function of [:E, F:], G, x,y be object;

      assume that

       A1: x in E and

       A2: y in F;

      ( dom f) = [:E, F:] by FUNCT_2:def 1;

      then ex g be Function st (( curry' f) . y) = g & ( dom g) = E & ( rng g) c= ( rng f) & for x be object st x in E holds (g . x) = (f . (x,y)) by A2, FUNCT_5: 32, ZFMISC_1: 90;

      hence ((( curry' f) . y) . x) = (f . (x,y)) by A1;

    end;

    definition

      let E,F,G be RealLinearSpace;

      let f be Function of [:the carrier of E, the carrier of F:], the carrier of G;

      :: LOPBAN_8:def1

      attr f is Bilinear means (for v be Point of E st v in ( dom ( curry f)) holds (( curry f) . v) is additive homogeneous Function of F, G) & (for v be Point of F st v in ( dom ( curry' f)) holds (( curry' f) . v) is additive homogeneous Function of E, G);

    end

    begin

    theorem :: LOPBAN_8:9

    

     EX1: for E,F,G be RealLinearSpace holds ( [:the carrier of E, the carrier of F:] --> ( 0. G)) is Bilinear

    proof

      let E,F,G be RealLinearSpace;

      set f = ( [:the carrier of E, the carrier of F:] --> ( 0. G));

      

       A2: for x be Point of E holds (( curry f) . x) is additive homogeneous Function of F, G

      proof

        let x be Point of E;

        reconsider L = (( curry f) . x) as Function of F, G;

        

         A5: for y1,y2 be Point of F holds (L . (y1 + y2)) = ((L . y1) + (L . y2))

        proof

          let y1,y2 be Point of F;

          

           A11: (L . (y1 + y2)) = (f . (x,(y1 + y2))) by LM4

          .= ( 0. G) by ZFMISC_1: 87, FUNCOP_1: 7;

          

           A12: (L . y1) = (f . (x,y1)) by LM4

          .= ( 0. G) by ZFMISC_1: 87, FUNCOP_1: 7;

          (L . y2) = (f . (x,y2)) by LM4

          .= ( 0. G) by ZFMISC_1: 87, FUNCOP_1: 7;

          hence (L . (y1 + y2)) = ((L . y1) + (L . y2)) by A11, A12, RLVECT_1: 4;

        end;

        for y be Point of F, a be Real holds (L . (a * y)) = (a * (L . y))

        proof

          let y be Point of F, a be Real;

          

           A18: (L . (a * y)) = (f . (x,(a * y))) by LM4

          .= ( 0. G) by ZFMISC_1: 87, FUNCOP_1: 7;

          (L . y) = (f . (x,y)) by LM4

          .= ( 0. G) by ZFMISC_1: 87, FUNCOP_1: 7;

          hence (L . (a * y)) = (a * (L . y)) by A18, RLVECT_1: 10;

        end;

        hence thesis by A5, LOPBAN_1:def 5, VECTSP_1:def 20;

      end;

      for x be Point of F st x in ( dom ( curry' f)) holds (( curry' f) . x) is additive homogeneous Function of E, G

      proof

        let x be Point of F;

        assume x in ( dom ( curry' f));

        reconsider L = (( curry' f) . x) as Function of E, G;

        

         A22: for y1,y2 be Point of E holds (L . (y1 + y2)) = ((L . y1) + (L . y2))

        proof

          let y1,y2 be Point of E;

          

           A28: (L . (y1 + y2)) = (f . ((y1 + y2),x)) by LM5

          .= ( 0. G) by ZFMISC_1: 87, FUNCOP_1: 7;

          

           A29: (L . y1) = (f . (y1,x)) by LM5

          .= ( 0. G) by ZFMISC_1: 87, FUNCOP_1: 7;

          (L . y2) = (f . (y2,x)) by LM5

          .= ( 0. G) by ZFMISC_1: 87, FUNCOP_1: 7;

          hence (L . (y1 + y2)) = ((L . y1) + (L . y2)) by A28, A29, RLVECT_1: 4;

        end;

        for y be Point of E, a be Real holds (L . (a * y)) = (a * (L . y))

        proof

          let y be Point of E, a be Real;

          

           A35: (L . (a * y)) = (f . ((a * y),x)) by LM5

          .= ( 0. G) by ZFMISC_1: 87, FUNCOP_1: 7;

          (L . y) = (f . (y,x)) by LM5

          .= ( 0. G) by ZFMISC_1: 87, FUNCOP_1: 7;

          hence (L . (a * y)) = (a * (L . y)) by A35, RLVECT_1: 10;

        end;

        hence thesis by A22, LOPBAN_1:def 5, VECTSP_1:def 20;

      end;

      hence f is Bilinear by A2;

    end;

    registration

      let E,F,G be RealLinearSpace;

      cluster Bilinear for Function of [:the carrier of E, the carrier of F:], the carrier of G;

      correctness

      proof

        ( [:the carrier of E, the carrier of F:] --> ( 0. G)) is Bilinear by EX1;

        hence thesis;

      end;

    end

    theorem :: LOPBAN_8:10

    

     LM6: for E,F,G be RealLinearSpace, L be Function of [:the carrier of E, the carrier of F:], the carrier of G holds L is Bilinear iff ((for x1,x2 be Point of E, y be Point of F holds (L . ((x1 + x2),y)) = ((L . (x1,y)) + (L . (x2,y)))) & (for x be Point of E, y be Point of F, a be Real holds (L . ((a * x),y)) = (a * (L . (x,y)))) & (for x be Point of E, y1,y2 be Point of F holds (L . (x,(y1 + y2))) = ((L . (x,y1)) + (L . (x,y2)))) & (for x be Point of E, y be Point of F, a be Real holds (L . (x,(a * y))) = (a * (L . (x,y)))))

    proof

      let E,F,G be RealLinearSpace, L be Function of [:the carrier of E, the carrier of F:], the carrier of G;

      

       A1: ( dom ( curry L)) = the carrier of E & ( dom ( curry' L)) = the carrier of F by FUNCT_2:def 1;

      hereby

        assume

         A2: L is Bilinear;

        thus for x1,x2 be Point of E, y be Point of F holds (L . ((x1 + x2),y)) = ((L . (x1,y)) + (L . (x2,y)))

        proof

          let x1,x2 be Point of E, y be Point of F;

          reconsider Ly = (( curry' L) . y) as additive homogeneous Function of E, G by A1, A2;

          

           A5: (Ly . x1) = (L . (x1,y)) by LM5;

          

           A6: (Ly . x2) = (L . (x2,y)) by LM5;

          

          thus (L . ((x1 + x2),y)) = (Ly . (x1 + x2)) by LM5

          .= ((L . (x1,y)) + (L . (x2,y))) by A5, A6, VECTSP_1:def 20;

        end;

        thus for x be Point of E, y be Point of F, a be Real holds (L . ((a * x),y)) = (a * (L . (x,y)))

        proof

          let x be Point of E, y be Point of F, a be Real;

          reconsider Ly = (( curry' L) . y) as additive homogeneous Function of E, G by A1, A2;

          

          thus (L . ((a * x),y)) = (Ly . (a * x)) by LM5

          .= (a * (Ly . x)) by LOPBAN_1:def 5

          .= (a * (L . (x,y))) by LM5;

        end;

        thus for x be Point of E, y1,y2 be Point of F holds (L . (x,(y1 + y2))) = ((L . (x,y1)) + (L . (x,y2)))

        proof

          let x be Point of E, y1,y2 be Point of F;

          reconsider Lx = (( curry L) . x) as additive homogeneous Function of F, G by A1, A2;

          

           A8: (Lx . y1) = (L . (x,y1)) by LM4;

          

           A9: (Lx . y2) = (L . (x,y2)) by LM4;

          

          thus (L . (x,(y1 + y2))) = (Lx . (y1 + y2)) by LM4

          .= ((L . (x,y1)) + (L . (x,y2))) by A8, A9, VECTSP_1:def 20;

        end;

        thus for x be Point of E, y be Point of F, a be Real holds (L . (x,(a * y))) = (a * (L . (x,y)))

        proof

          let x be Point of E, y be Point of F, a be Real;

          reconsider Lx = (( curry L) . x) as additive homogeneous Function of F, G by A1, A2;

          

           A10: (Lx . y) = (L . (x,y)) by LM4;

          

          thus (L . (x,(a * y))) = (Lx . (a * y)) by LM4

          .= (a * (L . (x,y))) by A10, LOPBAN_1:def 5;

        end;

      end;

      assume that

       A11: for x1,x2 be Point of E, y be Point of F holds (L . ((x1 + x2),y)) = ((L . (x1,y)) + (L . (x2,y))) and

       A12: for x be Point of E, y be Point of F, a be Real holds (L . ((a * x),y)) = (a * (L . (x,y))) and

       A13: for x be Point of E, y1,y2 be Point of F holds (L . (x,(y1 + y2))) = ((L . (x,y1)) + (L . (x,y2))) and

       A14: for x be Point of E, y be Point of F, a be Real holds (L . (x,(a * y))) = (a * (L . (x,y)));

      

       A15: for x be Point of E st x in ( dom ( curry L)) holds (( curry L) . x) is additive homogeneous Function of F, G

      proof

        let x be Point of E;

        assume x in ( dom ( curry L));

        reconsider Lx = (( curry L) . x) as Function of F, G;

        

         A16: for y1,y2 be Point of F holds (Lx . (y1 + y2)) = ((Lx . y1) + (Lx . y2))

        proof

          let y1,y2 be Point of F;

          

           A17: (L . (x,y1)) = (Lx . y1) by LM4;

          

          thus (Lx . (y1 + y2)) = (L . (x,(y1 + y2))) by LM4

          .= ((L . (x,y1)) + (L . (x,y2))) by A13

          .= ((Lx . y1) + (Lx . y2)) by A17, LM4;

        end;

        for y be Point of F, a be Real holds (Lx . (a * y)) = (a * (Lx . y))

        proof

          let y be Point of F, a be Real;

          

          thus (Lx . (a * y)) = (L . (x,(a * y))) by LM4

          .= (a * (L . (x,y))) by A14

          .= (a * (Lx . y)) by LM4;

        end;

        hence thesis by A16, LOPBAN_1:def 5, VECTSP_1:def 20;

      end;

      for y be Point of F st y in ( dom ( curry' L)) holds (( curry' L) . y) is additive homogeneous Function of E, G

      proof

        let y be Point of F;

        assume y in ( dom ( curry' L));

        reconsider Ly = (( curry' L) . y) as Function of E, G;

        

         A22: for x1,x2 be Point of E holds (Ly . (x1 + x2)) = ((Ly . x1) + (Ly . x2))

        proof

          let x1,x2 be Point of E;

          

           A23: (L . (x1,y)) = (Ly . x1) by LM5;

          

          thus (Ly . (x1 + x2)) = (L . ((x1 + x2),y)) by LM5

          .= ((L . (x1,y)) + (L . (x2,y))) by A11

          .= ((Ly . x1) + (Ly . x2)) by A23, LM5;

        end;

        for x be Point of E, a be Real holds (Ly . (a * x)) = (a * (Ly . x))

        proof

          let x be Point of E, a be Real;

          

          thus (Ly . (a * x)) = (L . ((a * x),y)) by LM5

          .= (a * (L . (x,y))) by A12

          .= (a * (Ly . x)) by LM5;

        end;

        hence thesis by A22, LOPBAN_1:def 5, VECTSP_1:def 20;

      end;

      hence L is Bilinear by A15;

    end;

    definition

      let E,F,G be RealLinearSpace;

      let f be Function of [:E, F:], G;

      :: LOPBAN_8:def2

      attr f is Bilinear means ex g be Function of [:the carrier of E, the carrier of F:], the carrier of G st f = g & g is Bilinear;

    end

    registration

      let E,F,G be RealLinearSpace;

      cluster Bilinear for Function of [:E, F:], G;

      correctness

      proof

        set g = ( [:the carrier of E, the carrier of F:] --> ( 0. G));

        reconsider f = g as Function of [:E, F:], G;

        take f;

        thus thesis by EX1;

      end;

    end

    definition

      let E,F,G be RealLinearSpace;

      let f be Function of [:E, F:], G;

      let x be Point of E;

      let y be Point of F;

      :: original: .

      redefine

      func f . (x,y) -> Point of G ;

      correctness

      proof

         [x, y] is set by TARSKI: 1;

        then

        reconsider z = [x, y] as Point of [:E, F:] by PRVECT_3: 9;

        (f . z) is Point of G;

        hence thesis;

      end;

    end

    theorem :: LOPBAN_8:11

    for E,F,G be RealLinearSpace, L be Function of [:E, F:], G holds L is Bilinear iff ((for x1,x2 be Point of E, y be Point of F holds (L . ((x1 + x2),y)) = ((L . (x1,y)) + (L . (x2,y)))) & (for x be Point of E, y be Point of F, a be Real holds (L . ((a * x),y)) = (a * (L . (x,y)))) & (for x be Point of E, y1,y2 be Point of F holds (L . (x,(y1 + y2))) = ((L . (x,y1)) + (L . (x,y2)))) & (for x be Point of E, y be Point of F, a be Real holds (L . (x,(a * y))) = (a * (L . (x,y))))) by LM6;

    definition

      let E,F,G be RealLinearSpace;

      mode BilinearOperator of E,F,G is Bilinear Function of [:E, F:], G;

    end

    definition

      let E,F,G be RealNormSpace;

      let f be Function of [:E, F:], G;

      :: LOPBAN_8:def3

      attr f is Bilinear means ex g be Function of [:the carrier of E, the carrier of F:], the carrier of G st f = g & g is Bilinear;

    end

    registration

      let E,F,G be RealNormSpace;

      cluster Bilinear for Function of [:E, F:], G;

      correctness

      proof

        set g = ( [:the carrier of E, the carrier of F:] --> ( 0. G));

        reconsider f = g as Function of [:E, F:], G;

        take f;

        thus thesis by EX1;

      end;

    end

    definition

      let E,F,G be RealNormSpace;

      mode BilinearOperator of E,F,G is Bilinear Function of [:E, F:], G;

    end

    reserve E,F,G for RealNormSpace;

    reserve L for BilinearOperator of E, F, G;

    reserve x for Element of E;

    reserve y for Element of F;

    definition

      let E,F,G be RealNormSpace;

      let f be Function of [:E, F:], G;

      let x be Point of E;

      let y be Point of F;

      :: original: .

      redefine

      func f . (x,y) -> Point of G ;

      correctness

      proof

         [x, y] is set by TARSKI: 1;

        then

        reconsider z = [x, y] as Point of [:E, F:] by PRVECT_3: 18;

        (f . z) is Point of G;

        hence thesis;

      end;

    end

    theorem :: LOPBAN_8:12

    

     LM8: for E,F,G be RealNormSpace, L be Function of [:E, F:], G holds L is Bilinear iff ((for x1,x2 be Point of E, y be Point of F holds (L . ((x1 + x2),y)) = ((L . (x1,y)) + (L . (x2,y)))) & (for x be Point of E, y be Point of F, a be Real holds (L . ((a * x),y)) = (a * (L . (x,y)))) & (for x be Point of E, y1,y2 be Point of F holds (L . (x,(y1 + y2))) = ((L . (x,y1)) + (L . (x,y2)))) & (for x be Point of E, y be Point of F, a be Real holds (L . (x,(a * y))) = (a * (L . (x,y))))) by LM6;

    theorem :: LOPBAN_8:13

    for E,F,G be RealNormSpace, f be BilinearOperator of E, F, G holds (f is_continuous_on the carrier of [:E, F:] iff f is_continuous_in ( 0. [:E, F:])) & (f is_continuous_on the carrier of [:E, F:] iff ex K be Real st 0 <= K & for x be Point of E, y be Point of F holds ||.(f . (x,y)).|| <= ((K * ||.x.||) * ||.y.||))

    proof

      let E,F,G be RealNormSpace, f be BilinearOperator of E, F, G;

      

       A1: ( dom f) = the carrier of [:E, F:] by FUNCT_2:def 1;

      

       A2: (f . ( 0. [:E, F:])) = (f . (( 0. E),( 0. F))) by PRVECT_3: 18

      .= (f . (( 0 * ( 0. E)),( 0. F))) by RLVECT_1: 10

      .= ( 0 * (f . (( 0. E),( 0. F)))) by LM8

      .= ( 0. G) by RLVECT_1: 10;

      

       A4: f is_continuous_in ( 0. [:E, F:]) implies ex K be Real st 0 <= K & for x be Point of E, y be Point of F holds ||.(f . (x,y)).|| <= ((K * ||.x.||) * ||.y.||)

      proof

        assume f is_continuous_in ( 0. [:E, F:]);

        then

        consider s be Real such that

         A5: 0 < s & for z be Point of [:E, F:] st z in ( dom f) & ||.(z - ( 0. [:E, F:])).|| < s holds ||.((f /. z) - (f /. ( 0. [:E, F:]))).|| < 1 by NFCONT_1: 7;

        consider s1 be Real such that

         A7: 0 < s1 & s1 < s & [:( Ball (( 0. E),s1)), ( Ball (( 0. F),s1)):] c= ( Ball (( 0. [:E, F:]),s)) by A5, NDIFF_8: 22, PRVECT_3: 18;

        set s2 = (s1 / 2);

        

         A8: 0 < s2 & s2 < s1 by A7, XREAL_1: 215, XREAL_1: 216;

         A9:

        now

          let x be Point of E, y be Point of F;

          assume ||.x.|| <= s2 & ||.y.|| <= s2;

          then

           A10: ||.x.|| < s1 & ||.y.|| < s1 by A8, XXREAL_0: 2;

           [x, y] is set by TARSKI: 1;

          then

          reconsider z = [x, y] as Point of [:E, F:] by PRVECT_3: 18;

           ||.(x - ( 0. E)).|| < s1 by A10, RLVECT_1: 13;

          then ||.(( 0. E) - x).|| < s1 by NORMSP_1: 7;

          then

           A12: x in ( Ball (( 0. E),s1));

           ||.(y - ( 0. F)).|| < s1 by A10, RLVECT_1: 13;

          then ||.(( 0. F) - y).|| < s1 by NORMSP_1: 7;

          then y in ( Ball (( 0. F),s1));

          then z in [:( Ball (( 0. E),s1)), ( Ball (( 0. F),s1)):] by A12, ZFMISC_1: 87;

          then z in ( Ball (( 0. [:E, F:]),s)) by A7;

          then ex z1 be Point of [:E, F:] st z = z1 & ||.(( 0. [:E, F:]) - z1).|| < s;

          then ||.(z - ( 0. [:E, F:])).|| < s by NORMSP_1: 7;

          then ||.((f /. z) - (f /. ( 0. [:E, F:]))).|| < 1 by A5, A1;

          hence ||.(f . (x,y)).|| < 1 by A2, RLVECT_1: 13;

        end;

        

         A14: 0 < (s2 * s2) by A8, XREAL_1: 129;

        take K = (1 / (s2 * s2));

        thus 0 <= K by A7;

        let x be Point of E, y be Point of F;

        

         A15: (f . (( 0. E),y)) = (f . (( 0 * ( 0. E)),y)) by RLVECT_1: 10

        .= ( 0 * (f . (( 0. E),y))) by LM8

        .= ( 0. G) by RLVECT_1: 10;

        

         A16: (f . (x,( 0. F))) = (f . (x,( 0 * ( 0. F)))) by RLVECT_1: 10

        .= ( 0 * (f . (x,( 0. F)))) by LM8

        .= ( 0. G) by RLVECT_1: 10;

        thus ||.(f . (x,y)).|| <= ((K * ||.x.||) * ||.y.||)

        proof

          per cases ;

            suppose

             C16: x <> ( 0. E) & y <> ( 0. F);

            then ||.x.|| <> 0 & ||.y.|| <> 0 by NORMSP_0:def 5;

            then

             A17: 0 < ||.x.|| & 0 < ||.y.||;

            set x1 = ((s2 / ||.x.||) * x);

            set y1 = ((s2 / ||.y.||) * y);

            

             A19: ||.x1.|| = ( |.(s2 / ||.x.||).| * ||.x.||) by NORMSP_1:def 1

            .= ((s2 / ||.x.||) * ||.x.||) by A7, COMPLEX1: 43

            .= s2 by C16, NORMSP_0:def 5, XCMPLX_1: 87;

            

             A21: ||.y1.|| = ( |.(s2 / ||.y.||).| * ||.y.||) by NORMSP_1:def 1

            .= ((s2 / ||.y.||) * ||.y.||) by A7, COMPLEX1: 43

            .= s2 by C16, NORMSP_0:def 5, XCMPLX_1: 87;

            

             A23: (f . (x1,y1)) = ((s2 / ||.x.||) * (f . (x,((s2 / ||.y.||) * y)))) by LM8;

            (f . (x,((s2 / ||.y.||) * y))) = ((s2 / ||.y.||) * (f . (x,y))) by LM8;

            

            then

             A24: (f . (x1,y1)) = (((s2 / ||.x.||) * (s2 / ||.y.||)) * (f . (x,y))) by A23, RLVECT_1:def 7

            .= (((s2 * s2) / ( ||.x.|| * ||.y.||)) * (f . (x,y))) by XCMPLX_1: 76;

            

             A25: 0 < ( ||.x.|| * ||.y.||) by A17, XREAL_1: 129;

             ||.(f . (x1,y1)).|| = ( |.((s2 * s2) / ( ||.x.|| * ||.y.||)).| * ||.(f . (x,y)).||) by A24, NORMSP_1:def 1

            .= (((s2 * s2) / ( ||.x.|| * ||.y.||)) * ||.(f . (x,y)).||) by A7, COMPLEX1: 43;

            then

             A28: (((s2 * s2) / ( ||.x.|| * ||.y.||)) * ||.(f . (x,y)).||) < 1 by A9, A19, A21;

            ((((s2 * s2) / ( ||.x.|| * ||.y.||)) * ||.(f . (x,y)).||) * ( ||.x.|| * ||.y.||)) <= (1 * ( ||.x.|| * ||.y.||)) by A28, XREAL_1: 64;

            then ((((s2 * s2) / ( ||.x.|| * ||.y.||)) * ( ||.x.|| * ||.y.||)) * ||.(f . (x,y)).||) <= ( ||.x.|| * ||.y.||);

            then ((s2 * s2) * ||.(f . (x,y)).||) <= ( ||.x.|| * ||.y.||) by A25, XCMPLX_1: 87;

            then (((s2 * s2) * ||.(f . (x,y)).||) / (s2 * s2)) <= (( ||.x.|| * ||.y.||) / (s2 * s2)) by A7, XREAL_1: 72;

            then ||.(f . (x,y)).|| <= (( ||.x.|| * ||.y.||) / (s2 * s2)) by A14, XCMPLX_1: 89;

            then ||.(f . (x,y)).|| <= ((1 / (s2 * s2)) * ( ||.x.|| * ||.y.||)) by XCMPLX_1: 99;

            hence ||.(f . (x,y)).|| <= ((K * ||.x.||) * ||.y.||);

          end;

            suppose

             A29: x = ( 0. E) or y = ( 0. F);

            then ||.x.|| = 0 or ||.y.|| = 0 ;

            hence ||.(f . (x,y)).|| <= ((K * ||.x.||) * ||.y.||) by A15, A16, A29;

          end;

        end;

      end;

      (ex K be Real st 0 <= K & for x be Point of E, y be Point of F holds ||.(f . (x,y)).|| <= ((K * ||.x.||) * ||.y.||)) implies f is_continuous_on the carrier of [:E, F:]

      proof

        given K be Real such that

         A32: 0 <= K & for x be Point of E, y be Point of F holds ||.(f . (x,y)).|| <= ((K * ||.x.||) * ||.y.||);

        

         A33: the carrier of [:E, F:] c= ( dom f) by FUNCT_2:def 1;

        for z0 be Point of [:E, F:], r1 be Real st z0 in the carrier of [:E, F:] & 0 < r1 holds ex s be Real st 0 < s & for z1 be Point of [:E, F:] st z1 in the carrier of [:E, F:] & ||.(z1 - z0).|| < s holds ||.((f /. z1) - (f /. z0)).|| < r1

        proof

          let z0 be Point of [:E, F:], r1 be Real;

          assume

           A34: z0 in the carrier of [:E, F:] & 0 < r1;

          set r = (r1 / 2);

          

           A35: 0 < r & r < r1 by A34, XREAL_1: 215, XREAL_1: 216;

          consider x0 be Point of E, y0 be Point of F such that

           A36: z0 = [x0, y0] by PRVECT_3: 18;

          set KXY0 = ((K + 1) * (( ||.x0.|| + 1) + ||.y0.||));

          set s1 = (r / KXY0);

          (K + 0 ) < (K + 1) by XREAL_1: 8;

          then

           A39: (K * (( ||.x0.|| + 1) + ||.y0.||)) < ((K + 1) * (( ||.x0.|| + 1) + ||.y0.||)) by XREAL_1: 68;

          

           A40: 0 < KXY0 by A32, XREAL_1: 129;

          then

           A41: 0 < s1 by A35, XREAL_1: 139;

          set s = ( min (s1,1));

          

           A42: s <= 1 & s <= s1 by XXREAL_0: 17;

          

           A43: 0 < s by A41, XXREAL_0: 21;

          then

           A44: ((K * (( ||.x0.|| + 1) + ||.y0.||)) * s) <= (KXY0 * s1) by A32, A39, A42, XREAL_1: 66;

          take s;

          thus 0 < s by A41, XXREAL_0: 21;

          let z1 be Point of [:E, F:];

          assume

           A45: z1 in the carrier of [:E, F:] & ||.(z1 - z0).|| < s;

          consider x1 be Point of E, y1 be Point of F such that

           A46: z1 = [x1, y1] by PRVECT_3: 18;

          

           A47: ((f . z1) - (f . z0)) = ((((f . (x1,y1)) - (f . (x0,y1))) + (f . (x0,y1))) - (f . (x0,y0))) by A36, A46, RLVECT_4: 1

          .= (((f . (x1,y1)) - (f . (x0,y1))) + ((f . (x0,y1)) - (f . (x0,y0)))) by RLVECT_1: 28;

          

           A49: ((f . (x1,y1)) - (f . (x0,y1))) = ((f . (x1,y1)) + (( - 1) * (f . (x0,y1)))) by RLVECT_1: 16

          .= ((f . (x1,y1)) + (f . ((( - 1) * x0),y1))) by LM8

          .= (f . ((x1 + (( - 1) * x0)),y1)) by LM8

          .= (f . ((x1 - x0),y1)) by RLVECT_1: 16;

          

           A51: ((f . (x0,y1)) - (f . (x0,y0))) = ((f . (x0,y1)) + (( - 1) * (f . (x0,y0)))) by RLVECT_1: 16

          .= ((f . (x0,y1)) + (f . (x0,(( - 1) * y0)))) by LM8

          .= (f . (x0,(y1 + (( - 1) * y0)))) by LM8

          .= (f . (x0,(y1 - y0))) by RLVECT_1: 16;

          

           A52: ||.(f . ((x1 - x0),y1)).|| <= ((K * ||.(x1 - x0).||) * ||.y1.||) by A32;

          

           A53: ||.(f . (x0,(y1 - y0))).|| <= ((K * ||.x0.||) * ||.(y1 - y0).||) by A32;

          ( - z0) = [( - x0), ( - y0)] by A36, PRVECT_3: 18;

          then

           A54: (z1 - z0) = [(x1 - x0), (y1 - y0)] by A46, PRVECT_3: 18;

          then ||.(x1 - x0).|| <= ||.(z1 - z0).|| by NDIFF_8: 21;

          then

           A55: ||.(x1 - x0).|| < s by A45, XXREAL_0: 2;

           ||.(y1 - y0).|| <= ||.(z1 - z0).|| by A54, NDIFF_8: 21;

          then

           A56: ||.(y1 - y0).|| < s by A45, XXREAL_0: 2;

          ( ||.(x1 - x0).|| * ||.y1.||) <= (s * ||.y1.||) by A55, XREAL_1: 64;

          then (K * ( ||.(x1 - x0).|| * ||.y1.||)) <= (K * (s * ||.y1.||)) by A32, XREAL_1: 64;

          then

           A57: ||.(f . ((x1 - x0),y1)).|| <= ((K * s) * ||.y1.||) by A52, XXREAL_0: 2;

          ( ||.(y1 - y0).|| * ||.x0.||) <= (s * ||.x0.||) by A56, XREAL_1: 64;

          then (K * ( ||.x0.|| * ||.(y1 - y0).||)) <= (K * (s * ||.x0.||)) by A32, XREAL_1: 64;

          then ||.(f . (x0,(y1 - y0))).|| <= ((K * s) * ||.x0.||) by A53, XXREAL_0: 2;

          then

           A58: ( ||.(f . ((x1 - x0),y1)).|| + ||.(f . (x0,(y1 - y0))).||) <= (((K * s) * ||.y1.||) + ((K * s) * ||.x0.||)) by A57, XREAL_1: 7;

           ||.y1.|| = ||.((y1 - y0) + y0).|| by RLVECT_4: 1;

          then

           A60: ||.y1.|| <= ( ||.(y1 - y0).|| + ||.y0.||) by NORMSP_1:def 1;

          ( ||.(y1 - y0).|| + ||.y0.||) <= (s + ||.y0.||) by A56, XREAL_1: 7;

          then

           A61: ||.y1.|| <= (s + ||.y0.||) by A60, XXREAL_0: 2;

          (s + ||.y0.||) <= (1 + ||.y0.||) by A42, XREAL_1: 7;

          then ||.y1.|| <= (1 + ||.y0.||) by A61, XXREAL_0: 2;

          then ( ||.y1.|| + ||.x0.||) <= ((1 + ||.y0.||) + ||.x0.||) by XREAL_1: 7;

          then (s * ( ||.y1.|| + ||.x0.||)) <= (s * ((1 + ||.y0.||) + ||.x0.||)) by A43, XREAL_1: 64;

          then ((s * ( ||.y1.|| + ||.x0.||)) * K) <= ((s * ((1 + ||.y0.||) + ||.x0.||)) * K) by A32, XREAL_1: 64;

          then ( ||.(f . ((x1 - x0),y1)).|| + ||.(f . (x0,(y1 - y0))).||) <= ((K * s) * (( ||.x0.|| + 1) + ||.y0.||)) by A58, XXREAL_0: 2;

          then ( ||.(f . ((x1 - x0),y1)).|| + ||.(f . (x0,(y1 - y0))).||) <= (KXY0 * (r / KXY0)) by A44, XXREAL_0: 2;

          then

           A64: ( ||.(f . ((x1 - x0),y1)).|| + ||.(f . (x0,(y1 - y0))).||) <= r by A40, XCMPLX_1: 87;

           ||.((f . z1) - (f . z0)).|| <= ( ||.((f . (x1,y1)) - (f . (x0,y1))).|| + ||.((f . (x0,y1)) - (f . (x0,y0))).||) by A47, NORMSP_1:def 1;

          then ||.((f /. z1) - (f /. z0)).|| <= r by A49, A51, A64, XXREAL_0: 2;

          hence ||.((f /. z1) - (f /. z0)).|| < r1 by A35, XXREAL_0: 2;

        end;

        hence thesis by A33, NFCONT_1: 19;

      end;

      hence thesis by A4;

    end;