:: LOPBAN_5 semantic presentation

begin

theorem :: LOPBAN_5:1
for seq being ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V33() V34() V35() ) Real_Sequence)
for r being ( ( ) ( V11() real ext-real ) Real) st seq : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V33() V34() V35() ) Real_Sequence) is bounded & 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V163() V164() V165() V166() V167() V168() V169() V207() V230() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ) <= r : ( ( ) ( V11() real ext-real ) Real) holds
lim_inf (r : ( ( ) ( V11() real ext-real ) Real) (#) seq : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V33() V34() V35() ) Real_Sequence) ) : ( ( Function-like ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V33() V34() V35() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) :] : ( ( ) ( non empty V33() V34() V35() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) ) = r : ( ( ) ( V11() real ext-real ) Real) * (lim_inf seq : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V33() V34() V35() ) Real_Sequence) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) ) ;

theorem :: LOPBAN_5:2
for seq being ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V33() V34() V35() ) Real_Sequence)
for r being ( ( ) ( V11() real ext-real ) Real) st seq : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V33() V34() V35() ) Real_Sequence) is bounded & 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V163() V164() V165() V166() V167() V168() V169() V207() V230() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ) <= r : ( ( ) ( V11() real ext-real ) Real) holds
lim_sup (r : ( ( ) ( V11() real ext-real ) Real) (#) seq : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V33() V34() V35() ) Real_Sequence) ) : ( ( Function-like ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V33() V34() V35() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) :] : ( ( ) ( non empty V33() V34() V35() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) ) = r : ( ( ) ( V11() real ext-real ) Real) * (lim_sup seq : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V33() V34() V35() ) Real_Sequence) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) ) ;

registration
let X be ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) ;
cluster MetricSpaceNorm X : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) NORMSTR ) : ( ( non empty Reflexive discerning V94() triangle ) ( non empty Reflexive discerning V94() triangle ) MetrStruct ) -> non empty Reflexive discerning V94() triangle complete ;
end;

