:: by Kazuhisa Nakasho

::

:: Received May 27, 2019

:: Copyright (c) 2019 Association of Mizar Users

definition

let X, Y be RealNormSpace;

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

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

attr u is invertible means :: LOPBAN13:def 1

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

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

:: deftheorem defines invertible LOPBAN13:def 1 :

for X, Y being RealNormSpace

for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds

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

for X, Y being RealNormSpace

for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds

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

definition

let X, Y be RealNormSpace;

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

assume A1: u is invertible ;

coherence

u " is Point of (R_NormSpace_of_BoundedLinearOperators (Y,X));

by A1;

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

assume A1: u is invertible ;

func Inv u -> Point of (R_NormSpace_of_BoundedLinearOperators (Y,X)) equals :Def1: :: LOPBAN13:def 2

u " ;

correctness u " ;

coherence

u " is Point of (R_NormSpace_of_BoundedLinearOperators (Y,X));

by A1;

:: deftheorem Def1 defines Inv LOPBAN13:def 2 :

for X, Y being RealNormSpace

for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st u is invertible holds

Inv u = u " ;

for X, Y being RealNormSpace

for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st u is invertible holds

Inv u = u " ;

theorem LOPBAN410: :: LOPBAN13:1

for X being RealNormSpace

for seq being sequence of X

for k being Nat holds ||.((Partial_Sums seq) . k).|| <= (Partial_Sums ||.seq.||) . k

for seq being sequence of X

for k being Nat holds ||.((Partial_Sums seq) . k).|| <= (Partial_Sums ||.seq.||) . k

proof end;

theorem LM0: :: LOPBAN13:2

for X being RealBanachSpace

for s being sequence of X st s is norm_summable holds

||.(Sum s).|| <= Sum ||.s.||

for s being sequence of X st s is norm_summable holds

||.(Sum s).|| <= Sum ||.s.||

proof end;

theorem LM1: :: LOPBAN13:3

for X being Banach_Algebra

for z being Point of X st ||.z.|| < 1 holds

( z GeoSeq is norm_summable & ||.(Sum (z GeoSeq)).|| <= 1 / (1 - ||.z.||) )

for z being Point of X st ||.z.|| < 1 holds

( z GeoSeq is norm_summable & ||.(Sum (z GeoSeq)).|| <= 1 / (1 - ||.z.||) )

proof end;

theorem LM2: :: LOPBAN13:4

for S being Banach_Algebra

for w being 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.||) )

for w being 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 end;

theorem :: LOPBAN13:5

for X being non trivial RealBanachSpace

for v1, v2 being Lipschitzian LinearOperator of X,X

for w1, w2 being Point of (R_Normed_Algebra_of_BoundedLinearOperators X)

for a being Real st v1 = w1 & v2 = w2 holds

( v1 * v2 = w1 * w2 & v1 + v2 = w1 + w2 & a (#) v1 = a * w1 )

for v1, v2 being Lipschitzian LinearOperator of X,X

for w1, w2 being Point of (R_Normed_Algebra_of_BoundedLinearOperators X)

for a being Real st v1 = w1 & v2 = w2 holds

( v1 * v2 = w1 * w2 & v1 + v2 = w1 + w2 & a (#) v1 = a * w1 )

proof end;

theorem :: LOPBAN13:6

for X being non trivial RealBanachSpace

for v1, v2 being Point of (R_NormSpace_of_BoundedLinearOperators (X,X))

for w1, w2 being Point of (R_Normed_Algebra_of_BoundedLinearOperators X)

for a being Real st v1 = w1 & v2 = w2 holds

( v1 + v2 = w1 + w2 & a * v1 = a * w1 ) ;

for v1, v2 being Point of (R_NormSpace_of_BoundedLinearOperators (X,X))

for w1, w2 being Point of (R_Normed_Algebra_of_BoundedLinearOperators X)

for a being Real st v1 = w1 & v2 = w2 holds

( v1 + v2 = w1 + w2 & a * v1 = a * w1 ) ;

theorem :: LOPBAN13:7

for X being non trivial RealBanachSpace

for v1, v2 being Point of (R_NormSpace_of_BoundedLinearOperators (X,X))

for w1, w2 being Point of (R_Normed_Algebra_of_BoundedLinearOperators X) st v1 = w1 & v2 = w2 holds

v1 * v2 = w1 * w2

for v1, v2 being Point of (R_NormSpace_of_BoundedLinearOperators (X,X))

for w1, w2 being Point of (R_Normed_Algebra_of_BoundedLinearOperators X) st v1 = w1 & v2 = w2 holds

v1 * v2 = w1 * w2

proof end;

theorem LM4: :: LOPBAN13:8

for X being non trivial RealBanachSpace

for v being Point of (R_NormSpace_of_BoundedLinearOperators (X,X))

for w being Point of (R_Normed_Algebra_of_BoundedLinearOperators X) st v = w holds

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

for v being Point of (R_NormSpace_of_BoundedLinearOperators (X,X))

for w being Point of (R_Normed_Algebra_of_BoundedLinearOperators X) st v = w holds

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

proof end;

theorem Th1: :: LOPBAN13:9

for X being non trivial RealBanachSpace

for v, I being 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 being Point of (R_Normed_Algebra_of_BoundedLinearOperators X) st

( w = v & (- w) GeoSeq is norm_summable & Inv (I + v) = Sum ((- w) GeoSeq) ) )

for v, I being 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 being Point of (R_Normed_Algebra_of_BoundedLinearOperators X) st

( w = v & (- w) GeoSeq is norm_summable & Inv (I + v) = Sum ((- w) GeoSeq) ) )

proof end;

theorem RELAT136: :: LOPBAN13:10

for X, Y, Z, W being RealNormSpace

for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))

