:: MAZURULM semantic presentation

begin

registration
cluster I[01] : ( ( ) ( non empty strict TopSpace-like real-membered ) TopStruct ) -> closed for ( ( ) ( real-membered ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) ;
end;

theorem :: MAZURULM:1
DYADIC : ( ( ) ( complex-membered ext-real-membered real-membered ) Element of K10(REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( ) set ) ) is ( ( dense ) ( complex-membered ext-real-membered real-membered dense ) Subset of ) ;

theorem :: MAZURULM:2
Cl DYADIC : ( ( ) ( complex-membered ext-real-membered real-membered ) Element of K10(REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( complex-membered ext-real-membered real-membered ) Element of K10(REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( ) set ) ) = [.0 : ( ( ) ( empty Function-like functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V66() real ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() bounded_below V93() V120() V121() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() left_end bounded_below ) Element of K10(REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V66() real ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below V120() V121() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() left_end bounded_below ) Element of K10(REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( ) set ) ) ) .] : ( ( ) ( complex-membered ext-real-membered real-membered V93() ) set ) ;

theorem :: MAZURULM:3
for E being ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace)
for a being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) + a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) = 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V66() real ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below V120() V121() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() left_end bounded_below ) Element of K10(REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( ) set ) ) ) * a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ;

theorem :: MAZURULM:4
for E being ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace)
for a, b being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds (a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) + b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) - b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) = a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ;

registration
let A be ( ( real-membered bounded_above ) ( complex-membered ext-real-membered real-membered bounded_above ) set ) ;
let r be ( ( real non negative ) ( V66() real ext-real non negative ) number ) ;
cluster r : ( ( real non negative ) ( V66() real ext-real non negative ) set ) ** A : ( ( real-membered bounded_above ) ( complex-membered ext-real-membered real-membered bounded_above ) set ) : ( ( ) ( complex-membered ext-real-membered real-membered ) set ) -> bounded_above ;
end;

registration
let A be ( ( real-membered bounded_above ) ( complex-membered ext-real-membered real-membered bounded_above ) set ) ;
let r be ( ( real non positive ) ( V66() real ext-real non positive ) number ) ;
cluster r : ( ( real non positive ) ( V66() real ext-real non positive ) set ) ** A : ( ( real-membered bounded_above ) ( complex-membered ext-real-membered real-membered bounded_above ) set ) : ( ( ) ( complex-membered ext-real-membered real-membered ) set ) -> bounded_below ;
end;

registration
let A be ( ( real-membered bounded_below ) ( complex-membered ext-real-membered real-membered bounded_below ) set ) ;
let r be ( ( real non negative ) ( V66() real ext-real non negative ) number ) ;
cluster r : ( ( real non negative ) ( V66() real ext-real non negative ) set ) ** A : ( ( real-membered bounded_below ) ( complex-membered ext-real-membered real-membered bounded_below ) set ) : ( ( ) ( complex-membered ext-real-membered real-membered ) set ) -> bounded_below ;
end;

registration
let A be ( ( non empty real-membered bounded_below ) ( non empty complex-membered ext-real-membered real-membered bounded_below ) set ) ;
let r be ( ( real non positive ) ( V66() real ext-real non positive ) number ) ;
cluster r : ( ( real non positive ) ( V66() real ext-real non positive ) set ) ** A : ( ( non empty real-membered bounded_below ) ( non empty complex-membered ext-real-membered real-membered bounded_below ) set ) : ( ( ) ( non empty complex-membered ext-real-membered real-membered ) set ) -> bounded_above ;
end;