definition
let X be ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) ;
let x0 be ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ;
let r be ( ( real ) ( V11() real ext-real ) number ) ;
func Ball (x0,r) -> ( ( ) ( ) Subset of ) equals :: LOPBAN_5:def 1
 { x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) where x is ( ( ) ( ) Point of ( ( ) ( ) set ) ) : ||.(x0 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) NORMSTR ) - x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of X : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) ) < r : ( ( Function-like quasi_total ) ( Relation-like [:X : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) -defined X : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [:[:X : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) } ;
end;

theorem :: LOPBAN_5:3
for X being ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace)
for Y being ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) -defined K323( the carrier of b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool the carrier of b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) SetSequence of ) st union (rng Y : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) -defined K323( the carrier of b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool the carrier of b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) SetSequence of ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) = the carrier of X : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) : ( ( ) ( non empty ) set ) & ( for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V163() V164() V165() V166() V167() V168() V207() V230() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ) holds Y : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) -defined K323( the carrier of b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool the carrier of b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) SetSequence of ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V163() V164() V165() V166() V167() V168() V207() V230() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of K323( the carrier of b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool the carrier of b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) is closed ) holds
ex n0 being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V163() V164() V165() V166() V167() V168() V207() V230() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ) ex r being ( ( ) ( V11() real ext-real ) Real) ex x0 being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) st
( 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V163() V164() V165() V166() V167() V168() V169() V207() V230() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ) < r : ( ( ) ( V11() real ext-real ) Real) & Ball (x0 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( ) Subset of ) c= Y : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) -defined K323( the carrier of b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool the carrier of b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) SetSequence of ) . n0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V163() V164() V165() V166() V167() V168() V207() V230() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of K323( the carrier of b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool (bool the carrier of b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: LOPBAN_5:4
for X, Y being ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace)
for f being ( ( Function-like quasi_total V226(b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) ,b2 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) ) V227(b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) ,b2 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) ) Lipschitzian ) ( non empty Relation-like the carrier of b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23( the carrier of b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) quasi_total V226(b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) ,b2 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) ) V227(b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) ,b2 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) ) Lipschitzian ) LinearOperator of X : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) ,Y : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) ) holds
( f : ( ( Function-like quasi_total V226(b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) ,b2 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) ) V227(b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) ,b2 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) ) Lipschitzian ) ( non empty Relation-like the carrier of b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23( the carrier of b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) quasi_total V226(b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) ,b2 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) ) V227(b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) ,b2 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) ) Lipschitzian ) LinearOperator of b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) ,b2 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) ) is_Lipschitzian_on the carrier of X : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) & f : ( ( Function-like quasi_total V226(b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) ,b2 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) ) V227(b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) ,b2 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) ) Lipschitzian ) ( non empty Relation-like the carrier of b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23( the carrier of b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) quasi_total V226(b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) ,b2 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) ) V227(b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) ,b2 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) ) Lipschitzian ) LinearOperator of b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) ,b2 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) ) is_continuous_on the carrier of X : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) & ( for x being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds f : ( ( Function-like quasi_total V226(b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) ,b2 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) ) V227(b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) ,b2 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) ) Lipschitzian ) ( non empty Relation-like the carrier of b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23( the carrier of b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) quasi_total V226(b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) ,b2 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) ) V227(b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) ,b2 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) ) Lipschitzian ) LinearOperator of b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) ,b2 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) ) is_continuous_in x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: LOPBAN_5:5
for X being ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace)
for Y being ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace)
for T being ( ( ) ( ) Subset of ) st ( for x being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ex K being ( ( real ) ( V11() real ext-real ) number ) st
( 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V163() V164() V165() V166() V167() V168() V169() V207() V230() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ) <= K : ( ( ) ( Relation-like Function-like ) Point of ( ( ) ( non empty ) set ) ) & ( for f being ( ( ) ( Relation-like Function-like ) Point of ( ( ) ( non empty ) set ) ) st f : ( ( ) ( Relation-like Function-like ) Point of ( ( ) ( non empty ) set ) ) in T : ( ( ) ( ) Subset of ) holds
||.(f : ( ( ) ( Relation-like Function-like ) Point of ( ( ) ( non empty ) set ) ) . x : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real non negative ) Element of REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) ) <= K : ( ( ) ( Relation-like Function-like ) Point of ( ( ) ( non empty ) set ) ) ) ) ) holds
ex L being ( ( real ) ( V11() real ext-real ) number ) st
( 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V163() V164() V165() V166() V167() V168() V169() V207() V230() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ) <= L : ( ( real ) ( V11() real ext-real ) number ) & ( for f being ( ( ) ( Relation-like Function-like ) Point of ( ( ) ( non empty ) set ) ) st f : ( ( ) ( Relation-like Function-like ) Point of ( ( ) ( non empty ) set ) ) in T : ( ( ) ( ) Subset of ) holds
||.f : ( ( ) ( Relation-like Function-like ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real non negative ) Element of REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) ) <= L : ( ( real ) ( V11() real ext-real ) number ) ) ) ;

