:: NORMSP_1 semantic presentation

begin

definition
attr c1 is strict ;
struct NORMSTR -> ( ( ) ( ) RLSStruct ) , ( ( ) ( ) N-ZeroStr ) ;
aggr NORMSTR(# carrier, ZeroF, addF, Mult, normF #) -> ( ( strict ) ( strict ) NORMSTR ) ;
end;

registration
cluster non empty strict for ( ( ) ( ) NORMSTR ) ;
end;

definition
let IT be ( ( non empty ) ( non empty ) NORMSTR ) ;
attr IT is RealNormSpace-like means :: NORMSP_1:def 1
 for x, y being ( ( ) ( ) Point of ( ( ) ( ) set ) )
for a being ( ( ) ( ext-real V36() real ) Real) holds
( ||.(a : ( ( ) ( ext-real V36() real ) Real) * x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of IT : ( ( ) ( ) N-ZeroStr ) : ( ( ) ( ) set ) ) .|| : ( ( ) ( ext-real V36() real ) Element of REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ) = (abs a : ( ( ) ( ext-real V36() real ) Real) ) : ( ( ) ( ext-real V36() real ) Element of REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ) * ||.x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( ext-real V36() real ) Element of REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ) : ( ( ) ( ext-real V36() real ) Element of REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ) & ||.(x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) + y : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of IT : ( ( ) ( ) N-ZeroStr ) : ( ( ) ( ) set ) ) .|| : ( ( ) ( ext-real V36() real ) Element of REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ) <= ||.x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( ext-real V36() real ) Element of REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ) + ||.y : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( ext-real V36() real ) Element of REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ) : ( ( ) ( ext-real V36() real ) Element of REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ) );
end;

registration
cluster non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive strict RealNormSpace-like for ( ( ) ( ) NORMSTR ) ;
end;

definition
mode RealNormSpace is ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) NORMSTR ) ;
end;

theorem :: NORMSP_1:1
for RNS being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) holds ||.(0. RNS : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) ) : ( ( ) ( V69(b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) ) left_complementable right_complementable complementable ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V36() real V124() V125() V126() V127() V128() V129() V130() ) Element of REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ) = 0 : ( ( ) ( empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() V130() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) ) ;

theorem :: NORMSP_1:2
for RNS being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace)
for x being ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) ) holds ||.(- x : ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( left_complementable right_complementable complementable ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( ext-real V36() real ) Element of REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ) = ||.x : ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( ext-real V36() real ) Element of REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ) ;

theorem :: NORMSP_1:3
for RNS being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace)
for x, y being ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) ) holds ||.(x : ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) ) - y : ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( left_complementable right_complementable complementable ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( ext-real V36() real ) Element of REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ) <= ||.x : ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( ext-real V36() real ) Element of REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ) + ||.y : ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( ext-real V36() real ) Element of REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ) : ( ( ) ( ext-real V36() real ) Element of REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ) ;

theorem :: NORMSP_1:4
for RNS being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace)
for x being ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) ) holds 0 : ( ( ) ( empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() V130() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) ) <= ||.x : ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( ext-real V36() real ) Element of REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ) ;

registration
let RNS be ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) ;
let x be ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) ) ;
cluster ||.x : ( ( ) ( left_complementable right_complementable complementable ) Element of the carrier of RNS : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( ext-real V36() real ) Element of REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ) -> non negative ;
end;