theorem :: MAZURULM:5
for t being ( ( real ) ( V66() real ext-real ) number )
for f being ( ( Function-like quasi_total ) ( non empty V4() V7( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() left_end bounded_below ) Element of K10(REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( ) set ) ) ) V8( REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) Function-like total quasi_total V78() V79() V80() ) Real_Sequence) holds f : ( ( Function-like quasi_total ) ( non empty V4() V7( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() left_end bounded_below ) Element of K10(REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( ) set ) ) ) V8( REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) Function-like total quasi_total V78() V79() V80() ) Real_Sequence) + (NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() left_end bounded_below ) Element of K10(REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( ) set ) ) --> t : ( ( real ) ( V66() real ext-real ) number ) ) : ( ( Function-like quasi_total ) ( non empty V4() V7( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() left_end bounded_below ) Element of K10(REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( ) set ) ) ) V8({b1 : ( ( real ) ( V66() real ext-real ) number ) } : ( ( ) ( non empty complex-membered ext-real-membered real-membered ) set ) ) Function-like constant total quasi_total V78() V79() V80() ) Element of K10(K11(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() left_end bounded_below ) Element of K10(REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( ) set ) ) ,{b1 : ( ( real ) ( V66() real ext-real ) number ) } : ( ( ) ( non empty complex-membered ext-real-membered real-membered ) set ) ) : ( ( ) ( V78() V79() V80() ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( non empty V4() V7( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() left_end bounded_below ) Element of K10(REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( ) set ) ) ) V8( REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) Function-like total quasi_total V78() V79() V80() ) Element of K10(K11(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() left_end bounded_below ) Element of K10(REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( V78() V79() V80() ) set ) ) : ( ( ) ( ) set ) ) = t : ( ( real ) ( V66() real ext-real ) number ) + f : ( ( Function-like quasi_total ) ( non empty V4() V7( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() left_end bounded_below ) Element of K10(REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( ) set ) ) ) V8( REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) Function-like total quasi_total V78() V79() V80() ) Real_Sequence) : ( ( Function-like ) ( non empty V4() V7( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() left_end bounded_below ) Element of K10(REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( ) set ) ) ) V8( REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) Function-like total quasi_total V78() V79() V80() ) Element of K10(K11(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() left_end bounded_below ) Element of K10(REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( V78() V79() V80() ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: MAZURULM:6
for r being ( ( ) ( V66() real ext-real ) Real) holds lim (NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() left_end bounded_below ) Element of K10(REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( ) set ) ) --> r : ( ( ) ( V66() real ext-real ) Real) ) : ( ( Function-like quasi_total ) ( non empty V4() V7( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() left_end bounded_below ) Element of K10(REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( ) set ) ) ) V8( REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) Function-like constant total quasi_total V78() V79() V80() convergent ) Element of K10(K11(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() left_end bounded_below ) Element of K10(REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( V78() V79() V80() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V66() real ext-real ) Element of REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) = r : ( ( ) ( V66() real ext-real ) Real) ;

theorem :: MAZURULM:7
for t being ( ( real ) ( V66() real ext-real ) number )
for f being ( ( Function-like quasi_total convergent ) ( non empty V4() V7( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() left_end bounded_below ) Element of K10(REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( ) set ) ) ) V8( REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) Function-like total quasi_total V78() V79() V80() convergent ) Real_Sequence) holds lim (t : ( ( real ) ( V66() real ext-real ) number ) + f : ( ( Function-like quasi_total convergent ) ( non empty V4() V7( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() left_end bounded_below ) Element of K10(REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( ) set ) ) ) V8( REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) Function-like total quasi_total V78() V79() V80() convergent ) Real_Sequence) ) : ( ( Function-like ) ( non empty V4() V7( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() left_end bounded_below ) Element of K10(REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( ) set ) ) ) V8( REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) Function-like total quasi_total V78() V79() V80() ) Element of K10(K11(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() left_end bounded_below ) Element of K10(REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( V78() V79() V80() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V66() real ext-real ) Element of REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) = t : ( ( real ) ( V66() real ext-real ) number ) + (lim f : ( ( Function-like quasi_total convergent ) ( non empty V4() V7( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() left_end bounded_below ) Element of K10(REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( ) set ) ) ) V8( REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) Function-like total quasi_total V78() V79() V80() convergent ) Real_Sequence) ) : ( ( ) ( V66() real ext-real ) Element of REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( V66() real ext-real ) Element of REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) ;

registration
let f be ( ( Function-like quasi_total convergent ) ( non empty V4() V7( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() left_end bounded_below ) Element of K10(REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( ) set ) ) ) V8( REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) Function-like total quasi_total V78() V79() V80() convergent ) Real_Sequence) ;
let t be ( ( real ) ( V66() real ext-real ) number ) ;
cluster t : ( ( real ) ( V66() real ext-real ) set ) + f : ( ( Function-like quasi_total convergent ) ( non empty V4() V7( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() left_end bounded_below ) Element of K10(REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( ) set ) ) ) V8( REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) Function-like total quasi_total V78() V79() V80() convergent ) Element of K10(K11(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() left_end bounded_below ) Element of K10(REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( V78() V79() V80() ) set ) ) : ( ( ) ( ) set ) ) : ( ( V4() Function-like ) ( V4() V7( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() left_end bounded_below ) Element of K10(REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( ) set ) ) ) Function-like total V78() V79() V80() ) set ) -> Function-like quasi_total convergent for ( ( Function-like quasi_total ) ( non empty V4() V7( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() left_end bounded_below ) Element of K10(REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( ) set ) ) ) V8( REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) Function-like total quasi_total V78() V79() V80() ) Real_Sequence) ;
end;