for g being Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z))

for h being Point of (R_NormSpace_of_BoundedLinearOperators (Z,W)) holds h * (g * f) = (h * g) * f

for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))

for g being Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z))

for h being Point of (R_NormSpace_of_BoundedLinearOperators (Z,W)) holds h * (g * f) = (h * g) * f

proof end;

theorem FUNCT229: :: LOPBAN13:11

for X, Y being RealNormSpace

for f being 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 )

for f being 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 end;

theorem LM50: :: LOPBAN13:12

for X, Y being non trivial RealBanachSpace

for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st u is invertible holds

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

for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st u is invertible holds

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

proof end;

theorem Th2: :: LOPBAN13:13

for X, Y being non trivial RealBanachSpace

for u, v being 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 being Point of (R_Normed_Algebra_of_BoundedLinearOperators X) ex s, I being 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) ) )

for u, v being 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 being Point of (R_Normed_Algebra_of_BoundedLinearOperators X) ex s, I being 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 end;

theorem Th3: :: LOPBAN13:14

for X, Y being non trivial RealBanachSpace

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

S is open

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

S is open

proof end;

definition

let X, Y be non trivial RealBanachSpace;

coherence

{ v where v is Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) : v is invertible } is open Subset of (R_NormSpace_of_BoundedLinearOperators (X,Y));

end;
func InvertibleOperators (X,Y) -> open Subset of (R_NormSpace_of_BoundedLinearOperators (X,Y)) equals :: LOPBAN13:def 3

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

correctness { v where v is Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) : v is invertible } ;

coherence

{ v where v is Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) : v is invertible } is open Subset of (R_NormSpace_of_BoundedLinearOperators (X,Y));

proof end;

:: deftheorem defines InvertibleOperators LOPBAN13:def 3 :

for X, Y being non trivial RealBanachSpace holds InvertibleOperators (X,Y) = { v where v is Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) : v is invertible } ;

for X, Y being non trivial RealBanachSpace holds InvertibleOperators (X,Y) = { v where v is Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) : v is invertible } ;

theorem LM60: :: LOPBAN13:15

for X, Y being non trivial RealBanachSpace

for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st u is invertible holds

( Inv u is invertible & Inv (Inv u) = u )

for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st u is invertible holds

( Inv u is invertible & Inv (Inv u) = u )

proof end;

theorem LM70: :: LOPBAN13:16

for X, Y being non trivial RealBanachSpace ex I being Function of (InvertibleOperators (X,Y)),(InvertibleOperators (Y,X)) st

( I is one-to-one & I is onto & ( for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st u in InvertibleOperators (X,Y) holds

I . u = Inv u ) )

( I is one-to-one & I is onto & ( for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st u in InvertibleOperators (X,Y) holds

I . u = Inv u ) )

proof end;

theorem LMTh2: :: LOPBAN13:17

for X, Y being non trivial RealBanachSpace

for u, v being 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 being Point of (R_Normed_Algebra_of_BoundedLinearOperators X) ex s, I being 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) ) )

for u, v being 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 being Point of (R_Normed_Algebra_of_BoundedLinearOperators X) ex s, I being 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 end;

theorem NRM: :: LOPBAN13:18

for X, Y, Z being RealNormSpace

for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))

for v being Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z))

for w being Point of (R_NormSpace_of_BoundedLinearOperators (X,Z)) st w = v * u holds

||.w.|| <= ||.v.|| * ||.u.||

for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))

for v being Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z))

for w being Point of (R_NormSpace_of_BoundedLinearOperators (X,Z)) st w = v * u holds

||.w.|| <= ||.v.|| * ||.u.||

proof end;

theorem LM100: :: LOPBAN13:19

for X, Y, Z being RealNormSpace

for u, v being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))

for w being Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z)) holds

( w * (u - v) = (w * u) - (w * v) & w * (u + v) = (w * u) + (w * v) )