theorem :: NORMSP_1:5
for a, b being ( ( ) ( ext-real V36() real ) Real)
for RNS being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace)
for x, y being ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) ) holds ||.((a : ( ( ) ( ext-real V36() real ) Real) * x : ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( left_complementable right_complementable complementable ) Element of the carrier of b3 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) + (b : ( ( ) ( ext-real V36() real ) Real) * y : ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( left_complementable right_complementable complementable ) Element of the carrier of b3 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( left_complementable right_complementable complementable ) Element of the carrier of b3 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( ext-real non negative V36() real ) Element of REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ) <= ((abs a : ( ( ) ( ext-real V36() real ) Real) ) : ( ( ) ( ext-real V36() real ) Element of REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ) * ||.x : ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( ext-real non negative V36() real ) Element of REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ) ) : ( ( ) ( ext-real V36() real ) Element of REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ) + ((abs b : ( ( ) ( ext-real V36() real ) Real) ) : ( ( ) ( ext-real V36() real ) Element of REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ) * ||.y : ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( ext-real non negative V36() real ) Element of REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ) ) : ( ( ) ( ext-real V36() real ) Element of REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ) : ( ( ) ( ext-real V36() real ) Element of REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ) ;

theorem :: NORMSP_1:6
for RNS being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace)
for x, y being ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) ) holds
( ||.(x : ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) ) - y : ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( left_complementable right_complementable complementable ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( ext-real non negative V36() real ) Element of REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ) = 0 : ( ( ) ( empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() V130() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) ) iff x : ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) ) = y : ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) ) ) ;

theorem :: NORMSP_1:7
for RNS being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace)
for x, y being ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) ) holds ||.(x : ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) ) - y : ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( left_complementable right_complementable complementable ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( ext-real non negative V36() real ) Element of REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ) = ||.(y : ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) ) - x : ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( left_complementable right_complementable complementable ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( ext-real non negative V36() real ) Element of REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ) ;

theorem :: NORMSP_1:8
for RNS being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace)
for x, y being ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) ) holds ||.x : ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( ext-real non negative V36() real ) Element of REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ) - ||.y : ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( ext-real non negative V36() real ) Element of REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ) : ( ( ) ( ext-real V36() real ) Element of REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ) <= ||.(x : ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) ) - y : ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( left_complementable right_complementable complementable ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( ext-real non negative V36() real ) Element of REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ) ;

theorem :: NORMSP_1:9
for RNS being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace)
for x, y being ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) ) holds abs (||.x : ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( ext-real non negative V36() real ) Element of REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ) - ||.y : ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( ext-real non negative V36() real ) Element of REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ) ) : ( ( ) ( ext-real V36() real ) Element of REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ) : ( ( ) ( ext-real V36() real ) Element of REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ) <= ||.(x : ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) ) - y : ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( left_complementable right_complementable complementable ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( ext-real non negative V36() real ) Element of REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ) ;

theorem :: NORMSP_1:10
for RNS being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace)
for x, z, y being ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) ) holds ||.(x : ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) ) - z : ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( left_complementable right_complementable complementable ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( ext-real non negative V36() real ) Element of REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ) <= ||.(x : ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) ) - y : ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( left_complementable right_complementable complementable ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( ext-real non negative V36() real ) Element of REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ) + ||.(y : ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) ) - z : ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( left_complementable right_complementable complementable ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( ext-real non negative V36() real ) Element of REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ) : ( ( ) ( ext-real non negative V36() real ) Element of REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ) ;

theorem :: NORMSP_1:11
for RNS being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace)
for x, y being ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) ) st x : ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) ) <> y : ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) ) holds
||.(x : ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) ) - y : ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( left_complementable right_complementable complementable ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( ext-real non negative V36() real ) Element of REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ) <> 0 : ( ( ) ( empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() V130() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) ) ;

theorem :: NORMSP_1:12
for f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function)
for RNS being ( ( non empty ) ( non empty ) 1-sorted )
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) is ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) iff ( dom f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) = NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) & ( for d being ( ( ) ( ) set ) st d : ( ( ) ( ) set ) in NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) holds
f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . d : ( ( ) ( ) set ) : ( ( ) ( ) set ) is ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ) ) ;

theorem :: NORMSP_1:13
for RNS being ( ( non empty ) ( non empty ) 1-sorted )
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ex S being ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) st rng S : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) = {x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty ) Element of bool the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ;