theorem :: MAZURULM:8
for E being ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace)
for a being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) )
for f being ( ( Function-like quasi_total ) ( non empty V4() V7( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() left_end bounded_below ) Element of K10(REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( ) set ) ) ) V8( REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) Function-like total quasi_total V78() V79() V80() ) Real_Sequence) holds f : ( ( Function-like quasi_total ) ( non empty V4() V7( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() left_end bounded_below ) Element of K10(REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( ) set ) ) ) V8( REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) Function-like total quasi_total V78() V79() V80() ) Real_Sequence) (#) (NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() left_end bounded_below ) Element of K10(REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( ) set ) ) --> a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( non empty V4() V7( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() left_end bounded_below ) Element of K10(REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( ) set ) ) ) V8( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) Function-like constant total quasi_total ) Element of K10(K11(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() left_end bounded_below ) Element of K10(REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( non empty V4() V7( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() left_end bounded_below ) Element of K10(REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( ) set ) ) ) V8( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total ) Element of K10(K11(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() left_end bounded_below ) Element of K10(REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = f : ( ( Function-like quasi_total ) ( non empty V4() V7( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() left_end bounded_below ) Element of K10(REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( ) set ) ) ) V8( REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) Function-like total quasi_total V78() V79() V80() ) Real_Sequence) * a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( non empty V4() V7( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() left_end bounded_below ) Element of K10(REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( ) set ) ) ) V8( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total ) Element of K10(K11(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() left_end bounded_below ) Element of K10(REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: MAZURULM:9
for E being ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace)
for a being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds lim (NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() left_end bounded_below ) Element of K10(REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( ) set ) ) --> a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( non empty V4() V7( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() left_end bounded_below ) Element of K10(REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( ) set ) ) ) V8( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) Function-like constant total quasi_total ) Element of K10(K11(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() left_end bounded_below ) Element of K10(REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) = a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ;

theorem :: MAZURULM:10
for E being ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace)
for a being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) )
for f being ( ( Function-like quasi_total convergent ) ( non empty V4() V7( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() left_end bounded_below ) Element of K10(REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( ) set ) ) ) V8( REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) Function-like total quasi_total V78() V79() V80() convergent ) Real_Sequence) holds lim (f : ( ( Function-like quasi_total convergent ) ( non empty V4() V7( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() left_end bounded_below ) Element of K10(REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( ) set ) ) ) V8( REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) Function-like total quasi_total V78() V79() V80() convergent ) Real_Sequence) * a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( non empty V4() V7( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() left_end bounded_below ) Element of K10(REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( ) set ) ) ) V8( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total ) Element of K10(K11(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() left_end bounded_below ) Element of K10(REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) = (lim f : ( ( Function-like quasi_total convergent ) ( non empty V4() V7( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() left_end bounded_below ) Element of K10(REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( ) set ) ) ) V8( REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) Function-like total quasi_total V78() V79() V80() convergent ) Real_Sequence) ) : ( ( ) ( V66() real ext-real ) Element of REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) * a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ;

registration
let f be ( ( Function-like quasi_total convergent ) ( non empty V4() V7( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() left_end bounded_below ) Element of K10(REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( ) set ) ) ) V8( REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) Function-like total quasi_total V78() V79() V80() convergent ) Real_Sequence) ;
let E be ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) ;
let a be ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ;
cluster f : ( ( Function-like quasi_total convergent ) ( non empty V4() V7( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() left_end bounded_below ) Element of K10(REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( ) set ) ) ) V8( REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) Function-like total quasi_total V78() V79() V80() convergent ) Element of K10(K11(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() left_end bounded_below ) Element of K10(REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( V78() V79() V80() ) set ) ) : ( ( ) ( ) set ) ) * a : ( ( ) ( ) Element of the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( non empty V4() V7( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() left_end bounded_below ) Element of K10(REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( ) set ) ) ) V8( the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total ) Element of K10(K11(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() left_end bounded_below ) Element of K10(REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( ) set ) ) , the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -> Function-like quasi_total convergent ;
end;