for u, v being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))

for w being Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z)) holds

( w * (u - v) = (w * u) - (w * v) & w * (u + v) = (w * u) + (w * v) )

proof end;

theorem LM200: :: LOPBAN13:20

for X, Y, Z being RealNormSpace

for w being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))

for u, v being Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z)) holds

( (u - v) * w = (u * w) - (v * w) & (u + v) * w = (u * w) + (v * w) )

for w being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))

for u, v being Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z)) holds

( (u - v) * w = (u * w) - (v * w) & (u + v) * w = (u * w) + (v * w) )

proof end;

theorem LM300: :: LOPBAN13:21

for X, Y being RealNormSpace

for u, v being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds u - (u + v) = - v

for u, v being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds u - (u + v) = - v

proof end;

theorem LM400: :: LOPBAN13:22

for X, Y being RealNormSpace

for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st u is invertible holds

( (Inv u) * u = id X & u * (Inv u) = id Y )

for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st u is invertible holds

( (Inv u) * u = id X & u * (Inv u) = id Y )

proof end;

theorem LMTh3: :: LOPBAN13:23

for X, Y being non trivial RealBanachSpace

for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st u is invertible holds

for r being Real st 0 < r holds

ex s being Real st

( 0 < s & ( for v being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st ||.(v - u).|| < s holds

||.((Inv v) - (Inv u)).|| < r ) )

for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st u is invertible holds

for r being Real st 0 < r holds

ex s being Real st

( 0 < s & ( for v being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st ||.(v - u).|| < s holds

||.((Inv v) - (Inv u)).|| < r ) )

proof end;

theorem LM80: :: LOPBAN13:24

for X, Y being non trivial RealBanachSpace

for I being PartFunc of (R_NormSpace_of_BoundedLinearOperators (X,Y)),(R_NormSpace_of_BoundedLinearOperators (Y,X)) st dom I = InvertibleOperators (X,Y) & ( for u being 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)

for I being PartFunc of (R_NormSpace_of_BoundedLinearOperators (X,Y)),(R_NormSpace_of_BoundedLinearOperators (Y,X)) st dom I = InvertibleOperators (X,Y) & ( for u being 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 end;

theorem :: LOPBAN13:25

for X, Y being non trivial RealBanachSpace ex I being 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 being 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 being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st u in InvertibleOperators (X,Y) holds

I . u = Inv u ) )

( dom I = InvertibleOperators (X,Y) & rng I = InvertibleOperators (Y,X) & I is one-to-one & I is_continuous_on InvertibleOperators (X,Y) & ex J being 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 being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st u in InvertibleOperators (X,Y) holds

I . u = Inv u ) )

proof end;

theorem LOPBAN1623: :: LOPBAN13:26

for X, Y, Z being RealNormSpace

for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))

for w being Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z)) holds

( w * (- u) = - (w * u) & (- w) * u = - (w * u) )

for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))

for w being Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z)) holds

( w * (- u) = - (w * u) & (- w) * u = - (w * u) )

proof end;

theorem :: LOPBAN13:27

for X, Y, Z being RealNormSpace

for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))

for w being Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z)) holds (- w) * (- u) = w * u

for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))

for w being Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z)) holds (- w) * (- u) = w * u

proof end;

theorem LOPBAN1624: :: LOPBAN13:28

for X, Y, Z being RealNormSpace

for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))

for w being Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z))

for r being Real holds

( w * (r * u) = (r * w) * u & (r * w) * u = (r * w) * u & (r * w) * u = r * (w * u) )

for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))

for w being Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z))

for r being Real holds

( w * (r * u) = (r * w) * u & (r * w) * u = (r * w) * u & (r * w) * u = r * (w * u) )

proof end;

theorem :: LOPBAN13:29

for X, Y, Z being RealNormSpace ex I being 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 being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))

for v being Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z)) holds I . (u,v) = v * u ) )

( I is_continuous_on the carrier of [:(R_NormSpace_of_BoundedLinearOperators (X,Y)),(R_NormSpace_of_BoundedLinearOperators (Y,Z)):] & ( for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))

for v being Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z)) holds I . (u,v) = v * u ) )

proof end;

theorem XXXX: :: LOPBAN13:30

for X, Y being RealNormSpace

for v being Lipschitzian LinearOperator of X,Y

for w being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))

for a being Real st v = w holds

a * w = a (#) v

for v being Lipschitzian LinearOperator of X,Y

for w being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))

for a being Real st v = w holds

a * w = a (#) v

proof end;

theorem :: LOPBAN13:31

for X, Y being RealNormSpace

for v being Lipschitzian LinearOperator of X,Y

for w being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))

for a being Real st v = w holds

- w = - v

for v being Lipschitzian LinearOperator of X,Y

for w being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))

for a being Real st v = w holds

- w = - v

proof end;