theorem :: NORMSP_1:14
for RNS being ( ( non empty ) ( non empty ) 1-sorted )
for S being ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) st ex x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st
for n being ( ( natural ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V36() real ) Nat) holds S : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) . n : ( ( natural ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V36() real ) Nat) : ( ( ) ( ) set ) = x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
ex x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st rng S : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) = {x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty ) Element of bool the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ;

theorem :: NORMSP_1:15
for RNS being ( ( non empty ) ( non empty ) 1-sorted )
for S being ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) st ex x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st rng S : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) = {x : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) ) } : ( ( ) ( non empty V124() V125() V126() V127() V128() V129() ) Element of bool the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) holds
for n being ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) ) holds S : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) . n : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) = S : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) . (n : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ;

theorem :: NORMSP_1:16
for RNS being ( ( non empty ) ( non empty ) 1-sorted )
for S being ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) st ( for n being ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) ) holds S : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) . n : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) = S : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) . (n : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) holds
for n, k being ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) ) holds S : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) . n : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) = S : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) . (n : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) ) + k : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ;

theorem :: NORMSP_1:17
for RNS being ( ( non empty ) ( non empty ) 1-sorted )
for S being ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) st ( for n, k being ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) ) holds S : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) . n : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) = S : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) . (n : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) ) + k : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) holds
for n, m being ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) ) holds S : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) . n : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) = S : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) . m : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ;

theorem :: NORMSP_1:18
for RNS being ( ( non empty ) ( non empty ) 1-sorted )
for S being ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) st ( for n, m being ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) ) holds S : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) . n : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) = S : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) . m : ( ( natural ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V36() real ) Nat) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) holds
ex x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st
for n being ( ( natural ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V36() real ) Nat) holds S : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) . n : ( ( natural ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V36() real ) Nat) : ( ( ) ( ) set ) = x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

definition
let RNS be ( ( non empty ) ( non empty ) 1-sorted ) ;
let S be ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of RNS : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of RNS : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of RNS : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) ;
let n be ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) ) ;
:: original: .
redefine func S . n -> ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;
end;