definition
let E, F be ( ( non empty ) ( non empty ) NORMSTR ) ;
let f be ( ( Function-like quasi_total ) ( non empty V4() V7( the carrier of E : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( non empty ) set ) ) V8( the carrier of F : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ;
attr f is isometric means :: MAZURULM:def 1
 for a, b being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds ||.((f : ( ( ) ( ) Element of the carrier of F : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) . a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of F : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) - (f : ( ( ) ( ) Element of the carrier of F : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) . b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of F : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of the carrier of F : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) .|| : ( ( ) ( V66() real ext-real ) Element of REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) = ||.(a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) - b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of E : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V66() real ext-real ) Element of REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) ;
end;

definition
let E, F be ( ( non empty ) ( non empty ) RLSStruct ) ;
let f be ( ( Function-like quasi_total ) ( non empty V4() V7( the carrier of E : ( ( non empty ) ( non empty ) RLSStruct ) : ( ( ) ( non empty ) set ) ) V8( the carrier of F : ( ( non empty ) ( non empty ) RLSStruct ) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ;
attr f is Affine means :: MAZURULM:def 2
 for a, b being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) )
for t being ( ( real ) ( V66() real ext-real ) number ) st 0 : ( ( ) ( empty Function-like functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V66() real ext-real non positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() bounded_below V93() V120() V121() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() left_end bounded_below ) Element of K10(REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( ) set ) ) ) <= t : ( ( real ) ( V66() real ext-real ) number ) & t : ( ( real ) ( V66() real ext-real ) number ) <= 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V66() real ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below V120() V121() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() left_end bounded_below ) Element of K10(REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( ) set ) ) ) holds
f : ( ( ) ( ) Element of the carrier of F : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) . (((1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V66() real ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below V120() V121() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() left_end bounded_below ) Element of K10(REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( ) set ) ) ) - t : ( ( real ) ( V66() real ext-real ) number ) ) : ( ( ) ( V66() real ext-real ) Element of REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) * a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of E : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) + (t : ( ( real ) ( V66() real ext-real ) number ) * b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of E : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of E : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of F : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) = ((1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V66() real ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below V120() V121() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() left_end bounded_below ) Element of K10(REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( ) set ) ) ) - t : ( ( real ) ( V66() real ext-real ) number ) ) : ( ( ) ( V66() real ext-real ) Element of REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) * (f : ( ( ) ( ) Element of the carrier of F : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) . a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of F : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of the carrier of F : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) + (t : ( ( real ) ( V66() real ext-real ) number ) * (f : ( ( ) ( ) Element of the carrier of F : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) . b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of F : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of the carrier of F : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of F : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) ;
attr f is midpoints-preserving means :: MAZURULM:def 3
 for a, b being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds f : ( ( ) ( ) Element of the carrier of F : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) . ((1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V66() real ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below V120() V121() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() left_end bounded_below ) Element of K10(REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( ) set ) ) ) / 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V66() real ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below V120() V121() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() left_end bounded_below ) Element of K10(REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V66() real ext-real non negative V121() ) Element of RAT : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered rational-membered V77() ) set ) ) * (a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) + b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of E : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of E : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of F : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) = (1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V66() real ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below V120() V121() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() left_end bounded_below ) Element of K10(REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( ) set ) ) ) / 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V66() real ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below V120() V121() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() left_end bounded_below ) Element of K10(REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V66() real ext-real non negative V121() ) Element of RAT : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered rational-membered V77() ) set ) ) * ((f : ( ( ) ( ) Element of the carrier of F : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) . a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of F : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) + (f : ( ( ) ( ) Element of the carrier of F : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) . b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of F : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of the carrier of F : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of F : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) ;
end;

registration
let E be ( ( non empty ) ( non empty ) NORMSTR ) ;
cluster id E : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( Function-like quasi_total ) ( non empty V4() V7( the carrier of E : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( non empty ) set ) ) V8( the carrier of E : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total ) Element of K10(K11( the carrier of E : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( non empty ) set ) , the carrier of E : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -> Function-like quasi_total isometric ;
end;

registration
let E be ( ( non empty ) ( non empty ) RLSStruct ) ;
cluster id E : ( ( non empty ) ( non empty ) RLSStruct ) : ( ( Function-like quasi_total ) ( non empty V4() V7( the carrier of E : ( ( non empty ) ( non empty ) RLSStruct ) : ( ( ) ( non empty ) set ) ) V8( the carrier of E : ( ( non empty ) ( non empty ) RLSStruct ) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total ) Element of K10(K11( the carrier of E : ( ( non empty ) ( non empty ) RLSStruct ) : ( ( ) ( non empty ) set ) , the carrier of E : ( ( non empty ) ( non empty ) RLSStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -> Function-like quasi_total Affine midpoints-preserving ;
end;

registration
let E be ( ( non empty ) ( non empty ) NORMSTR ) ;
cluster non empty V4() V7( the carrier of E : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( non empty ) set ) ) V8( the carrier of E : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total bijective isometric Affine midpoints-preserving for ( ( ) ( ) Element of K10(K11( the carrier of E : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( non empty ) set ) , the carrier of E : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;
end;

theorem :: MAZURULM:11
for E, F, G being ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace)
for f being ( ( Function-like quasi_total ) ( non empty V4() V7( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) V8( the carrier of b2 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) )
for g being ( ( Function-like quasi_total ) ( non empty V4() V7( the carrier of b2 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) V8( the carrier of b3 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st f : ( ( Function-like quasi_total ) ( non empty V4() V7( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) V8( the carrier of b2 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is isometric & g : ( ( Function-like quasi_total ) ( non empty V4() V7( the carrier of b2 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) V8( the carrier of b3 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is isometric holds
g : ( ( Function-like quasi_total ) ( non empty V4() V7( the carrier of b2 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) V8( the carrier of b3 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) * f : ( ( Function-like quasi_total ) ( non empty V4() V7( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) V8( the carrier of b2 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) : ( ( Function-like ) ( non empty V4() V7( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) V8( the carrier of b3 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total ) Element of K10(K11( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) , the carrier of b3 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) is isometric ;

registration
let E be ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) ;
let f, g be ( ( Function-like quasi_total isometric ) ( non empty V4() V7( the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) V8( the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total isometric ) UnOp of ( ( ) ( non empty ) set ) ) ;
cluster g : ( ( Function-like quasi_total isometric ) ( non empty V4() V7( the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) ) V8( the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total isometric ) Element of K10(K11( the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) , the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) * f : ( ( Function-like quasi_total isometric ) ( non empty V4() V7( the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) ) V8( the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total isometric ) Element of K10(K11( the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) , the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V4() ) ( V4() Function-like ) set ) -> Function-like quasi_total isometric for ( ( Function-like quasi_total ) ( non empty V4() V7( the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) ) V8( the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total ) UnOp of ( ( ) ( non empty ) set ) ) ;
end;

theorem :: MAZURULM:12
for E, F being ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace)
for f being ( ( Function-like quasi_total ) ( non empty V4() V7( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) V8( the carrier of b2 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st f : ( ( Function-like quasi_total ) ( non empty V4() V7( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) V8( the carrier of b2 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is bijective & f : ( ( Function-like quasi_total ) ( non empty V4() V7( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) V8( the carrier of b2 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is isometric holds
f : ( ( Function-like quasi_total ) ( non empty V4() V7( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) V8( the carrier of b2 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) /" : ( ( Function-like quasi_total ) ( non empty V4() V7( the carrier of b2 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) V8( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total ) Element of K10(K11( the carrier of b2 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) is isometric ;

registration
let E be ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) ;
let f be ( ( Function-like quasi_total bijective isometric ) ( non empty V4() V7( the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) V8( the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) Function-like one-to-one total quasi_total onto bijective isometric ) UnOp of ( ( ) ( non empty ) set ) ) ;
cluster f : ( ( Function-like quasi_total bijective isometric ) ( non empty V4() V7( the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) ) V8( the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) ) Function-like one-to-one total quasi_total onto bijective isometric ) Element of K10(K11( the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) , the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) /" : ( ( Function-like quasi_total ) ( non empty V4() V7( the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) ) V8( the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total ) Element of K10(K11( the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) , the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -> Function-like quasi_total isometric ;
end;

theorem :: MAZURULM:13
for E, F, G being ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace)
for f being ( ( Function-like quasi_total ) ( non empty V4() V7( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) V8( the carrier of b2 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) )
for g being ( ( Function-like quasi_total ) ( non empty V4() V7( the carrier of b2 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) V8( the carrier of b3 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st f : ( ( Function-like quasi_total ) ( non empty V4() V7( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) V8( the carrier of b2 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is midpoints-preserving & g : ( ( Function-like quasi_total ) ( non empty V4() V7( the carrier of b2 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) V8( the carrier of b3 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is midpoints-preserving holds
g : ( ( Function-like quasi_total ) ( non empty V4() V7( the carrier of b2 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) V8( the carrier of b3 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) * f : ( ( Function-like quasi_total ) ( non empty V4() V7( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) V8( the carrier of b2 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) : ( ( Function-like ) ( non empty V4() V7( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) V8( the carrier of b3 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total ) Element of K10(K11( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) , the carrier of b3 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) is midpoints-preserving ;

registration
let E be ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) ;
let f, g be ( ( Function-like quasi_total midpoints-preserving ) ( non empty V4() V7( the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) V8( the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total midpoints-preserving ) UnOp of ( ( ) ( non empty ) set ) ) ;
cluster g : ( ( Function-like quasi_total midpoints-preserving ) ( non empty V4() V7( the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) ) V8( the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total midpoints-preserving ) Element of K10(K11( the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) , the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) * f : ( ( Function-like quasi_total midpoints-preserving ) ( non empty V4() V7( the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) ) V8( the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total midpoints-preserving ) Element of K10(K11( the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) , the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V4() ) ( V4() Function-like ) set ) -> Function-like quasi_total midpoints-preserving for ( ( Function-like quasi_total ) ( non empty V4() V7( the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) ) V8( the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total ) UnOp of ( ( ) ( non empty ) set ) ) ;
end;

theorem :: MAZURULM:14
for E, F being ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace)
for f being ( ( Function-like quasi_total ) ( non empty V4() V7( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) V8( the carrier of b2 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st f : ( ( Function-like quasi_total ) ( non empty V4() V7( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) V8( the carrier of b2 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is bijective & f : ( ( Function-like quasi_total ) ( non empty V4() V7( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) V8( the carrier of b2 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is midpoints-preserving holds
f : ( ( Function-like quasi_total ) ( non empty V4() V7( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) V8( the carrier of b2 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) /" : ( ( Function-like quasi_total ) ( non empty V4() V7( the carrier of b2 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) V8( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total ) Element of K10(K11( the carrier of b2 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) is midpoints-preserving ;

registration
let E be ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) ;
let f be ( ( Function-like quasi_total bijective midpoints-preserving ) ( non empty V4() V7( the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) V8( the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) Function-like one-to-one total quasi_total onto bijective midpoints-preserving ) UnOp of ( ( ) ( non empty ) set ) ) ;
cluster f : ( ( Function-like quasi_total bijective midpoints-preserving ) ( non empty V4() V7( the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) ) V8( the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) ) Function-like one-to-one total quasi_total onto bijective midpoints-preserving ) Element of K10(K11( the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) , the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) /" : ( ( Function-like quasi_total ) ( non empty V4() V7( the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) ) V8( the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total ) Element of K10(K11( the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) , the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -> Function-like quasi_total midpoints-preserving ;
end;

theorem :: MAZURULM:15
for E, F, G being ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace)
for f being ( ( Function-like quasi_total ) ( non empty V4() V7( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) V8( the carrier of b2 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) )
for g being ( ( Function-like quasi_total ) ( non empty V4() V7( the carrier of b2 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) V8( the carrier of b3 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st f : ( ( Function-like quasi_total ) ( non empty V4() V7( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) V8( the carrier of b2 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is Affine & g : ( ( Function-like quasi_total ) ( non empty V4() V7( the carrier of b2 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) V8( the carrier of b3 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is Affine holds
g : ( ( Function-like quasi_total ) ( non empty V4() V7( the carrier of b2 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) V8( the carrier of b3 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) * f : ( ( Function-like quasi_total ) ( non empty V4() V7( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) V8( the carrier of b2 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) : ( ( Function-like ) ( non empty V4() V7( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) V8( the carrier of b3 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total ) Element of K10(K11( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) , the carrier of b3 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) is Affine ;

registration
let E be ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) ;
let f, g be ( ( Function-like quasi_total Affine ) ( non empty V4() V7( the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) V8( the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total Affine ) UnOp of ( ( ) ( non empty ) set ) ) ;
cluster g : ( ( Function-like quasi_total Affine ) ( non empty V4() V7( the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) ) V8( the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total Affine ) Element of K10(K11( the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) , the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) * f : ( ( Function-like quasi_total Affine ) ( non empty V4() V7( the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) ) V8( the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total Affine ) Element of K10(K11( the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) , the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( V4() ) ( V4() Function-like ) set ) -> Function-like quasi_total Affine for ( ( Function-like quasi_total ) ( non empty V4() V7( the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) ) V8( the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total ) UnOp of ( ( ) ( non empty ) set ) ) ;
end;

theorem :: MAZURULM:16
for E, F being ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace)
for f being ( ( Function-like quasi_total ) ( non empty V4() V7( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) V8( the carrier of b2 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st f : ( ( Function-like quasi_total ) ( non empty V4() V7( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) V8( the carrier of b2 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is bijective & f : ( ( Function-like quasi_total ) ( non empty V4() V7( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) V8( the carrier of b2 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is Affine holds
f : ( ( Function-like quasi_total ) ( non empty V4() V7( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) V8( the carrier of b2 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) /" : ( ( Function-like quasi_total ) ( non empty V4() V7( the carrier of b2 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) V8( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total ) Element of K10(K11( the carrier of b2 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) is Affine ;

registration
let E be ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) ;
let f be ( ( Function-like quasi_total bijective Affine ) ( non empty V4() V7( the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) V8( the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) Function-like one-to-one total quasi_total onto bijective Affine ) UnOp of ( ( ) ( non empty ) set ) ) ;
cluster f : ( ( Function-like quasi_total bijective Affine ) ( non empty V4() V7( the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) ) V8( the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) ) Function-like one-to-one total quasi_total onto bijective Affine ) Element of K10(K11( the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) , the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) /" : ( ( Function-like quasi_total ) ( non empty V4() V7( the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) ) V8( the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total ) Element of K10(K11( the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) , the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) -> Function-like quasi_total Affine ;
end;

definition
let E be ( ( non empty ) ( non empty ) RLSStruct ) ;
let a be ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ;
func a -reflection -> ( ( Function-like quasi_total ) ( non empty V4() V7( the carrier of E : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( non empty ) set ) ) V8( the carrier of E : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total ) UnOp of ( ( ) ( non empty ) set ) ) means :: MAZURULM:def 4
 for b being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds it : ( ( Function-like quasi_total Affine ) ( non empty V4() V7( the carrier of E : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( non empty ) set ) ) V8( the carrier of E : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total Affine ) Element of K10(K11( the carrier of E : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( non empty ) set ) , the carrier of E : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of E : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( non empty ) set ) ) = (2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V66() real ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below V120() V121() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() left_end bounded_below ) Element of K10(REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( ) set ) ) ) * a : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of E : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( non empty ) set ) ) - b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of E : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( non empty ) set ) ) ;
end;

theorem :: MAZURULM:17
for E being ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace)
for a being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds (a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) -reflection) : ( ( Function-like quasi_total ) ( non empty V4() V7( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) V8( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total ) UnOp of ( ( ) ( non empty ) set ) ) * (a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) -reflection) : ( ( Function-like quasi_total ) ( non empty V4() V7( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) V8( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total ) UnOp of ( ( ) ( non empty ) set ) ) : ( ( Function-like ) ( non empty V4() V7( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) V8( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total ) Element of K10(K11( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = id E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( Function-like quasi_total ) ( non empty V4() V7( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) V8( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total isometric Affine midpoints-preserving ) Element of K10(K11( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

registration
let E be ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) ;
let a be ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ;
cluster a : ( ( ) ( ) Element of the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) ) -reflection : ( ( Function-like quasi_total ) ( non empty V4() V7( the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) ) V8( the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total ) UnOp of ( ( ) ( non empty ) set ) ) -> Function-like quasi_total bijective ;
end;

theorem :: MAZURULM:18
for E being ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace)
for a being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds
( (a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) -reflection) : ( ( Function-like quasi_total ) ( non empty V4() V7( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) V8( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) Function-like one-to-one total quasi_total onto bijective ) UnOp of ( ( ) ( non empty ) set ) ) . a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) = a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) & ( for b being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) st (a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) -reflection) : ( ( Function-like quasi_total ) ( non empty V4() V7( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) V8( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) Function-like one-to-one total quasi_total onto bijective ) UnOp of ( ( ) ( non empty ) set ) ) . b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) = b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds
a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) = b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: MAZURULM:19
for E being ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace)
for a, b being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds ((a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) -reflection) : ( ( Function-like quasi_total ) ( non empty V4() V7( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) V8( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) Function-like one-to-one total quasi_total onto bijective ) UnOp of ( ( ) ( non empty ) set ) ) . b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) - a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) = a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) - b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ;

theorem :: MAZURULM:20
for E being ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace)
for a, b being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds ||.(((a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) -reflection) : ( ( Function-like quasi_total ) ( non empty V4() V7( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) V8( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) Function-like one-to-one total quasi_total onto bijective ) UnOp of ( ( ) ( non empty ) set ) ) . b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) - a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V66() real ext-real non negative ) Element of REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) = ||.(b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) - a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V66() real ext-real non negative ) Element of REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) ;

theorem :: MAZURULM:21
for E being ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace)
for a, b being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds ((a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) -reflection) : ( ( Function-like quasi_total ) ( non empty V4() V7( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) V8( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) Function-like one-to-one total quasi_total onto bijective ) UnOp of ( ( ) ( non empty ) set ) ) . b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) - b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) = 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V66() real ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below V120() V121() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() left_end bounded_below ) Element of K10(REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( ) set ) ) ) * (a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) - b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) ;

theorem :: MAZURULM:22
for E being ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace)
for a, b being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds ||.(((a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) -reflection) : ( ( Function-like quasi_total ) ( non empty V4() V7( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) V8( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) Function-like one-to-one total quasi_total onto bijective ) UnOp of ( ( ) ( non empty ) set ) ) . b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) - b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V66() real ext-real non negative ) Element of REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) = 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V66() real ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below V120() V121() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V77() left_end bounded_below ) Element of K10(REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( ) set ) ) ) * ||.(b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) - a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) .|| : ( ( ) ( V66() real ext-real non negative ) Element of REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) : ( ( ) ( V66() real ext-real non negative ) Element of REAL : ( ( ) ( non empty V28() complex-membered ext-real-membered real-membered V77() non bounded_below non bounded_above V93() ) set ) ) ;

theorem :: MAZURULM:23
for E being ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace)
for a being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds (a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) -reflection) : ( ( Function-like quasi_total ) ( non empty V4() V7( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) V8( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) Function-like one-to-one total quasi_total onto bijective ) UnOp of ( ( ) ( non empty ) set ) ) /" : ( ( Function-like quasi_total ) ( non empty V4() V7( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) V8( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total ) Element of K10(K11( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) -reflection : ( ( Function-like quasi_total ) ( non empty V4() V7( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) V8( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) Function-like one-to-one total quasi_total onto bijective ) UnOp of ( ( ) ( non empty ) set ) ) ;

registration
let E be ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) ;
let a be ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ;
cluster a : ( ( ) ( ) Element of the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) ) -reflection : ( ( Function-like quasi_total ) ( non empty V4() V7( the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) ) V8( the carrier of E : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) NORMSTR ) : ( ( ) ( non empty ) set ) ) Function-like one-to-one total quasi_total onto bijective ) UnOp of ( ( ) ( non empty ) set ) ) -> Function-like quasi_total isometric ;
end;

theorem :: MAZURULM:24
for E, F being ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace)
for f being ( ( Function-like quasi_total ) ( non empty V4() V7( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) V8( the carrier of b2 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st f : ( ( Function-like quasi_total ) ( non empty V4() V7( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) V8( the carrier of b2 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is isometric holds
f : ( ( Function-like quasi_total ) ( non empty V4() V7( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) V8( the carrier of b2 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is_continuous_on dom f : ( ( Function-like quasi_total ) ( non empty V4() V7( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) V8( the carrier of b2 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K10( the carrier of b1 : ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ;

registration
let E, F be ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) ;
cluster Function-like quasi_total bijective isometric -> Function-like quasi_total midpoints-preserving for ( ( ) ( ) Element of K10(K11( the carrier of E : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( non empty ) set ) , the carrier of F : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;
end;

registration
let E, F be ( ( non empty V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning V170() RealNormSpace-like ) ( non empty V133() V134() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V166() discerning V170() RealNormSpace-like ) RealNormSpace) ;
cluster Function-like quasi_total isometric midpoints-preserving -> Function-like quasi_total Affine for ( ( ) ( ) Element of K10(K11( the carrier of E : ( ( non empty ) ( non empty ) NORMSTR ) : ( ( ) ( non empty ) set ) , the carrier of F : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;
end;