definition
let X, Y be ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) ;
let H be ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of (R_NormSpace_of_BoundedLinearOperators (X : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) ,Y : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) )) : ( ( non empty ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) , the carrier of (R_NormSpace_of_BoundedLinearOperators (X : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) ,Y : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) )) : ( ( non empty ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) ) ;
let x be ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ;
func H # x -> ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of Y : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) sequence of ( ( ) ( non empty ) set ) ) means :: LOPBAN_5:def 2
 for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V163() V164() V165() V166() V167() V168() V207() V230() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ) holds it : ( ( Function-like quasi_total ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) -valued Function-like V23(X : ( ( ) ( ) set ) ) quasi_total V33() V34() V35() ) Element of bool [:X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) :] : ( ( ) ( V33() V34() V35() ) set ) : ( ( ) ( non empty ) set ) ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V163() V164() V165() V166() V167() V168() V207() V230() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of the carrier of Y : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) ) = (H : ( ( Function-like quasi_total ) ( Relation-like [:X : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) -defined X : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [:[:X : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V163() V164() V165() V166() V167() V168() V207() V230() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (X : ( ( ) ( ) set ) ,Y : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) NORMSTR ) )) : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( non empty ) set ) ) . x : ( ( Function-like quasi_total ) ( Relation-like [:REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) -defined X : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [:[:REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of Y : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) ) ;
end;

theorem :: LOPBAN_5:6
for X being ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace)
for Y being ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace)
for vseq being ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of (R_NormSpace_of_BoundedLinearOperators (b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) ,b2 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) )) : ( ( non empty ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) sequence of ( ( ) ( non empty ) set ) )
for tseq being ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23( the carrier of b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st ( for x being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds
( vseq : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of (R_NormSpace_of_BoundedLinearOperators (b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) ,b2 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) )) : ( ( non empty ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) sequence of ( ( ) ( non empty ) set ) ) # x : ( ( ) ( Relation-like Function-like ) Point of ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of b2 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) sequence of ( ( ) ( non empty ) set ) ) is convergent & tseq : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23( the carrier of b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . x : ( ( ) ( Relation-like Function-like ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) = lim (vseq : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of (R_NormSpace_of_BoundedLinearOperators (b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) ,b2 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) )) : ( ( non empty ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) sequence of ( ( ) ( non empty ) set ) ) # x : ( ( ) ( Relation-like Function-like ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of b2 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) sequence of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ) holds
( tseq : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23( the carrier of b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is ( ( Function-like quasi_total V226(b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) ,b2 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) ) V227(b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) ,b2 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) ) Lipschitzian ) ( non empty Relation-like the carrier of b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23( the carrier of b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) : ( ( ) ( non empty ) set ) ) quasi_total V226(b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) ,b2 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) ) V227(b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) ,b2 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) ) Lipschitzian ) LinearOperator of X : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) ,Y : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) ) & ( for x being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds ||.(tseq : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23( the carrier of b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . x : ( ( ) ( Relation-like Function-like ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real non negative ) Element of REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) ) <= (lim_inf ||.vseq : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of (R_NormSpace_of_BoundedLinearOperators (b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) ,b2 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) )) : ( ( non empty ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) sequence of ( ( ) ( non empty ) set ) ) .|| : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V33() V34() V35() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) :] : ( ( ) ( non empty V33() V34() V35() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) ) * ||.x : ( ( ) ( Relation-like Function-like ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) ) ) & ( for ttseq being ( ( ) ( Relation-like Function-like ) Point of ( ( ) ( non empty ) set ) ) st ttseq : ( ( ) ( Relation-like Function-like ) Point of ( ( ) ( non empty ) set ) ) = tseq : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23( the carrier of b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) holds
||.ttseq : ( ( ) ( Relation-like Function-like ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real non negative ) Element of REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) ) <= lim_inf ||.vseq : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of (R_NormSpace_of_BoundedLinearOperators (b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) ,b2 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) RealNormSpace) )) : ( ( non empty ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) sequence of ( ( ) ( non empty ) set ) ) .|| : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V33() V34() V35() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) :] : ( ( ) ( non empty V33() V34() V35() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) ) ) ) ;

begin

theorem :: LOPBAN_5:7
for X being ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace)
for X0 being ( ( ) ( ) Subset of )
for Y being ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace)
for vseq being ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of (R_NormSpace_of_BoundedLinearOperators (b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) ,b3 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) )) : ( ( non empty ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) NORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) sequence of ( ( ) ( non empty ) set ) ) st X0 : ( ( ) ( ) Subset of ) is dense & ( for x being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) st x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) in X0 : ( ( ) ( ) Subset of ) holds
vseq : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of (R_NormSpace_of_BoundedLinearOperators (b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) ,b3 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) )) : ( ( non empty ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) NORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) sequence of ( ( ) ( non empty ) set ) ) # x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of b3 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) sequence of ( ( ) ( non empty ) set ) ) is convergent ) & ( for x being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ex K being ( ( real ) ( V11() real ext-real ) number ) st
( 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V163() V164() V165() V166() V167() V168() V169() V207() V230() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ) <= K : ( ( real ) ( V11() real ext-real ) number ) & ( for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V163() V164() V165() V166() V167() V168() V207() V230() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ) holds ||.((vseq : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of (R_NormSpace_of_BoundedLinearOperators (b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) ,b3 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) )) : ( ( non empty ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) NORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) sequence of ( ( ) ( non empty ) set ) ) # x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of b3 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) sequence of ( ( ) ( non empty ) set ) ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V163() V164() V165() V166() V167() V168() V207() V230() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of the carrier of b3 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) : ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real non negative ) Element of REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) ) <= K : ( ( real ) ( V11() real ext-real ) number ) ) ) ) holds
for x being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds vseq : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of (R_NormSpace_of_BoundedLinearOperators (b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) ,b3 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) )) : ( ( non empty ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) NORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) sequence of ( ( ) ( non empty ) set ) ) # x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of b3 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) sequence of ( ( ) ( non empty ) set ) ) is convergent ;