definition
let RNS be ( ( non empty ) ( non empty ) addLoopStr ) ;
let S1, S2 be ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of RNS : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of RNS : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of RNS : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) ;
func S1 + S2 -> ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of RNS : ( ( V55() ) ( V55() ) set ) : ( ( ) ( ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of RNS : ( ( V55() ) ( V55() ) set ) : ( ( ) ( ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of RNS : ( ( V55() ) ( V55() ) set ) : ( ( ) ( ) set ) ) ) sequence of ( ( ) ( ) set ) ) means :: NORMSP_1:def 2
 for n being ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) ) holds it : ( ( Function-like V18([:REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ,RNS : ( ( V55() ) ( V55() ) set ) :] : ( ( ) ( ) set ) ,RNS : ( ( V55() ) ( V55() ) set ) ) ) ( Relation-like [:REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ,RNS : ( ( V55() ) ( V55() ) set ) :] : ( ( ) ( ) set ) -defined RNS : ( ( V55() ) ( V55() ) set ) -valued Function-like V18([:REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ,RNS : ( ( V55() ) ( V55() ) set ) :] : ( ( ) ( ) set ) ,RNS : ( ( V55() ) ( V55() ) set ) ) ) Element of bool [:[:REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ,RNS : ( ( V55() ) ( V55() ) set ) :] : ( ( ) ( ) set ) ,RNS : ( ( V55() ) ( V55() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) . n : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) = (S1 : ( ( ) ( ) set ) . n : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) + (S2 : ( ( Function-like V18(RNS : ( ( V55() ) ( V55() ) set ) , REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ) ) ( Relation-like RNS : ( ( V55() ) ( V55() ) set ) -defined REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) -valued Function-like V18(RNS : ( ( V55() ) ( V55() ) set ) , REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ) ) Element of bool [:RNS : ( ( V55() ) ( V55() ) set ) ,REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) . n : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of RNS : ( ( V55() ) ( V55() ) set ) : ( ( ) ( ) set ) ) ;
end;

definition
let RNS be ( ( non empty ) ( non empty ) addLoopStr ) ;
let S1, S2 be ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of RNS : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of RNS : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of RNS : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) ;
func S1 - S2 -> ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of RNS : ( ( V55() ) ( V55() ) set ) : ( ( ) ( ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of RNS : ( ( V55() ) ( V55() ) set ) : ( ( ) ( ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of RNS : ( ( V55() ) ( V55() ) set ) : ( ( ) ( ) set ) ) ) sequence of ( ( ) ( ) set ) ) means :: NORMSP_1:def 3
 for n being ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) ) holds it : ( ( Function-like V18([:REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ,RNS : ( ( V55() ) ( V55() ) set ) :] : ( ( ) ( ) set ) ,RNS : ( ( V55() ) ( V55() ) set ) ) ) ( Relation-like [:REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ,RNS : ( ( V55() ) ( V55() ) set ) :] : ( ( ) ( ) set ) -defined RNS : ( ( V55() ) ( V55() ) set ) -valued Function-like V18([:REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ,RNS : ( ( V55() ) ( V55() ) set ) :] : ( ( ) ( ) set ) ,RNS : ( ( V55() ) ( V55() ) set ) ) ) Element of bool [:[:REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ,RNS : ( ( V55() ) ( V55() ) set ) :] : ( ( ) ( ) set ) ,RNS : ( ( V55() ) ( V55() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) . n : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) = (S1 : ( ( ) ( ) set ) . n : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) - (S2 : ( ( Function-like V18(RNS : ( ( V55() ) ( V55() ) set ) , REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ) ) ( Relation-like RNS : ( ( V55() ) ( V55() ) set ) -defined REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) -valued Function-like V18(RNS : ( ( V55() ) ( V55() ) set ) , REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ) ) Element of bool [:RNS : ( ( V55() ) ( V55() ) set ) ,REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) . n : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of RNS : ( ( V55() ) ( V55() ) set ) : ( ( ) ( ) set ) ) ;
end;

definition
let RNS be ( ( non empty ) ( non empty ) addLoopStr ) ;
let S be ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of RNS : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of RNS : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of RNS : ( ( non empty ) ( non empty ) addLoopStr ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) ;
let x be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
func S - x -> ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of RNS : ( ( V55() ) ( V55() ) set ) : ( ( ) ( ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of RNS : ( ( V55() ) ( V55() ) set ) : ( ( ) ( ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of RNS : ( ( V55() ) ( V55() ) set ) : ( ( ) ( ) set ) ) ) sequence of ( ( ) ( ) set ) ) means :: NORMSP_1:def 4
 for n being ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) ) holds it : ( ( Function-like V18([:REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ,RNS : ( ( V55() ) ( V55() ) set ) :] : ( ( ) ( ) set ) ,RNS : ( ( V55() ) ( V55() ) set ) ) ) ( Relation-like [:REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ,RNS : ( ( V55() ) ( V55() ) set ) :] : ( ( ) ( ) set ) -defined RNS : ( ( V55() ) ( V55() ) set ) -valued Function-like V18([:REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ,RNS : ( ( V55() ) ( V55() ) set ) :] : ( ( ) ( ) set ) ,RNS : ( ( V55() ) ( V55() ) set ) ) ) Element of bool [:[:REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ,RNS : ( ( V55() ) ( V55() ) set ) :] : ( ( ) ( ) set ) ,RNS : ( ( V55() ) ( V55() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) . n : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) = (S : ( ( ) ( ) set ) . n : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) - x : ( ( Function-like V18(RNS : ( ( V55() ) ( V55() ) set ) , REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ) ) ( Relation-like RNS : ( ( V55() ) ( V55() ) set ) -defined REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) -valued Function-like V18(RNS : ( ( V55() ) ( V55() ) set ) , REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ) ) Element of bool [:RNS : ( ( V55() ) ( V55() ) set ) ,REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of RNS : ( ( V55() ) ( V55() ) set ) : ( ( ) ( ) set ) ) ;
end;

definition
let RNS be ( ( non empty ) ( non empty ) RLSStruct ) ;
let S be ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of RNS : ( ( non empty ) ( non empty ) RLSStruct ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of RNS : ( ( non empty ) ( non empty ) RLSStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of RNS : ( ( non empty ) ( non empty ) RLSStruct ) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) ;
let a be ( ( ) ( ext-real V36() real ) Real) ;
func a * S -> ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of RNS : ( ( V55() ) ( V55() ) set ) : ( ( ) ( ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of RNS : ( ( V55() ) ( V55() ) set ) : ( ( ) ( ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of RNS : ( ( V55() ) ( V55() ) set ) : ( ( ) ( ) set ) ) ) sequence of ( ( ) ( ) set ) ) means :: NORMSP_1:def 5
 for n being ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) ) holds it : ( ( Function-like V18([:REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ,RNS : ( ( V55() ) ( V55() ) set ) :] : ( ( ) ( ) set ) ,RNS : ( ( V55() ) ( V55() ) set ) ) ) ( Relation-like [:REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ,RNS : ( ( V55() ) ( V55() ) set ) :] : ( ( ) ( ) set ) -defined RNS : ( ( V55() ) ( V55() ) set ) -valued Function-like V18([:REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ,RNS : ( ( V55() ) ( V55() ) set ) :] : ( ( ) ( ) set ) ,RNS : ( ( V55() ) ( V55() ) set ) ) ) Element of bool [:[:REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ,RNS : ( ( V55() ) ( V55() ) set ) :] : ( ( ) ( ) set ) ,RNS : ( ( V55() ) ( V55() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) . n : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) = a : ( ( Function-like V18(RNS : ( ( V55() ) ( V55() ) set ) , REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ) ) ( Relation-like RNS : ( ( V55() ) ( V55() ) set ) -defined REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) -valued Function-like V18(RNS : ( ( V55() ) ( V55() ) set ) , REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ) ) Element of bool [:RNS : ( ( V55() ) ( V55() ) set ) ,REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) * (S : ( ( ) ( ) set ) . n : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of RNS : ( ( V55() ) ( V55() ) set ) : ( ( ) ( ) set ) ) ;
end;

definition
let RNS be ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) ;
let S be ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of RNS : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of RNS : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of RNS : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) ;
attr S is convergent means :: NORMSP_1:def 6
 ex g being ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( ) set ) ) st
for r being ( ( ) ( ext-real V36() real ) Real) st 0 : ( ( ) ( empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() V130() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) ) < r : ( ( ) ( ext-real V36() real ) Real) holds
ex m being ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) ) st
for n being ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) ) st m : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) ) <= n : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) ) holds
||.((S : ( ( ) ( ) set ) . n : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) - g : ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of RNS : ( ( V55() ) ( V55() ) set ) : ( ( ) ( ) set ) ) .|| : ( ( ) ( ext-real V36() real ) Element of REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ) < r : ( ( ) ( ext-real V36() real ) Real) ;
end;

