lopban13.miz



    begin

    reserve X,Y,Z for non trivial RealBanachSpace;

    definition

      let X,Y be RealNormSpace;

      let u be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y));

      :: LOPBAN13:def1

      attr u is invertible means u is one-to-one & ( rng u) = the carrier of Y & (u " ) is Point of ( R_NormSpace_of_BoundedLinearOperators (Y,X));

    end

    definition

      let X,Y be RealNormSpace;

      let u be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y));

      assume

       A1: u is invertible;

      :: LOPBAN13:def2

      func Inv u -> Point of ( R_NormSpace_of_BoundedLinearOperators (Y,X)) equals

      : Def1: (u " );

      correctness by A1;

    end

    theorem :: LOPBAN13:1

    

     LOPBAN410: for X be RealNormSpace, seq be sequence of X, k be Nat holds ||.(( Partial_Sums seq) . k).|| <= (( Partial_Sums ||.seq.||) . k)

    proof

      let X be RealNormSpace, seq be sequence of X;

      defpred P[ Nat] means ||.(( Partial_Sums seq) . $1).|| <= (( Partial_Sums ||.seq.||) . $1);

       A1:

      now

        let k be Nat;

        assume P[k];

        then

         A2: ( ||.(( Partial_Sums seq) . k).|| + ||.(seq . (k + 1)).||) <= ((( Partial_Sums ||.seq.||) . k) + ||.(seq . (k + 1)).||) by XREAL_1: 6;

        

         A3: ||.((( Partial_Sums seq) . k) + (seq . (k + 1))).|| <= ( ||.(( Partial_Sums seq) . k).|| + ||.(seq . (k + 1)).||) by NORMSP_1:def 1;

         ||.(( Partial_Sums seq) . (k + 1)).|| = ||.((( Partial_Sums seq) . k) + (seq . (k + 1))).|| by BHSP_4:def 1;

        then ||.(( Partial_Sums seq) . (k + 1)).|| <= ((( Partial_Sums ||.seq.||) . k) + ||.(seq . (k + 1)).||) by A3, A2, XXREAL_0: 2;

        then ||.(( Partial_Sums seq) . (k + 1)).|| <= ((( Partial_Sums ||.seq.||) . k) + ( ||.seq.|| . (k + 1))) by NORMSP_0:def 4;

        hence P[(k + 1)] by SERIES_1:def 1;

      end;

      (( Partial_Sums ||.seq.||) . 0 ) = ( ||.seq.|| . 0 ) by SERIES_1:def 1

      .= ||.(seq . 0 ).|| by NORMSP_0:def 4;

      then

       A4: P[ 0 ] by BHSP_4:def 1;

      for k be Nat holds P[k] from NAT_1:sch 2( A4, A1);

      hence thesis;

    end;

    theorem :: LOPBAN13:2

    

     LM0: for X be RealBanachSpace, s be sequence of X st s is norm_summable holds ||.( Sum s).|| <= ( Sum ||.s.||)

    proof

      let X be RealBanachSpace, s be sequence of X;

      assume

       A1: s is norm_summable;

      then

       A3: ||.s.|| is summable;

       A5:

      now

        let k be Nat;

        ( ||.( Partial_Sums s).|| . k) = ||.(( Partial_Sums s) . k).|| by NORMSP_0:def 4;

        hence ( ||.( Partial_Sums s).|| . k) <= (( Partial_Sums ||.s.||) . k) by LOPBAN410;

      end;

      

       A6: s is summable by A1;

      then

       A8: ||.( Partial_Sums s).|| is convergent by NORMSP_1: 23;

      ( lim ||.( Partial_Sums s).||) = ||.( Sum s).|| by A6, LOPBAN_1: 20;

      hence ||.( Sum s).|| <= ( Sum ||.s.||) by A3, A5, A8, SEQ_2: 18;

    end;

    theorem :: LOPBAN13:3

    

     LM1: for X be Banach_Algebra, z be Point of X st ||.z.|| < 1 holds (z GeoSeq ) is norm_summable & ||.( Sum (z GeoSeq )).|| <= (1 / (1 - ||.z.||))

    proof

      let X be Banach_Algebra;

      let z be Element of X;

      

       A1: for n be Nat holds ( 0 <= ( ||.(z GeoSeq ).|| . n) & ( ||.(z GeoSeq ).|| . n) <= (( ||.z.|| GeoSeq ) . n))

      proof

        defpred S1[ Nat] means ( 0 <= ( ||.(z GeoSeq ).|| . $1) & ( ||.(z GeoSeq ).|| . $1) <= (( ||.z.|| GeoSeq ) . $1));

        

         A3: for k be Nat st S1[k] holds S1[(k + 1)]

        proof

          let k be Nat;

           ||.(((z GeoSeq ) . k) * z).|| <= ( ||.((z GeoSeq ) . k).|| * ||.z.||) by LOPBAN_2:def 9;

          then

           A4: ||.(((z GeoSeq ) . k) * z).|| <= (( ||.(z GeoSeq ).|| . k) * ||.z.||) by NORMSP_0:def 4;

          assume S1[k];

          then (( ||.(z GeoSeq ).|| . k) * ||.z.||) <= ((( ||.z.|| GeoSeq ) . k) * ||.z.||) by XREAL_1: 64;

          then

           A5: ||.(((z GeoSeq ) . k) * z).|| <= ((( ||.z.|| GeoSeq ) . k) * ||.z.||) by A4, XXREAL_0: 2;

          ( ||.(z GeoSeq ).|| . (k + 1)) = ||.((z GeoSeq ) . (k + 1)).|| by NORMSP_0:def 4

          .= ||.(((z GeoSeq ) . k) * z).|| by LOPBAN_3:def 9;

          hence S1[(k + 1)] by A5, PREPOWER: 3;

        end;

         ||.((z GeoSeq ) . 0 ).|| = ||.( 1. X).|| by LOPBAN_3:def 9

        .= 1 by LOPBAN_2:def 10

        .= (( ||.z.|| GeoSeq ) . 0 ) by PREPOWER: 3;

        then

         A6: S1[ 0 ] by NORMSP_0:def 4;

        for n be Nat holds S1[n] from NAT_1:sch 2( A6, A3);

        hence for n be Nat holds ( 0 <= ( ||.(z GeoSeq ).|| . n) & ( ||.(z GeoSeq ).|| . n) <= (( ||.z.|| GeoSeq ) . n));

      end;

      assume ||.z.|| < 1;

      then |. ||.z.||.| < 1 by ABSVALUE:def 1;

      then

       A7: ( ||.z.|| GeoSeq ) is summable & ( Sum ( ||.z.|| GeoSeq )) = (1 / (1 - ||.z.||)) by SERIES_1: 24;

      then

       A8: ||.(z GeoSeq ).|| is summable & ( Sum ||.(z GeoSeq ).||) <= ( Sum ( ||.z.|| GeoSeq )) by A1, SERIES_1: 20;

      (z GeoSeq ) is norm_summable by A1, A7, SERIES_1: 20;

      then ||.( Sum (z GeoSeq )).|| <= ( Sum ||.(z GeoSeq ).||) by LM0;

      hence thesis by A7, A8, XXREAL_0: 2;

    end;

    theorem :: LOPBAN13:4

    

     LM2: for S be Banach_Algebra, w be Point of S st ||.w.|| < 1 holds (( 1. S) + w) is invertible & (( - w) GeoSeq ) is norm_summable & ((( 1. S) + w) " ) = ( Sum (( - w) GeoSeq )) & ||.((( 1. S) + w) " ).|| <= (1 / (1 - ||.w.||))

    proof

      let S be Banach_Algebra, w be Point of S;

      assume

       A1: ||.w.|| < 1;

      set x = (( 1. S) + w);

      

       A2: ||.(( 1. S) - x).|| = ||.(x - ( 1. S)).|| by NORMSP_1: 7

      .= ||.w.|| by RLVECT_4: 1;

      then

       A3: x is invertible & (x " ) = ( Sum ((( 1. S) - x) GeoSeq )) by A1, LOPBAN_3: 42;

      (( 1. S) - x) = ((( 1. S) - ( 1. S)) - w) by RLVECT_1: 27

      .= (( 0. S) - w) by RLVECT_1: 15

      .= ( - w) by RLVECT_1: 14;

      hence thesis by A1, A2, A3, LM1;

    end;

    theorem :: LOPBAN13:5

    for X be non trivial RealBanachSpace, v1,v2 be Lipschitzian LinearOperator of X, X, w1,w2 be Point of ( R_Normed_Algebra_of_BoundedLinearOperators X), a be Real st v1 = w1 & v2 = w2 holds (v1 * v2) = (w1 * w2) & (v1 + v2) = (w1 + w2) & (a (#) v1) = (a * w1)

    proof

      let X be non trivial RealBanachSpace, v1,v2 be Lipschitzian LinearOperator of X, X, w1,w2 be Point of ( R_Normed_Algebra_of_BoundedLinearOperators X), a be Real;

      set S = ( R_Normed_Algebra_of_BoundedLinearOperators X);

      assume

       A1: v1 = w1 & v2 = w2;

      reconsider zw1 = w1, zw2 = w2 as Element of ( BoundedLinearOperators (X,X));

      v1 = ( modetrans (v1,X,X)) & v2 = ( modetrans (v2,X,X)) by LOPBAN_1: 29;

      

      hence (v1 * v2) = (zw1 * zw2) by A1

      .= (w1 * w2) by LOPBAN_2:def 4;

      reconsider zw1 = w1, zw2 = w2 as Point of ( R_NormSpace_of_BoundedLinearOperators (X,X));

      reconsider zw12 = (zw1 + zw2) as Point of ( R_NormSpace_of_BoundedLinearOperators (X,X));

      zw12 is Lipschitzian LinearOperator of X, X by LOPBAN_1:def 9;

      then

       A4: ( dom zw12) = the carrier of X by FUNCT_2:def 1;

      

       A5: ( dom (v1 + v2)) = (( dom v1) /\ ( dom v2)) by VFUNCT_1:def 1

      .= (the carrier of X /\ ( dom v2)) by FUNCT_2:def 1

      .= (the carrier of X /\ the carrier of X) by FUNCT_2:def 1

      .= the carrier of X;

      for s be object st s in ( dom (v1 + v2)) holds ((v1 + v2) . s) = (zw12 . s)

      proof

        let s be object;

        assume

         A6: s in ( dom (v1 + v2));

        then

        reconsider d = s as Point of X;

        

        thus ((v1 + v2) . s) = ((v1 + v2) /. d) by A5, PARTFUN1:def 6

        .= ((v1 /. d) + (v2 /. d)) by A6, VFUNCT_1:def 1

        .= (zw12 . s) by A1, LOPBAN_1: 35;

      end;

      hence (v1 + v2) = (w1 + w2) by A4, A5, FUNCT_1: 2;

      reconsider zw12 = (a * zw1) as Point of ( R_NormSpace_of_BoundedLinearOperators (X,X));

      zw12 is Lipschitzian LinearOperator of X, X by LOPBAN_1:def 9;

      then

       A8: ( dom zw12) = the carrier of X by FUNCT_2:def 1;

      

       A9: ( dom (a (#) v1)) = ( dom v1) by VFUNCT_1:def 4

      .= the carrier of X by FUNCT_2:def 1;

      for s be object st s in ( dom (a (#) v1)) holds ((a (#) v1) . s) = (zw12 . s)

      proof

        let s be object;

        assume

         A10: s in ( dom (a (#) v1));

        then

        reconsider d = s as Point of X;

        

        thus ((a (#) v1) . s) = ((a (#) v1) /. d) by A9, PARTFUN1:def 6

        .= (a * (v1 /. d)) by A10, VFUNCT_1:def 4

        .= (zw12 . s) by A1, LOPBAN_1: 36;

      end;

      hence (a (#) v1) = (a * w1) by A8, A9, FUNCT_1: 2;

    end;

    theorem :: LOPBAN13:6

    for X be non trivial RealBanachSpace, v1,v2 be Point of ( R_NormSpace_of_BoundedLinearOperators (X,X)), w1,w2 be Point of ( R_Normed_Algebra_of_BoundedLinearOperators X), a be Real st v1 = w1 & v2 = w2 holds (v1 + v2) = (w1 + w2) & (a * v1) = (a * w1);

    theorem :: LOPBAN13:7

    for X be non trivial RealBanachSpace, v1,v2 be Point of ( R_NormSpace_of_BoundedLinearOperators (X,X)), w1,w2 be Point of ( R_Normed_Algebra_of_BoundedLinearOperators X) st v1 = w1 & v2 = w2 holds (v1 * v2) = (w1 * w2)

    proof

      let X be non trivial RealBanachSpace, v1,v2 be Point of ( R_NormSpace_of_BoundedLinearOperators (X,X)), w1,w2 be Point of ( R_Normed_Algebra_of_BoundedLinearOperators X);

      set S = ( R_Normed_Algebra_of_BoundedLinearOperators X);

      assume

       A1: v1 = w1 & v2 = w2;

      reconsider zw1 = w1, zw2 = w2 as Element of ( BoundedLinearOperators (X,X));

      

      thus (v1 * v2) = (zw1 * zw2) by A1

      .= (w1 * w2) by LOPBAN_2:def 4;

    end;

    theorem :: LOPBAN13:8

    

     LM4: for X be non trivial RealBanachSpace, v be Point of ( R_NormSpace_of_BoundedLinearOperators (X,X)), w be Point of ( R_Normed_Algebra_of_BoundedLinearOperators X) st v = w holds (v is invertible iff w is invertible) & (w is invertible implies (v " ) = (w " ))

    proof

      let X be non trivial RealBanachSpace, v be Point of ( R_NormSpace_of_BoundedLinearOperators (X,X)), w be Point of ( R_Normed_Algebra_of_BoundedLinearOperators X);

      set S = ( R_Normed_Algebra_of_BoundedLinearOperators X);

      assume

       A1: v = w;

      

       A2: v is Lipschitzian LinearOperator of X, X by LOPBAN_1:def 9;

      

       A4: v is invertible implies w is invertible

      proof

        assume

         A5: v is invertible;

        then

        reconsider x = (v " ) as Point of S;

        

         A7: (v " ) is Lipschitzian LinearOperator of X, X by A5, LOPBAN_1:def 9;

        reconsider zx = x, zv = v as Element of ( BoundedLinearOperators (X,X));

        ( dom v) = the carrier of X & ( rng v) = the carrier of X by A2, A5, FUNCT_2:def 1;

        then

         A9: ((v " ) * v) = ( id X) & (v * (v " )) = ( id X) by A5, FUNCT_1: 39;

        

         A10: (v " ) = ( modetrans ((v " ),X,X)) & v = ( modetrans (v,X,X)) by A2, A7, LOPBAN_1: 29;

        

        then

         A11: ((v " ) * v) = (zx * zv)

        .= (x * w) by A1, LOPBAN_2:def 4;

        (v * (v " )) = (zv * zx) by A10

        .= (w * x) by A1, LOPBAN_2:def 4;

        hence w is invertible by A9, A11;

      end;

      w is invertible implies v is invertible & (v " ) = (w " )

      proof

        assume

         A13: w is invertible;

        

         A14: v is Lipschitzian LinearOperator of X, X by LOPBAN_1:def 9;

        reconsider y = (w " ) as Lipschitzian LinearOperator of X, X by LOPBAN_1:def 9;

        reconsider zy = y, zw = w as Element of ( BoundedLinearOperators (X,X));

        

         A15: y = ( modetrans (y,X,X)) & v = ( modetrans (v,X,X)) by A14, LOPBAN_1: 29;

        

        then

         A16: (y * v) = (zy * zw) by A1

        .= ((w " ) * w) by LOPBAN_2:def 4

        .= ( id X) by A13, LOPBAN_3:def 8;

        

         A17: (v * y) = (zw * zy) by A1, A15

        .= (w * (w " )) by LOPBAN_2:def 4

        .= ( id X) by A13, LOPBAN_3:def 8;

        reconsider y0 = y, v0 = v as Function of the carrier of X, the carrier of X by LOPBAN_1:def 9;

        

         A18: ( dom v) = the carrier of X by A14, FUNCT_2:def 1;

        

         A19: v0 is one-to-one & v0 is onto by A16, A17, FUNCT_2: 23;

        then ( dom y) = ( rng v) by FUNCT_2:def 1;

        hence thesis by A16, A18, A19, FUNCT_1: 41;

      end;

      hence thesis by A4;

    end;

    theorem :: LOPBAN13:9

    

     Th1: for v,I be Point of ( R_NormSpace_of_BoundedLinearOperators (X,X)) st I = ( id X) & ||.v.|| < 1 holds (I + v) is invertible & ||.( Inv (I + v)).|| <= (1 / (1 - ||.v.||)) & ex w be Point of ( R_Normed_Algebra_of_BoundedLinearOperators X) st w = v & (( - w) GeoSeq ) is norm_summable & ( Inv (I + v)) = ( Sum (( - w) GeoSeq ))

    proof

      let v,I be Point of ( R_NormSpace_of_BoundedLinearOperators (X,X));

      assume that

       A1: I = ( id X) and

       A2: ||.v.|| < 1;

      set S = ( R_Normed_Algebra_of_BoundedLinearOperators X);

      reconsider w = v as Point of S;

      set x = (( 1. S) + w);

       ||.w.|| < 1 by A2;

      then

       A3: x is invertible & (( - w) GeoSeq ) is norm_summable & (x " ) = ( Sum (( - w) GeoSeq )) & ||.(x " ).|| <= (1 / (1 - ||.w.||)) by LM2;

      hence

       A6: (I + v) is invertible by A1, LM4;

      

       A7: ((I + v) " ) = (x " ) by A1, A3, LM4;

      hence ||.( Inv (I + v)).|| <= (1 / (1 - ||.v.||)) by A3, A6, Def1;

      thus thesis by A3, A6, A7, Def1;

    end;

    theorem :: LOPBAN13:10

    

     RELAT136: for X,Y,Z,W be RealNormSpace, f be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)), g be Point of ( R_NormSpace_of_BoundedLinearOperators (Y,Z)), h be Point of ( R_NormSpace_of_BoundedLinearOperators (Z,W)) holds (h * (g * f)) = ((h * g) * f)

    proof

      let X,Y,Z,W be RealNormSpace, f be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)), g be Point of ( R_NormSpace_of_BoundedLinearOperators (Y,Z)), h be Point of ( R_NormSpace_of_BoundedLinearOperators (Z,W));

      

       A2: (h * g) is Lipschitzian LinearOperator of Y, W by LOPBAN_2: 2;

      (g * f) is Lipschitzian LinearOperator of X, Z by LOPBAN_2: 2;

      

      hence (h * (g * f)) = (( modetrans (h,Z,W)) * (( modetrans (g,Y,Z)) * ( modetrans (f,X,Y)))) by LOPBAN_1: 29

      .= ((( modetrans (h,Z,W)) * ( modetrans (g,Y,Z))) * ( modetrans (f,X,Y))) by RELAT_1: 36

      .= ((h * g) * f) by A2, LOPBAN_1: 29;

    end;

    theorem :: LOPBAN13:11

    

     FUNCT229: for X,Y be RealNormSpace, f be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)) st f is one-to-one & ( rng f) = the carrier of Y holds ((f " ) * f) = ( id X) & (f * (f " )) = ( id Y)

    proof

      let X,Y be RealNormSpace, f be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y));

      assume

       A1: f is one-to-one & ( rng f) = the carrier of Y;

      

       A2: f is Lipschitzian LinearOperator of X, Y by LOPBAN_1:def 9;

      hence ((f " ) * f) = ( id X) by A1, FUNCT_2: 29;

      thus (f * (f " )) = ( id Y) by A1, A2, FUNCT_2: 29;

    end;

    theorem :: LOPBAN13:12

    

     LM50: for u be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)) st u is invertible holds 0 < ||.u.|| & 0 < ||.( Inv u).||

    proof

      let u be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y));

      assume

       A1: u is invertible;

      set S = ( R_Normed_Algebra_of_BoundedLinearOperators X);

      reconsider Lu = u as Lipschitzian LinearOperator of X, Y by LOPBAN_1:def 9;

      reconsider LInvu = ( Inv u) as Lipschitzian LinearOperator of Y, X by LOPBAN_1:def 9;

      

       A8: (( BoundedLinearOperatorsNorm (X,X)) . (LInvu * Lu)) <= ((( BoundedLinearOperatorsNorm (Y,X)) . LInvu) * (( BoundedLinearOperatorsNorm (X,Y)) . Lu)) by LOPBAN_2: 2;

      LInvu = (u " ) by A1, Def1;

      

      then (( BoundedLinearOperatorsNorm (X,X)) . (LInvu * Lu)) = ||.( 1. S).|| by A1, FUNCT_2: 29

      .= 1 by LOPBAN_2:def 10;

      then ||.( Inv u).|| <> 0 & ||.u.|| <> 0 by A8;

      hence 0 < ||.u.|| & 0 < ||.( Inv u).||;

    end;

    theorem :: LOPBAN13:13

    

     Th2: for u,v be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)) st u is invertible & ||.v.|| < (1 / ||.( Inv u).||) holds (u + v) is invertible & ||.( Inv (u + v)).|| <= (1 / ((1 / ||.( Inv u).||) - ||.v.||)) & ex w be Point of ( R_Normed_Algebra_of_BoundedLinearOperators X), s,I be Point of ( R_NormSpace_of_BoundedLinearOperators (X,X)) st w = (( Inv u) * v) & s = w & I = ( id X) & ||.s.|| < 1 & (( - w) GeoSeq ) is norm_summable & (I + s) is invertible & ||.( Inv (I + s)).|| <= (1 / (1 - ||.s.||)) & ( Inv (I + s)) = ( Sum (( - w) GeoSeq )) & ( Inv (u + v)) = (( Inv (I + s)) * ( Inv u))

    proof

      let u,v be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y));

      assume that

       A1: u is invertible and

       A2: ||.v.|| < (1 / ||.( Inv u).||);

      set S = ( R_Normed_Algebra_of_BoundedLinearOperators X);

      ( 1. S) = ( id X);

      then

      reconsider I = ( id X) as Point of ( R_NormSpace_of_BoundedLinearOperators (X,X));

      reconsider Is = I as Point of S;

      

       A6: u is Lipschitzian LinearOperator of X, Y by LOPBAN_1:def 9;

      

       A7: v is Lipschitzian LinearOperator of X, Y by LOPBAN_1:def 9;

      reconsider udv = (( Inv u) * v) as Point of ( R_NormSpace_of_BoundedLinearOperators (X,X));

      reconsider udv2 = udv as Point of S;

      reconsider Lu = u, Lv = v as Lipschitzian LinearOperator of X, Y by LOPBAN_1:def 9;

      reconsider LInvu = ( Inv u) as Lipschitzian LinearOperator of Y, X by LOPBAN_1:def 9;

      

       A14: ( modetrans (LInvu,Y,X)) = LInvu & ( modetrans (Lv,X,Y)) = Lv by LOPBAN_1: 29;

      then

       A15: ||.udv.|| <= ( ||.( Inv u).|| * ||.v.||) by LOPBAN_2: 2;

      LInvu = (u " ) by A1, Def1;

      

      then

       A17: (( BoundedLinearOperatorsNorm (X,X)) . (LInvu * Lu)) = ||.( 1. S).|| by A1, FUNCT_2: 29

      .= 1 by LOPBAN_2:def 10;

      

       A18: ||.( Inv u).|| <> 0

      proof

        assume ||.( Inv u).|| = 0 ;

        then 1 <= ( 0 * (( BoundedLinearOperatorsNorm (X,Y)) . u)) by A17, LOPBAN_2: 2;

        hence contradiction;

      end;

      then ( ||.( Inv u).|| * ||.v.||) < ( ||.( Inv u).|| * (1 / ||.( Inv u).||)) by A2, XREAL_1: 68;

      then

       A20: ( ||.( Inv u).|| * ||.v.||) < 1 by A18, XCMPLX_1: 106;

      then

       A21: ||.udv.|| < 1 by A15, XXREAL_0: 2;

      then

       A22: (I + udv) is invertible & ||.( Inv (I + udv)).|| <= (1 / (1 - ||.udv.||)) & ex w be Point of ( R_Normed_Algebra_of_BoundedLinearOperators X) st w = udv & (( - w) GeoSeq ) is norm_summable & ( Inv (I + udv)) = ( Sum (( - w) GeoSeq )) by Th1;

      

       A23: (u + v) is Lipschitzian LinearOperator of X, Y by LOPBAN_1:def 9;

      then

       A24: ( modetrans ((u + v),X,Y)) = (u + v) by LOPBAN_1: 29;

      

       A25: (I + udv) is Lipschitzian LinearOperator of X, X by LOPBAN_1:def 9;

      then

       A26: ( modetrans ((I + udv),X,X)) = (I + udv) by LOPBAN_1: 29;

      

       A27: ( modetrans (u,X,Y)) = u by A6, LOPBAN_1: 29;

      

       A28: for x be Element of the carrier of X holds ((u + v) . x) = ((u * (I + udv)) . x)

      proof

        let x be Element of the carrier of X;

        

         A33: ((u * (I + udv)) . x) = (( modetrans (u,X,Y)) . (( modetrans ((I + udv),X,X)) . x)) by FUNCT_2: 15

        .= (u . ((I + udv) . x)) by A25, A27, LOPBAN_1: 29;

        

         A35: ((I + udv) . x) = ((( id X) . x) + (udv . x)) by LOPBAN_1: 35

        .= (x + (udv . x));

        Lu is additive;

        then

         A37: (Lu . ((I + udv) . x)) = ((Lu . x) + (Lu . (udv . x))) by A35;

        

         A39: ( Inv u) is Lipschitzian LinearOperator of Y, X by LOPBAN_1:def 9;

        

         A40: ( modetrans (v,X,Y)) = v by A7, LOPBAN_1: 29;

        (u . (udv . x)) = (u . (( modetrans (( Inv u),Y,X)) . (( modetrans (v,X,Y)) . x))) by FUNCT_2: 15

        .= (u . (( Inv u) . (v . x))) by A39, A40, LOPBAN_1: 29

        .= (u . ((u " ) . (v . x))) by A1, Def1

        .= (v . x) by A1, FUNCT_1: 35;

        hence thesis by A33, A37, LOPBAN_1: 35;

      end;

      then

       A43: (u + v) is one-to-one by A1, A22, A23, A26, A27, FUNCT_2:def 7;

      

       A44: ( modetrans (u,X,Y)) is onto by A1, A6, LOPBAN_1: 29;

      ( modetrans ((I + udv),X,X)) is onto by A22, A25, LOPBAN_1: 29;

      then (( modetrans (u,X,Y)) * ( modetrans ((I + udv),X,X))) is onto by A44, FUNCT_2: 27;

      then

       A46: ( rng (u + v)) = the carrier of Y by A23, A28, FUNCT_2:def 7;

      set Iuv = (( Inv (I + udv)) * ( Inv u));

      Iuv is Lipschitzian LinearOperator of Y, X by LOPBAN_2: 2;

      then

       A48: ( modetrans (Iuv,Y,X)) = Iuv by LOPBAN_1: 29;

      ( Inv u) is Lipschitzian LinearOperator of Y, X by LOPBAN_1:def 9;

      then

       A49: ( modetrans (( Inv u),Y,X)) = ( Inv u) by LOPBAN_1: 29;

      

       B49: ( Inv (I + udv)) is Lipschitzian LinearOperator of X, X by LOPBAN_1:def 9;

      then

       A50: ( modetrans (( Inv (I + udv)),X,X)) = ( Inv (I + udv)) by LOPBAN_1: 29;

      

       A51: ( modetrans (((I + udv) " ),X,X)) = ( modetrans (( Inv (I + udv)),X,X)) by A21, Def1, Th1

      .= ( Inv (I + udv)) by B49, LOPBAN_1: 29

      .= ((I + udv) " ) by A21, Def1, Th1;

      ( modetrans (( Inv u),Y,X)) = (u " ) by A1, A49, Def1;

      

      then

       A53: (( Inv u) * u) = ((u " ) * u) by A6, LOPBAN_1: 29

      .= ( id X) by A1, FUNCT229;

      (( Inv u) * u) is Lipschitzian LinearOperator of X, X by LOPBAN_2: 2;

      then ( modetrans ((( Inv u) * u),X,X)) = ( id X) by A53, LOPBAN_1: 29;

      

      then

       A55: ((( Inv u) * u) * (I + udv)) = (( id X) * (I + udv)) by A25, LOPBAN_1: 29

      .= (I + udv) by A25, FUNCT_2: 17;

      

       A56: (( modetrans (Iuv,Y,X)) * ( modetrans ((u + v),X,Y))) = ((( Inv (I + udv)) * ( Inv u)) * (u + v))

      .= (( Inv (I + udv)) * (( Inv u) * (u + v))) by RELAT136

      .= (( Inv (I + udv)) * (( Inv u) * (u * (I + udv)))) by A23, A28, FUNCT_2:def 7

      .= (( Inv (I + udv)) * (I + udv)) by A55, RELAT136

      .= (( modetrans (((I + udv) " ),X,X)) * ( modetrans ((I + udv),X,X))) by A21, Def1, Th1

      .= (((I + udv) " ) * (I + udv)) by A25, A51, LOPBAN_1: 29

      .= ( id X) by A22, FUNCT229;

      then

       A57: (( modetrans ((u + v),X,Y)) " ) = ( modetrans (Iuv,Y,X)) by A24, A43, A46, FUNCT_2: 30;

      thus

       A58: (u + v) is invertible by A24, A43, A46, A48, A56, FUNCT_2: 30;

      reconsider Iuvp = Iuv as Point of ( R_NormSpace_of_BoundedLinearOperators (Y,X));

      

       A59: (( BoundedLinearOperatorsNorm (Y,X)) . Iuv) <= ((( BoundedLinearOperatorsNorm (X,X)) . ( modetrans (( Inv (I + udv)),X,X))) * (( BoundedLinearOperatorsNorm (Y,X)) . ( modetrans (( Inv u),Y,X)))) by LOPBAN_2: 2;

      ((( BoundedLinearOperatorsNorm (X,X)) . ( Inv (I + udv))) * (( BoundedLinearOperatorsNorm (Y,X)) . ( Inv u))) <= ((1 / (1 - ||.udv.||)) * ||.( Inv u).||) by A22, XREAL_1: 64;

      then

       A64: ||.Iuvp.|| <= ((1 / (1 - ||.udv.||)) * ||.( Inv u).||) by A49, A50, A59, XXREAL_0: 2;

      

       A65: (1 - ( ||.( Inv u).|| * ||.v.||)) <= (1 - ||.udv.||) by A14, LOPBAN_2: 2, XREAL_1: 10;

       0 < (1 - ( ||.( Inv u).|| * ||.v.||)) by A20, XREAL_1: 50;

      then (1 / (1 - ||.udv.||)) <= (1 / (1 - ( ||.( Inv u).|| * ||.v.||))) by A65, XREAL_1: 118;

      then ((1 / (1 - ||.udv.||)) * ||.( Inv u).||) <= ((1 / (1 - ( ||.( Inv u).|| * ||.v.||))) * ||.( Inv u).||) by XREAL_1: 64;

      then

       A67: ((1 / (1 - ||.udv.||)) * ||.( Inv u).||) <= ( ||.( Inv u).|| / (1 - ( ||.( Inv u).|| * ||.v.||))) by XCMPLX_1: 99;

      ((1 - ( ||.( Inv u).|| * ||.v.||)) / ||.( Inv u).||) = ((1 / ||.( Inv u).||) - (( ||.( Inv u).|| * ||.v.||) / ||.( Inv u).||)) by XCMPLX_1: 120

      .= ((1 / ||.( Inv u).||) - ||.v.||) by A18, XCMPLX_1: 89;

      then (1 / ((1 / ||.( Inv u).||) - ||.v.||)) = ( ||.( Inv u).|| / (1 - ( ||.( Inv u).|| * ||.v.||))) by XCMPLX_1: 57;

      then ||.Iuvp.|| <= (1 / ((1 / ||.( Inv u).||) - ||.v.||)) by A64, A67, XXREAL_0: 2;

      hence ||.( Inv (u + v)).|| <= (1 / ((1 / ||.( Inv u).||) - ||.v.||)) by A24, A48, A57, A58, Def1;

      consider w be Point of ( R_Normed_Algebra_of_BoundedLinearOperators X) such that

       A70: w = udv & (( - w) GeoSeq ) is norm_summable & ( Inv (I + udv)) = ( Sum (( - w) GeoSeq )) by A21, Th1;

      reconsider S = ( Sum (( - w) GeoSeq )) as Point of ( R_NormSpace_of_BoundedLinearOperators (X,X));

      take w, udv, I;

      thus w = (( Inv u) * v) & udv = w & I = ( id X) & ||.udv.|| < 1 & (( - w) GeoSeq ) is norm_summable & (I + udv) is invertible & ||.( Inv (I + udv)).|| <= (1 / (1 - ||.udv.||)) & ( Inv (I + udv)) = ( Sum (( - w) GeoSeq )) by A21, A70, Th1;

      thus ( Inv (u + v)) = (( Inv (I + udv)) * ( Inv u)) by A24, A48, A57, A58, Def1;

    end;

    theorem :: LOPBAN13:14

    

     Th3: for S be Subset of ( R_NormSpace_of_BoundedLinearOperators (X,Y)) st S = { v where v be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)) : v is invertible } holds S is open

    proof

      let S be Subset of ( R_NormSpace_of_BoundedLinearOperators (X,Y));

      assume

       A1: S = { v where v be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)) : v is invertible };

      set P = ( R_NormSpace_of_BoundedLinearOperators (X,Y));

      for u be Point of P st u in S holds ex r be Real st r > 0 & ( Ball (u,r)) c= S

      proof

        let u be Point of P;

        assume u in S;

        then

         A2: ex v be Point of P st u = v & v is invertible by A1;

        then

         A3: 0 < ||.( Inv u).|| by LM50;

        set r = (1 / ||.( Inv u).||);

        take r;

        thus 0 < r by A3, XREAL_1: 139;

        now

          let x be object;

          assume x in ( Ball (u,r));

          then x in { y where y be Point of P : ||.(y - u).|| < r } by NDIFF_8: 17;

          then

          consider v be Point of P such that

           A4: x = v & ||.(v - u).|| < r;

          v = (u + (v - u)) by RLVECT_4: 1;

          then v is invertible by A2, A4, Th2;

          hence x in S by A1, A4;

        end;

        hence ( Ball (u,r)) c= S by TARSKI:def 3;

      end;

      hence S is open by NDIFF_8: 20;

    end;

    definition

      let X, Y;

      :: LOPBAN13:def3

      func InvertibleOperators (X,Y) -> open Subset of ( R_NormSpace_of_BoundedLinearOperators (X,Y)) equals { v where v be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)) : v is invertible };

      correctness

      proof

        set S = { v where v be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)) : v is invertible };

        now

          let x be object;

          assume x in S;

          then ex v be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)) st x = v & v is invertible;

          hence x in the carrier of ( R_NormSpace_of_BoundedLinearOperators (X,Y));

        end;

        then

        reconsider S as Subset of ( R_NormSpace_of_BoundedLinearOperators (X,Y)) by TARSKI:def 3;

        S is open by Th3;

        hence thesis;

      end;

    end

    theorem :: LOPBAN13:15

    

     LM60: for u be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)) st u is invertible holds ( Inv u) is invertible & ( Inv ( Inv u)) = u

    proof

      let u be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y));

      assume

       A1: u is invertible;

      then

       A3: ( Inv u) = (u " ) by Def1;

      reconsider Lu = u as Lipschitzian LinearOperator of X, Y by LOPBAN_1:def 9;

      

       A5: ( rng ( Inv u)) = ( dom Lu) by A1, A3, FUNCT_1: 33

      .= the carrier of X by FUNCT_2:def 1;

      

       A6: (( Inv u) " ) = u by A1, A3, FUNCT_1: 43;

      thus ( Inv u) is invertible by A1, A3, A5, FUNCT_1: 43;

      hence ( Inv ( Inv u)) = u by A6, Def1;

    end;

    theorem :: LOPBAN13:16

    

     LM70: ex I be Function of ( InvertibleOperators (X,Y)), ( InvertibleOperators (Y,X)) st I is one-to-one & I is onto & for u be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)) st u in ( InvertibleOperators (X,Y)) holds (I . u) = ( Inv u)

    proof

      set S = ( R_NormSpace_of_BoundedLinearOperators (X,Y));

      defpred P1[ object, object] means ex u be Point of S st $1 = u & $2 = ( Inv u);

      

       A1: for x be object st x in ( InvertibleOperators (X,Y)) holds ex y be object st y in ( InvertibleOperators (Y,X)) & P1[x, y]

      proof

        let x be object;

        assume x in ( InvertibleOperators (X,Y));

        then

        consider u be Point of S such that

         A2: x = u & u is invertible;

        take y = ( Inv u);

        y is invertible by A2, LM60;

        hence y in ( InvertibleOperators (Y,X));

        thus P1[x, y] by A2;

      end;

      consider I be Function of ( InvertibleOperators (X,Y)), ( InvertibleOperators (Y,X)) such that

       A3: for x be object st x in ( InvertibleOperators (X,Y)) holds P1[x, (I . x)] from FUNCT_2:sch 1( A1);

      take I;

      

       A4: for u be Point of S st u in ( InvertibleOperators (X,Y)) holds (I . u) = ( Inv u)

      proof

        let u be Point of S;

        assume u in ( InvertibleOperators (X,Y));

        then P1[u, (I . u)] by A3;

        hence (I . u) = ( Inv u);

      end;

      

       A5: ( InvertibleOperators (X,Y)) <> {} implies ( InvertibleOperators (Y,X)) <> {}

      proof

        assume ( InvertibleOperators (X,Y)) <> {} ;

        then

        consider x be object such that

         A6: x in ( InvertibleOperators (X,Y)) by XBOOLE_0:def 1;

        consider u be Point of S such that

         A7: x = u & u is invertible by A6;

        ( Inv u) is invertible by A7, LM60;

        then ( Inv u) in ( InvertibleOperators (Y,X));

        hence ( InvertibleOperators (Y,X)) <> {} ;

      end;

      

       B7: for x1,x2 be object st x1 in ( InvertibleOperators (X,Y)) & x2 in ( InvertibleOperators (X,Y)) & (I . x1) = (I . x2) holds x1 = x2

      proof

        let x1,x2 be object;

        assume that

         A8: x1 in ( InvertibleOperators (X,Y)) & x2 in ( InvertibleOperators (X,Y)) and

         A9: (I . x1) = (I . x2);

        reconsider u1 = x1, u2 = x2 as Point of S by A8;

        

         A10: (ex v1 be Point of S st u1 = v1 & v1 is invertible) & (ex v2 be Point of S st u2 = v2 & v2 is invertible) by A8;

        

         A11: (I . u1) = ( Inv u1) by A4, A8;

        u1 = ( Inv ( Inv u1)) by A10, LM60

        .= ( Inv ( Inv u2)) by A4, A8, A9, A11

        .= u2 by A10, LM60;

        hence x1 = x2;

      end;

      now

        let y be object;

        assume y in ( InvertibleOperators (Y,X));

        then

        consider v be Point of ( R_NormSpace_of_BoundedLinearOperators (Y,X)) such that

         A15: y = v & v is invertible;

        ( Inv v) is invertible by A15, LM60;

        then

         A16: ( Inv v) in ( InvertibleOperators (X,Y));

        ( Inv ( Inv v)) = v by A15, LM60;

        then y = (I . ( Inv v)) by A4, A15, A16;

        hence y in ( rng I) by A5, A16, FUNCT_2: 4;

      end;

      then ( InvertibleOperators (Y,X)) c= ( rng I) by TARSKI:def 3;

      hence thesis by A4, A5, B7, FUNCT_2: 19, XBOOLE_0:def 10;

    end;

    theorem :: LOPBAN13:17

    

     LMTh2: for u,v be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)) st u is invertible & ||.(v - u).|| < (1 / ||.( Inv u).||) holds v is invertible & ||.( Inv v).|| <= (1 / ((1 / ||.( Inv u).||) - ||.(v - u).||)) & ex w be Point of ( R_Normed_Algebra_of_BoundedLinearOperators X), s,I be Point of ( R_NormSpace_of_BoundedLinearOperators (X,X)) st w = (( Inv u) * (v - u)) & s = w & I = ( id X) & ||.s.|| < 1 & (( - w) GeoSeq ) is norm_summable & (I + s) is invertible & ||.( Inv (I + s)).|| <= (1 / (1 - ||.s.||)) & ( Inv (I + s)) = ( Sum (( - w) GeoSeq )) & ( Inv v) = (( Inv (I + s)) * ( Inv u))

    proof

      let u,v be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y));

      assume

       A1: u is invertible & ||.(v - u).|| < (1 / ||.( Inv u).||);

      set vu = (v - u);

      v = (u + vu) by RLVECT_4: 1;

      hence thesis by A1, Th2;

    end;

    begin

    theorem :: LOPBAN13:18

    

     NRM: for X,Y,Z be RealNormSpace, u be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)), v be Point of ( R_NormSpace_of_BoundedLinearOperators (Y,Z)), w be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Z)) st w = (v * u) holds ||.w.|| <= ( ||.v.|| * ||.u.||)

    proof

      let X,Y,Z be RealNormSpace, u be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)), v be Point of ( R_NormSpace_of_BoundedLinearOperators (Y,Z)), w be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Z));

      assume

       A2: w = (v * u);

      ( modetrans (v,Y,Z)) = v & ( modetrans (u,X,Y)) = u by LOPBAN_1:def 11;

      hence ||.w.|| <= ( ||.v.|| * ||.u.||) by A2, LOPBAN_2: 2;

    end;

    theorem :: LOPBAN13:19

    

     LM100: for X,Y,Z be RealNormSpace, u,v be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)), w be Point of ( R_NormSpace_of_BoundedLinearOperators (Y,Z)) holds (w * (u - v)) = ((w * u) - (w * v)) & (w * (u + v)) = ((w * u) + (w * v))

    proof

      let X,Y,Z be RealNormSpace, u,v be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)), w be Point of ( R_NormSpace_of_BoundedLinearOperators (Y,Z));

      

       A2: ( modetrans (u,X,Y)) = u by LOPBAN_1:def 11;

      for x be Point of X holds ((w * (u - v)) . x) = (((w * u) . x) - ((w * v) . x))

      proof

        let x be Point of X;

        

         A6: ( modetrans (w,Y,Z)) is additive;

        

        thus ((w * (u - v)) . x) = (( modetrans (w,Y,Z)) . (( modetrans ((u - v),X,Y)) . x)) by FUNCT_2: 15

        .= (( modetrans (w,Y,Z)) . ((u - v) . x)) by LOPBAN_1:def 11

        .= (( modetrans (w,Y,Z)) . ((u . x) - (v . x))) by LOPBAN_1: 40

        .= ((( modetrans (w,Y,Z)) . (u . x)) + (( modetrans (w,Y,Z)) . ( - (v . x)))) by A6

        .= ((( modetrans (w,Y,Z)) . (u . x)) + (( modetrans (w,Y,Z)) . (( - 1) * (v . x)))) by RLVECT_1: 16

        .= ((( modetrans (w,Y,Z)) . (u . x)) + (( - 1) * (( modetrans (w,Y,Z)) . (v . x)))) by LOPBAN_1:def 5

        .= ((( modetrans (w,Y,Z)) . (u . x)) - (( modetrans (w,Y,Z)) . (v . x))) by RLVECT_1: 16

        .= ((( modetrans (w,Y,Z)) . (( modetrans (u,X,Y)) . x)) - (( modetrans (w,Y,Z)) . (( modetrans (v,X,Y)) . x))) by A2, LOPBAN_1:def 11

        .= (((( modetrans (w,Y,Z)) * ( modetrans (u,X,Y))) . x) - (( modetrans (w,Y,Z)) . (( modetrans (v,X,Y)) . x))) by FUNCT_2: 15

        .= (((w * u) . x) - ((w * v) . x)) by FUNCT_2: 15;

      end;

      hence (w * (u - v)) = ((w * u) - (w * v)) by LOPBAN_1: 40;

      for x be Point of X holds ((w * (u + v)) . x) = (((w * u) . x) + ((w * v) . x))

      proof

        let x be Point of X;

        

         A7: ( modetrans (w,Y,Z)) is additive;

        

        thus ((w * (u + v)) . x) = (( modetrans (w,Y,Z)) . (( modetrans ((u + v),X,Y)) . x)) by FUNCT_2: 15

        .= (( modetrans (w,Y,Z)) . ((u + v) . x)) by LOPBAN_1:def 11

        .= (( modetrans (w,Y,Z)) . ((u . x) + (v . x))) by LOPBAN_1: 35

        .= ((( modetrans (w,Y,Z)) . (u . x)) + (( modetrans (w,Y,Z)) . (v . x))) by A7

        .= ((( modetrans (w,Y,Z)) . (( modetrans (u,X,Y)) . x)) + (( modetrans (w,Y,Z)) . (( modetrans (v,X,Y)) . x))) by A2, LOPBAN_1:def 11

        .= (((( modetrans (w,Y,Z)) * ( modetrans (u,X,Y))) . x) + (( modetrans (w,Y,Z)) . (( modetrans (v,X,Y)) . x))) by FUNCT_2: 15

        .= (((w * u) . x) + ((w * v) . x)) by FUNCT_2: 15;

      end;

      hence (w * (u + v)) = ((w * u) + (w * v)) by LOPBAN_1: 35;

    end;

    theorem :: LOPBAN13:20

    

     LM200: for X,Y,Z be RealNormSpace, w be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)), u,v be Point of ( R_NormSpace_of_BoundedLinearOperators (Y,Z)) holds ((u - v) * w) = ((u * w) - (v * w)) & ((u + v) * w) = ((u * w) + (v * w))

    proof

      let X,Y,Z be RealNormSpace, w be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)), u,v be Point of ( R_NormSpace_of_BoundedLinearOperators (Y,Z));

      

       A1: ( modetrans (w,X,Y)) = w by LOPBAN_1:def 11;

      

       A2: ( modetrans (u,Y,Z)) = u by LOPBAN_1:def 11;

      for x be Point of X holds (((u - v) * w) . x) = (((u * w) . x) - ((v * w) . x))

      proof

        let x be Point of X;

        

        thus (((u - v) * w) . x) = (( modetrans ((u - v),Y,Z)) . (( modetrans (w,X,Y)) . x)) by FUNCT_2: 15

        .= (( modetrans ((u - v),Y,Z)) . (w . x)) by LOPBAN_1:def 11

        .= ((u - v) . (w . x)) by LOPBAN_1:def 11

        .= ((u . (w . x)) - (v . (w . x))) by LOPBAN_1: 40

        .= ((( modetrans (u,Y,Z)) . (( modetrans (w,X,Y)) . x)) - (( modetrans (v,Y,Z)) . (( modetrans (w,X,Y)) . x))) by A1, A2, LOPBAN_1:def 11

        .= (((( modetrans (u,Y,Z)) * ( modetrans (w,X,Y))) . x) - (( modetrans (v,Y,Z)) . (( modetrans (w,X,Y)) . x))) by FUNCT_2: 15

        .= (((u * w) . x) - ((v * w) . x)) by FUNCT_2: 15;

      end;

      hence ((u - v) * w) = ((u * w) - (v * w)) by LOPBAN_1: 40;

      for x be Point of X holds (((u + v) * w) . x) = (((u * w) . x) + ((v * w) . x))

      proof

        let x be Point of X;

        

        thus (((u + v) * w) . x) = (( modetrans ((u + v),Y,Z)) . (( modetrans (w,X,Y)) . x)) by FUNCT_2: 15

        .= (( modetrans ((u + v),Y,Z)) . (w . x)) by LOPBAN_1:def 11

        .= ((u + v) . (w . x)) by LOPBAN_1:def 11

        .= ((u . (w . x)) + (v . (w . x))) by LOPBAN_1: 35

        .= ((( modetrans (u,Y,Z)) . (( modetrans (w,X,Y)) . x)) + (( modetrans (v,Y,Z)) . (( modetrans (w,X,Y)) . x))) by A1, A2, LOPBAN_1:def 11

        .= (((( modetrans (u,Y,Z)) * ( modetrans (w,X,Y))) . x) + (( modetrans (v,Y,Z)) . (( modetrans (w,X,Y)) . x))) by FUNCT_2: 15

        .= (((u * w) . x) + ((v * w) . x)) by FUNCT_2: 15;

      end;

      hence ((u + v) * w) = ((u * w) + (v * w)) by LOPBAN_1: 35;

    end;

    theorem :: LOPBAN13:21

    

     LM300: for X,Y be RealNormSpace, u,v be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)) holds (u - (u + v)) = ( - v)

    proof

      let X,Y be RealNormSpace, u,v be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y));

      

      thus (u - (u + v)) = ((u - u) - v) by RLVECT_1: 27

      .= (( 0. ( R_NormSpace_of_BoundedLinearOperators (X,Y))) - v) by RLVECT_1: 15

      .= ( - v) by RLVECT_1: 14;

    end;

    theorem :: LOPBAN13:22

    

     LM400: for X,Y be RealNormSpace, u be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)) st u is invertible holds (( Inv u) * u) = ( id X) & (u * ( Inv u)) = ( id Y)

    proof

      let X,Y be RealNormSpace, v be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y));

      assume

       A1: v is invertible;

      v is Lipschitzian LinearOperator of X, Y by LOPBAN_1:def 9;

      then

       A7: ( dom v) = the carrier of X & ( rng v) = the carrier of Y by A1, FUNCT_2:def 1;

      ( Inv v) = (v " ) by A1, Def1;

      then

       A9: ( modetrans (( Inv v),Y,X)) = (v " ) by LOPBAN_1:def 11;

      then

       A11: (( Inv v) * v) = ((v " ) * v) by LOPBAN_1:def 11;

      (v * ( Inv v)) = (v * (v " )) by A9, LOPBAN_1:def 11;

      hence thesis by A1, A7, A11, FUNCT_1: 39;

    end;

    theorem :: LOPBAN13:23

    

     LMTh3: for u be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)) st u is invertible holds for r be Real st 0 < r holds ex s be Real st 0 < s & for v be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)) st ||.(v - u).|| < s holds ||.(( Inv v) - ( Inv u)).|| < r

    proof

      let u be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y));

      assume

       A1: u is invertible;

      let r be Real;

      assume

       A2: 0 < r;

      set r0 = (r / 2);

      

       A3: 0 < r0 & r0 < r by A2, XREAL_1: 215, XREAL_1: 216;

      set s1 = (1 / ||.( Inv u).||);

      set AG = ( R_Normed_Algebra_of_BoundedLinearOperators X);

      

       A5: 0 < ||.( Inv u).|| by A1, LM50;

      then

       A6: 0 < s1 by XREAL_1: 139;

      set s2 = ((1 / 2) / ||.( Inv u).||);

      

       A7: 0 < s2 by A5, XREAL_1: 139;

      

       A8: 0 < ( ||.( Inv u).|| * ||.( Inv u).||) by A5, XREAL_1: 129;

      

       A9: 0 < (r0 / 2) by A3, XREAL_1: 215;

      set s3 = ((r0 / 2) / ( ||.( Inv u).|| * ||.( Inv u).||));

      

       A10: 0 < s3 by A8, A9, XREAL_1: 139;

      set s4 = ( min (s1,s2));

      

       A11: 0 < s4 & s4 <= s1 & s4 <= s2 by A6, A7, XXREAL_0: 15, XXREAL_0: 17;

      set s = ( min (s4,s3));

      

       B11: 0 < s & s <= s4 & s <= s3 by A10, A11, XXREAL_0: 15, XXREAL_0: 17;

      then

       A12: 0 < s & s <= s1 & s <= s2 & s <= s3 by A11, XXREAL_0: 2;

      take s;

      thus 0 < s by A10, A11, XXREAL_0: 15;

      let v be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y));

      assume

       A13: ||.(v - u).|| < s;

      then ||.(v - u).|| < s1 by A12, XXREAL_0: 2;

      then

      consider w be Point of ( R_Normed_Algebra_of_BoundedLinearOperators X), s,I be Point of ( R_NormSpace_of_BoundedLinearOperators (X,X)) such that

       A14: w = (( Inv u) * (v - u)) & s = w & I = ( id X) & ||.s.|| < 1 & (( - w) GeoSeq ) is norm_summable & (I + s) is invertible & ||.( Inv (I + s)).|| <= (1 / (1 - ||.s.||)) & ( Inv (I + s)) = ( Sum (( - w) GeoSeq )) & ( Inv v) = (( Inv (I + s)) * ( Inv u)) by A1, LMTh2;

      reconsider sA = s as Point of AG;

      

       A16: (I * ( Inv u)) = (( id X) * ( modetrans (( Inv u),Y,X))) by A14, LOPBAN_1:def 11

      .= ( modetrans (( Inv u),Y,X)) by FUNCT_2: 17

      .= ( Inv u) by LOPBAN_1:def 11;

      reconsider IIu = (I * ( Inv u)) as Point of ( R_NormSpace_of_BoundedLinearOperators (Y,X));

      (( Inv v) - ( Inv u)) = ((( Inv (I + s)) - I) * ( Inv u)) by A14, A16, LM200;

      then

       A18: ||.(( Inv v) - ( Inv u)).|| <= ( ||.(( Inv (I + s)) - I).|| * ||.( Inv u).||) by NRM;

      

       A19: (( Inv (I + s)) * (I + s)) = I by A14, LM400;

      (( Inv (I + s)) * I) = (( modetrans (( Inv (I + s)),X,X)) * ( id X)) by A14, LOPBAN_1:def 11

      .= ( modetrans (( Inv (I + s)),X,X)) by FUNCT_2: 17

      .= ( Inv (I + s)) by LOPBAN_1:def 11;

      

      then (( Inv (I + s)) - I) = (( Inv (I + s)) * (I - (I + s))) by A19, LM100

      .= (( Inv (I + s)) * ( - s)) by LM300;

      then ||.(( Inv (I + s)) - I).|| <= ( ||.( Inv (I + s)).|| * ||.( - s).||) by NRM;

      then

       A23: ||.(( Inv (I + s)) - I).|| <= ( ||.( Inv (I + s)).|| * ||.s.||) by NORMSP_1: 2;

      

       A24: ||.s.|| <= ( ||.( Inv u).|| * ||.(v - u).||) by A14, NRM;

      ( ||.( Inv (I + s)).|| * ||.s.||) <= ( ||.( Inv (I + s)).|| * ( ||.( Inv u).|| * ||.(v - u).||)) by A14, NRM, XREAL_1: 64;

      then

       A25: ||.(( Inv (I + s)) - I).|| <= (( ||.( Inv (I + s)).|| * ||.( Inv u).||) * ||.(v - u).||) by A23, XXREAL_0: 2;

      ( ||.( Inv (I + s)).|| * ( ||.( Inv u).|| * ||.(v - u).||)) <= ((1 / (1 - ||.s.||)) * ( ||.( Inv u).|| * ||.(v - u).||)) by A14, XREAL_1: 64;

      then ||.(( Inv (I + s)) - I).|| <= (((1 / (1 - ||.s.||)) * ||.( Inv u).||) * ||.(v - u).||) by A25, XXREAL_0: 2;

      then ( ||.(( Inv (I + s)) - I).|| * ||.( Inv u).||) <= ((((1 / (1 - ||.s.||)) * ||.( Inv u).||) * ||.(v - u).||) * ||.( Inv u).||) by XREAL_1: 64;

      then

       A29: ||.(( Inv v) - ( Inv u)).|| <= ((((1 / (1 - ||.s.||)) * ||.( Inv u).||) * ||.(v - u).||) * ||.( Inv u).||) by A18, XXREAL_0: 2;

       ||.(v - u).|| < s2 by A12, A13, XXREAL_0: 2;

      then ( ||.( Inv u).|| * ||.(v - u).||) <= ( ||.( Inv u).|| * ((1 / 2) / ||.( Inv u).||)) by XREAL_1: 64;

      then ( ||.( Inv u).|| * ||.(v - u).||) <= (1 / 2) by A5, XCMPLX_1: 87;

      then ||.s.|| <= (1 / 2) by A24, XXREAL_0: 2;

      then (1 - (1 / 2)) <= (1 - ||.s.||) by XREAL_1: 10;

      then (1 / (1 - ||.s.||)) <= (1 / (1 / 2)) by XREAL_1: 118;

      then

       A32: ((1 / (1 - ||.s.||)) * (( ||.( Inv u).|| * ||.( Inv u).||) * ||.(v - u).||)) <= (2 * (( ||.( Inv u).|| * ||.( Inv u).||) * ||.(v - u).||)) by XREAL_1: 64;

       ||.(v - u).|| < s3 by B11, A13, XXREAL_0: 2;

      then ( ||.(v - u).|| * ( ||.( Inv u).|| * ||.( Inv u).||)) <= (s3 * ( ||.( Inv u).|| * ||.( Inv u).||)) by XREAL_1: 64;

      then ( ||.(v - u).|| * ( ||.( Inv u).|| * ||.( Inv u).||)) <= (r0 / 2) by A8, XCMPLX_1: 87;

      then (2 * ( ||.( Inv u).|| * ( ||.( Inv u).|| * ||.(v - u).||))) <= ((r0 / 2) * 2) by XREAL_1: 64;

      then ((1 / (1 - ||.s.||)) * (( ||.( Inv u).|| * ||.( Inv u).||) * ||.(v - u).||)) <= r0 by A32, XXREAL_0: 2;

      then ||.(( Inv v) - ( Inv u)).|| <= r0 by A29, XXREAL_0: 2;

      hence ||.(( Inv v) - ( Inv u)).|| < r by A3, XXREAL_0: 2;

    end;

    theorem :: LOPBAN13:24

    

     LM80: for I be PartFunc of ( R_NormSpace_of_BoundedLinearOperators (X,Y)), ( R_NormSpace_of_BoundedLinearOperators (Y,X)) st ( dom I) = ( InvertibleOperators (X,Y)) & for u be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)) st u in ( InvertibleOperators (X,Y)) holds (I . u) = ( Inv u) holds I is_continuous_on ( InvertibleOperators (X,Y))

    proof

      let I be PartFunc of ( R_NormSpace_of_BoundedLinearOperators (X,Y)), ( R_NormSpace_of_BoundedLinearOperators (Y,X));

      assume

       A1: ( dom I) = ( InvertibleOperators (X,Y)) & for u be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)) st u in ( InvertibleOperators (X,Y)) holds (I . u) = ( Inv u);

      set S = ( R_NormSpace_of_BoundedLinearOperators (X,Y));

      set T = ( InvertibleOperators (X,Y));

      for x0 be Point of S holds for r be Real st x0 in T & 0 < r holds ex s be Real st 0 < s & for x1 be Point of S st x1 in T & ||.(x1 - x0).|| < s holds ||.((I /. x1) - (I /. x0)).|| < r

      proof

        let x0 be Point of S;

        let r be Real;

        assume

         A2: x0 in T & 0 < r;

        then ex u be Point of S st x0 = u & u is invertible;

        then

        consider s be Real such that

         A4: 0 < s & for v be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)) st ||.(v - x0).|| < s holds ||.(( Inv v) - ( Inv x0)).|| < r by A2, LMTh3;

        take s;

        thus 0 < s by A4;

        let x1 be Point of S;

        assume

         A5: x1 in T & ||.(x1 - x0).|| < s;

        

         A7: (I /. x0) = (I . x0) by A1, A2, PARTFUN1:def 6

        .= ( Inv x0) by A1, A2;

        (I /. x1) = (I . x1) by A1, A5, PARTFUN1:def 6

        .= ( Inv x1) by A1, A5;

        hence thesis by A4, A5, A7;

      end;

      hence I is_continuous_on ( InvertibleOperators (X,Y)) by A1, NFCONT_1: 19;

    end;

    theorem :: LOPBAN13:25

    ex I be PartFunc of ( R_NormSpace_of_BoundedLinearOperators (X,Y)), ( R_NormSpace_of_BoundedLinearOperators (Y,X)) st ( dom I) = ( InvertibleOperators (X,Y)) & ( rng I) = ( InvertibleOperators (Y,X)) & I is one-to-one & I is_continuous_on ( InvertibleOperators (X,Y)) & (ex J be PartFunc of ( R_NormSpace_of_BoundedLinearOperators (Y,X)), ( R_NormSpace_of_BoundedLinearOperators (X,Y)) st J = (I " ) & J is one-to-one & ( dom J) = ( InvertibleOperators (Y,X)) & ( rng J) = ( InvertibleOperators (X,Y)) & J is_continuous_on ( InvertibleOperators (Y,X))) & for u be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)) st u in ( InvertibleOperators (X,Y)) holds (I . u) = ( Inv u)

    proof

      set S = ( R_NormSpace_of_BoundedLinearOperators (X,Y));

      set K = ( R_NormSpace_of_BoundedLinearOperators (Y,X));

      consider J be Function of ( InvertibleOperators (X,Y)), ( InvertibleOperators (Y,X)) such that

       A1: J is one-to-one & J is onto & for u be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)) st u in ( InvertibleOperators (X,Y)) holds (J . u) = ( Inv u) by LM70;

      

       A2: ( InvertibleOperators (X,Y)) <> {} implies ( InvertibleOperators (Y,X)) <> {}

      proof

        assume ( InvertibleOperators (X,Y)) <> {} ;

        then

        consider x be object such that

         A3: x in ( InvertibleOperators (X,Y)) by XBOOLE_0:def 1;

        consider u be Point of S such that

         A4: x = u & u is invertible by A3;

        ( Inv u) is invertible by A4, LM60;

        then ( Inv u) in ( InvertibleOperators (Y,X));

        hence ( InvertibleOperators (Y,X)) <> {} ;

      end;

      then ( dom J) = ( InvertibleOperators (X,Y)) by FUNCT_2:def 1;

      then J in ( PFuncs (the carrier of ( R_NormSpace_of_BoundedLinearOperators (X,Y)),the carrier of ( R_NormSpace_of_BoundedLinearOperators (Y,X)))) by A1, PARTFUN1:def 3;

      then

      reconsider I = J as PartFunc of the carrier of ( R_NormSpace_of_BoundedLinearOperators (X,Y)), the carrier of ( R_NormSpace_of_BoundedLinearOperators (Y,X)) by PARTFUN1: 46;

      take I;

      thus

       A9: ( dom I) = ( InvertibleOperators (X,Y)) by A2, FUNCT_2:def 1;

      thus ( rng I) = ( InvertibleOperators (Y,X)) by A1;

      thus I is one-to-one by A1;

      reconsider L = (J " ) as Function of ( InvertibleOperators (Y,X)), ( InvertibleOperators (X,Y)) by A1, FUNCT_2: 25;

      

       A14: ( dom (J " )) = ( InvertibleOperators (Y,X)) by A1, FUNCT_1: 33;

      

       A16: ( rng (J " )) = ( dom J) by A1, FUNCT_1: 33

      .= ( InvertibleOperators (X,Y)) by A2, FUNCT_2:def 1;

      then L in ( PFuncs (the carrier of ( R_NormSpace_of_BoundedLinearOperators (Y,X)),the carrier of ( R_NormSpace_of_BoundedLinearOperators (X,Y)))) by A14, PARTFUN1:def 3;

      then

      reconsider L as PartFunc of the carrier of ( R_NormSpace_of_BoundedLinearOperators (Y,X)), the carrier of ( R_NormSpace_of_BoundedLinearOperators (X,Y)) by PARTFUN1: 46;

      for v be Point of ( R_NormSpace_of_BoundedLinearOperators (Y,X)) st v in ( InvertibleOperators (Y,X)) holds (L . v) = ( Inv v)

      proof

        let v be Point of ( R_NormSpace_of_BoundedLinearOperators (Y,X));

        assume v in ( InvertibleOperators (Y,X));

        then

        consider u be object such that

         A23: u in ( InvertibleOperators (X,Y)) & (J . u) = v by A1, FUNCT_2: 11;

        reconsider u as Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)) by A23;

        

         A24: ex u0 be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)) st u = u0 & u0 is invertible by A23;

        ( Inv v) = ( Inv ( Inv u)) by A1, A23

        .= u by A24, LM60;

        hence thesis by A1, A2, A23, FUNCT_2: 26;

      end;

      hence thesis by A1, A9, A14, A16, LM80;

    end;

    theorem :: LOPBAN13:26

    

     LOPBAN1623: for X,Y,Z be RealNormSpace, u be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)), w be Point of ( R_NormSpace_of_BoundedLinearOperators (Y,Z)) holds (w * ( - u)) = ( - (w * u)) & (( - w) * u) = ( - (w * u))

    proof

      let X,Y,Z be RealNormSpace, u be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)), w be Point of ( R_NormSpace_of_BoundedLinearOperators (Y,Z));

      for x be Point of X holds ((w * ( - u)) . x) = (( - 1) * ((w * u) . x))

      proof

        let x be Point of X;

        

        thus ((w * ( - u)) . x) = (( modetrans (w,Y,Z)) . (( modetrans (( - u),X,Y)) . x)) by FUNCT_2: 15

        .= (( modetrans (w,Y,Z)) . (( - u) . x)) by LOPBAN_1:def 11

        .= (( modetrans (w,Y,Z)) . ((( - 1) * u) . x)) by RLVECT_1: 16

        .= (( modetrans (w,Y,Z)) . (( - 1) * (u . x))) by LOPBAN_1: 36

        .= (( - 1) * (( modetrans (w,Y,Z)) . (u . x))) by LOPBAN_1:def 5

        .= (( - 1) * (( modetrans (w,Y,Z)) . (( modetrans (u,X,Y)) . x))) by LOPBAN_1:def 11

        .= (( - 1) * ((w * u) . x)) by FUNCT_2: 15;

      end;

      

      hence (w * ( - u)) = (( - 1) * (w * u)) by LOPBAN_1: 36

      .= ( - (w * u)) by RLVECT_1: 16;

      for x be Point of X holds ((( - w) * u) . x) = (( - 1) * ((w * u) . x))

      proof

        let x be Point of X;

        

        thus ((( - w) * u) . x) = (( modetrans (( - w),Y,Z)) . (( modetrans (u,X,Y)) . x)) by FUNCT_2: 15

        .= (( - w) . (( modetrans (u,X,Y)) . x)) by LOPBAN_1:def 11

        .= ((( - 1) * w) . (( modetrans (u,X,Y)) . x)) by RLVECT_1: 16

        .= (( - 1) * (w . (( modetrans (u,X,Y)) . x))) by LOPBAN_1: 36

        .= (( - 1) * (( modetrans (w,Y,Z)) . (( modetrans (u,X,Y)) . x))) by LOPBAN_1:def 11

        .= (( - 1) * ((w * u) . x)) by FUNCT_2: 15;

      end;

      

      hence (( - w) * u) = (( - 1) * (w * u)) by LOPBAN_1: 36

      .= ( - (w * u)) by RLVECT_1: 16;

    end;

    theorem :: LOPBAN13:27

    for X,Y,Z be RealNormSpace, u be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)), w be Point of ( R_NormSpace_of_BoundedLinearOperators (Y,Z)) holds (( - w) * ( - u)) = (w * u)

    proof

      let X,Y,Z be RealNormSpace, u be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)), w be Point of ( R_NormSpace_of_BoundedLinearOperators (Y,Z));

      

      thus (( - w) * ( - u)) = ( - (w * ( - u))) by LOPBAN1623

      .= ( - ( - (w * u))) by LOPBAN1623

      .= (w * u) by RLVECT_1: 17;

    end;

    theorem :: LOPBAN13:28

    

     LOPBAN1624: for X,Y,Z be RealNormSpace, u be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)), w be Point of ( R_NormSpace_of_BoundedLinearOperators (Y,Z)), r be Real holds (w * (r * u)) = ((r * w) * u) & ((r * w) * u) = ((r * w) * u) & ((r * w) * u) = (r * (w * u))

    proof

      let X,Y,Z be RealNormSpace, u be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)), w be Point of ( R_NormSpace_of_BoundedLinearOperators (Y,Z)), r be Real;

      

       A3: for x be Point of X holds ((w * (r * u)) . x) = (r * ((w * u) . x))

      proof

        let x be Point of X;

        

        thus ((w * (r * u)) . x) = (( modetrans (w,Y,Z)) . (( modetrans ((r * u),X,Y)) . x)) by FUNCT_2: 15

        .= (( modetrans (w,Y,Z)) . ((r * u) . x)) by LOPBAN_1:def 11

        .= (( modetrans (w,Y,Z)) . (r * (u . x))) by LOPBAN_1: 36

        .= (r * (( modetrans (w,Y,Z)) . (u . x))) by LOPBAN_1:def 5

        .= (r * (( modetrans (w,Y,Z)) . (( modetrans (u,X,Y)) . x))) by LOPBAN_1:def 11

        .= (r * ((w * u) . x)) by FUNCT_2: 15;

      end;

      for x be Point of X holds (((r * w) * u) . x) = (r * ((w * u) . x))

      proof

        let x be Point of X;

        

        thus (((r * w) * u) . x) = (( modetrans ((r * w),Y,Z)) . (( modetrans (u,X,Y)) . x)) by FUNCT_2: 15

        .= ((r * w) . (( modetrans (u,X,Y)) . x)) by LOPBAN_1:def 11

        .= (r * (w . (( modetrans (u,X,Y)) . x))) by LOPBAN_1: 36

        .= (r * (( modetrans (w,Y,Z)) . (( modetrans (u,X,Y)) . x))) by LOPBAN_1:def 11

        .= (r * ((w * u) . x)) by FUNCT_2: 15;

      end;

      then ((r * w) * u) = (r * (w * u)) by LOPBAN_1: 36;

      hence thesis by A3, LOPBAN_1: 36;

    end;

    theorem :: LOPBAN13:29

    for X,Y,Z be RealNormSpace holds ex I be BilinearOperator of ( R_NormSpace_of_BoundedLinearOperators (X,Y)), ( R_NormSpace_of_BoundedLinearOperators (Y,Z)), ( R_NormSpace_of_BoundedLinearOperators (X,Z)) st I is_continuous_on the carrier of [:( R_NormSpace_of_BoundedLinearOperators (X,Y)), ( R_NormSpace_of_BoundedLinearOperators (Y,Z)):] & for u be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)), v be Point of ( R_NormSpace_of_BoundedLinearOperators (Y,Z)) holds (I . (u,v)) = (v * u)

    proof

      let X,Y,Z be RealNormSpace;

      set E = ( R_NormSpace_of_BoundedLinearOperators (X,Y));

      set F = ( R_NormSpace_of_BoundedLinearOperators (Y,Z));

      set G = ( R_NormSpace_of_BoundedLinearOperators (X,Z));

      defpred P1[ object, object] means ex u be Point of E, v be Point of F st $1 = [u, v] & $2 = (v * u);

      

       A1: for x be object st x in the carrier of [:E, F:] holds ex y be object st y in the carrier of G & P1[x, y]

      proof

        let x be object;

        assume x in the carrier of [:E, F:];

        then

        consider u be Point of E, v be Point of F such that

         A2: x = [u, v] by PRVECT_3: 18;

        take y = (v * u);

        thus y in the carrier of G & P1[x, y] by A2;

      end;

      consider L be Function of the carrier of [:E, F:], the carrier of G such that

       A3: for x be object st x in the carrier of [:E, F:] holds P1[x, (L . x)] from FUNCT_2:sch 1( A1);

      

       A4: for u be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)), v be Point of ( R_NormSpace_of_BoundedLinearOperators (Y,Z)) holds (L . (u,v)) = (v * u)

      proof

        let u be Point of E, v be Point of F;

         [u, v] is set by TARSKI: 1;

        then

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

        consider u1 be Point of E, v1 be Point of F such that

         A5: x = [u1, v1] & (L . x) = (v1 * u1) by A3;

        u = u1 & v = v1 by A5, XTUPLE_0: 1;

        hence thesis by A5;

      end;

      

       A6: 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;

        

        thus (L . ((x1 + x2),y)) = (y * (x1 + x2)) by A4

        .= ((y * x1) + (y * x2)) by LM100

        .= ((L . (x1,y)) + (y * x2)) by A4

        .= ((L . (x1,y)) + (L . (x2,y))) by A4;

      end;

      

       A7: 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;

        

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

        .= ((a * y) * x) by LOPBAN1624

        .= (a * (y * x)) by LOPBAN1624

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

      end;

      

       A8: 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;

        

        thus (L . (x,(y1 + y2))) = ((y1 + y2) * x) by A4

        .= ((y1 * x) + (y2 * x)) by LM200

        .= ((L . (x,y1)) + (y2 * x)) by A4

        .= ((L . (x,y1)) + (L . (x,y2))) by A4;

      end;

      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;

        

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

        .= (a * (y * x)) by LOPBAN1624

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

      end;

      then

      reconsider L as BilinearOperator of E, F, G by A6, A7, A8, LOPBAN_8: 12;

      take L;

      set K = 1;

      for x be Point of E, y be Point of F holds ||.(L . (x,y)).|| <= ((K * ||.x.||) * ||.y.||)

      proof

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

        (L . (x,y)) = (y * x) by A4;

        hence ||.(L . (x,y)).|| <= ((K * ||.x.||) * ||.y.||) by NRM;

      end;

      hence thesis by A4, LOPBAN_8: 13;

    end;

    theorem :: LOPBAN13:30

    

     XXXX: for X,Y be RealNormSpace, v be Lipschitzian LinearOperator of X, Y, w be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)), a be Real st v = w holds (a * w) = (a (#) v)

    proof

      let X,Y be RealNormSpace, v be Lipschitzian LinearOperator of X, Y, w be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)), a be Real;

      set S = ( R_Normed_Algebra_of_BoundedLinearOperators X);

      assume

       A1: v = w;

      (a * w) is Lipschitzian LinearOperator of X, Y by LOPBAN_1:def 9;

      then

       A3: ( dom (a * w)) = the carrier of X by FUNCT_2:def 1;

      

       A4: ( dom (a (#) v)) = ( dom v) by VFUNCT_1:def 4

      .= the carrier of X by FUNCT_2:def 1;

      for s be object st s in ( dom (a (#) v)) holds ((a (#) v) . s) = ((a * w) . s)

      proof

        let s be object;

        assume

         A5: s in ( dom (a (#) v));

        then

        reconsider d = s as Point of X;

        

        thus ((a (#) v) . s) = ((a (#) v) /. d) by A4, PARTFUN1:def 6

        .= (a * (v /. d)) by A5, VFUNCT_1:def 4

        .= ((a * w) . s) by A1, LOPBAN_1: 36;

      end;

      hence (a (#) v) = (a * w) by A3, A4, FUNCT_1: 2;

    end;

    theorem :: LOPBAN13:31

    for X,Y be RealNormSpace, v be Lipschitzian LinearOperator of X, Y, w be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)), a be Real st v = w holds ( - w) = ( - v)

    proof

      let X,Y be RealNormSpace, v be Lipschitzian LinearOperator of X, Y, w be Point of ( R_NormSpace_of_BoundedLinearOperators (X,Y)), a be Real;

      assume

       A1: v = w;

      

      thus ( - w) = (( - 1) * w) by RLVECT_1: 16

      .= (( - 1) (#) v) by A1, XXXX

      .= ( - v) by VFUNCT_1: 23;

    end;