theorem :: LOPBAN_5:8
for X, Y being ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace)
for X0 being ( ( ) ( ) Subset of )
for vseq being ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of (R_NormSpace_of_BoundedLinearOperators (b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) ,b2 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) )) : ( ( non empty ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) NORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) sequence of ( ( ) ( non empty ) set ) ) st X0 : ( ( ) ( ) Subset of ) is dense & ( for x being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) st x : ( ( ) ( Relation-like Function-like ) Point of ( ( ) ( non empty ) set ) ) in X0 : ( ( ) ( ) Subset of ) holds
vseq : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of (R_NormSpace_of_BoundedLinearOperators (b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) ,b2 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) )) : ( ( non empty ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) NORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) sequence of ( ( ) ( non empty ) set ) ) # x : ( ( ) ( Relation-like Function-like ) Point of ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of b2 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) sequence of ( ( ) ( non empty ) set ) ) is convergent ) & ( for x being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ex K being ( ( real ) ( V11() real ext-real ) number ) st
( 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V163() V164() V165() V166() V167() V168() V169() V207() V230() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ) <= K : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) & ( for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V163() V164() V165() V166() V167() V168() V207() V230() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ) holds ||.((vseq : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of (R_NormSpace_of_BoundedLinearOperators (b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) ,b2 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) )) : ( ( non empty ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) NORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) sequence of ( ( ) ( non empty ) set ) ) # x : ( ( ) ( Relation-like Function-like ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of b2 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) sequence of ( ( ) ( non empty ) set ) ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V163() V164() V165() V166() V167() V168() V207() V230() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) : ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real non negative ) Element of REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) ) <= K : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) ) ) holds
ex tseq being ( ( ) ( Relation-like Function-like ) Point of ( ( ) ( non empty ) set ) ) st
( ( for x being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds
( vseq : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of (R_NormSpace_of_BoundedLinearOperators (b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) ,b2 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) )) : ( ( non empty ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) NORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) sequence of ( ( ) ( non empty ) set ) ) # x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of b2 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) sequence of ( ( ) ( non empty ) set ) ) is convergent & tseq : ( ( ) ( Relation-like Function-like ) Point of ( ( ) ( non empty ) set ) ) . x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) : ( ( ) ( non empty ) set ) ) = lim (vseq : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of (R_NormSpace_of_BoundedLinearOperators (b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) ,b2 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) )) : ( ( non empty ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) NORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) sequence of ( ( ) ( non empty ) set ) ) # x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of b2 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) : ( ( ) ( non empty ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) sequence of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) : ( ( ) ( non empty ) set ) ) & ||.(tseq : ( ( ) ( Relation-like Function-like ) Point of ( ( ) ( non empty ) set ) ) . x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) : ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real non negative ) Element of REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) ) <= (lim_inf ||.vseq : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of (R_NormSpace_of_BoundedLinearOperators (b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) ,b2 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) )) : ( ( non empty ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) NORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) sequence of ( ( ) ( non empty ) set ) ) .|| : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V33() V34() V35() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) :] : ( ( ) ( non empty V33() V34() V35() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) ) * ||.x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real non negative ) Element of REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) ) ) ) & ||.tseq : ( ( ) ( Relation-like Function-like ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V11() real ext-real non negative ) Element of REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) ) <= lim_inf ||.vseq : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of (R_NormSpace_of_BoundedLinearOperators (b1 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) ,b2 : ( ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) RealBanachSpace) )) : ( ( non empty ) ( non empty V120() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V156() RealNormSpace-like complete ) NORMSTR ) : ( ( ) ( non empty ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total ) sequence of ( ( ) ( non empty ) set ) ) .|| : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) -valued Function-like V23( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ) quasi_total V33() V34() V35() ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V163() V164() V165() V166() V167() V168() V169() ) Element of bool REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) : ( ( ) ( non empty ) set ) ) ,REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) :] : ( ( ) ( non empty V33() V34() V35() ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V43() V163() V164() V165() V169() ) set ) ) ) ;