theorem :: NORMSP_1:19
for RNS being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace)
for S1, S2 being ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) st S1 : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) is convergent & S2 : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) is convergent holds
S1 : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) + S2 : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) is convergent ;

theorem :: NORMSP_1:20
for RNS being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace)
for S1, S2 being ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) st S1 : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) is convergent & S2 : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) is convergent holds
S1 : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) - S2 : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) is convergent ;

theorem :: NORMSP_1:21
for RNS being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace)
for x being ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) )
for S being ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) st S : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) is convergent holds
S : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) - x : ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) ) : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) is convergent ;

theorem :: NORMSP_1:22
for a being ( ( ) ( ext-real V36() real ) Real)
for RNS being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace)
for S being ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) st S : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) is convergent holds
a : ( ( ) ( ext-real V36() real ) Real) * S : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) is convergent ;

theorem :: NORMSP_1:23
for RNS being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace)
for S being ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) st S : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) is convergent holds
||.S : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) .|| : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ) ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) is convergent ;

definition
let RNS be ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) ;
let S be ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of RNS : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of RNS : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of RNS : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) ;
assume S : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of RNS : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of RNS : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of RNS : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) is convergent ;
func lim S -> ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( ) set ) ) means :: NORMSP_1:def 7
 for r being ( ( ) ( ext-real V36() real ) Real) st 0 : ( ( ) ( empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() V130() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) ) < r : ( ( ) ( ext-real V36() real ) Real) holds
ex m being ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) ) st
for n being ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) ) st m : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) ) <= n : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) ) holds
||.((S : ( ( ) ( ) set ) . n : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of ( ( ) ( ) set ) ) - it : ( ( Function-like V18(RNS : ( ( V55() ) ( V55() ) set ) , REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ) ) ( Relation-like RNS : ( ( V55() ) ( V55() ) set ) -defined REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) -valued Function-like V18(RNS : ( ( V55() ) ( V55() ) set ) , REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ) ) Element of bool [:RNS : ( ( V55() ) ( V55() ) set ) ,REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of the carrier of RNS : ( ( V55() ) ( V55() ) set ) : ( ( ) ( ) set ) ) .|| : ( ( ) ( ext-real V36() real ) Element of REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ) < r : ( ( ) ( ext-real V36() real ) Real) ;
end;

theorem :: NORMSP_1:24
for RNS being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace)
for g being ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) )
for S being ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) st S : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) is convergent & lim S : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) : ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) ) = g : ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) ) holds
( ||.(S : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) - g : ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) .|| : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ) ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) is convergent & lim ||.(S : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) - g : ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) .|| : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ) ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ext-real V36() real ) Element of REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) ) = 0 : ( ( ) ( empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V36() real V122() V123() V124() V125() V126() V127() V128() V129() V130() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) ) ) ;

theorem :: NORMSP_1:25
for RNS being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace)
for S1, S2 being ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) st S1 : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) is convergent & S2 : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) is convergent holds
lim (S1 : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) + S2 : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) : ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) ) = (lim S1 : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) ) + (lim S2 : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( left_complementable right_complementable complementable ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ;

theorem :: NORMSP_1:26
for RNS being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace)
for S1, S2 being ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) st S1 : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) is convergent & S2 : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) is convergent holds
lim (S1 : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) - S2 : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) : ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) ) = (lim S1 : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) ) - (lim S2 : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( left_complementable right_complementable complementable ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ;

theorem :: NORMSP_1:27
for RNS being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace)
for x being ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) )
for S being ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) st S : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) is convergent holds
lim (S : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) - x : ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) : ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) ) = (lim S : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) ) - x : ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( left_complementable right_complementable complementable ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ;

theorem :: NORMSP_1:28
for a being ( ( ) ( ext-real V36() real ) Real)
for RNS being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace)
for S being ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) st S : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) is convergent holds
lim (a : ( ( ) ( ext-real V36() real ) Real) * S : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) : ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) ) = a : ( ( ) ( ext-real V36() real ) Real) * (lim S : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) -defined the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V124() V125() V126() V127() V128() V129() V130() ) Element of bool REAL : ( ( ) ( non empty V50() V124() V125() V126() V130() ) set ) : ( ( ) ( ) set ) ) , the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ) sequence of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( left_complementable right_complementable complementable ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( left_complementable right_complementable complementable ) Element of the carrier of b2 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ) ( non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V120() discerning reflexive RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ;