:: VECTMETR semantic presentation

begin

definition
let V be ( ( non empty ) ( non empty ) MetrStruct ) ;
attr V is convex means :: VECTMETR:def 1
 for x, y being ( ( ) ( ) Element of ( ( ) ( ) set ) )
for r being ( ( ) ( V11() real ext-real ) Real) st 0 : ( ( ) ( empty ordinal natural V11() real integer Relation-like non-empty empty-yielding NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined RAT : ( ( ) ( non empty V34() V64() V65() V66() V67() V70() ) set ) -valued Function-like one-to-one constant functional V34() FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V53() V54() V55() V56() V63() V64() V65() V66() V67() V68() V69() V70() with_common_domain ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) <= r : ( ( ) ( V11() real ext-real ) Real) & r : ( ( ) ( V11() real ext-real ) Real) <= 1 : ( ( ) ( non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) holds
ex z being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st
( dist (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) = r : ( ( ) ( V11() real ext-real ) Real) * (dist (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) )) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) & dist (z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) = (1 : ( ( ) ( non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) - r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) * (dist (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) )) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) );
end;

definition
let V be ( ( non empty ) ( non empty ) MetrStruct ) ;
attr V is internal means :: VECTMETR:def 2
 for x, y being ( ( ) ( ) Element of ( ( ) ( ) set ) )
for p, q being ( ( ) ( V11() real ext-real ) Real) st p : ( ( ) ( V11() real ext-real ) Real) > 0 : ( ( ) ( empty ordinal natural V11() real integer Relation-like non-empty empty-yielding NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined RAT : ( ( ) ( non empty V34() V64() V65() V66() V67() V70() ) set ) -valued Function-like one-to-one constant functional V34() FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V53() V54() V55() V56() V63() V64() V65() V66() V67() V68() V69() V70() with_common_domain ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) & q : ( ( ) ( V11() real ext-real ) Real) > 0 : ( ( ) ( empty ordinal natural V11() real integer Relation-like non-empty empty-yielding NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined RAT : ( ( ) ( non empty V34() V64() V65() V66() V67() V70() ) set ) -valued Function-like one-to-one constant functional V34() FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V53() V54() V55() V56() V63() V64() V65() V66() V67() V68() V69() V70() with_common_domain ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) holds
ex f being ( ( ) ( Relation-like NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of V : ( ( ) ( ) MetrStruct ) : ( ( ) ( ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of the carrier of V : ( ( ) ( ) MetrStruct ) : ( ( ) ( ) set ) ) st
( f : ( ( ) ( Relation-like NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of V : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of the carrier of V : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) ) /. 1 : ( ( ) ( non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of V : ( ( ) ( ) MetrStruct ) : ( ( ) ( ) set ) ) = x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & f : ( ( ) ( Relation-like NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of V : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of the carrier of V : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) ) /. (len f : ( ( ) ( Relation-like NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of V : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of the carrier of V : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of V : ( ( ) ( ) MetrStruct ) : ( ( ) ( ) set ) ) = y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & ( for i being ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) st 1 : ( ( ) ( non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) <= i : ( ( ) ( Relation-like NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like V53() V54() V55() ) FinSequence of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) & i : ( ( ) ( Relation-like NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like V53() V54() V55() ) FinSequence of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) <= (len f : ( ( ) ( Relation-like NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of V : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of the carrier of V : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) - 1 : ( ( ) ( non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V11() real integer ext-real ) Element of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) holds
dist ((f : ( ( ) ( Relation-like NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of V : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of the carrier of V : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) ) /. i : ( ( ) ( Relation-like NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like V53() V54() V55() ) FinSequence of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) ) : ( ( ) ( ) Element of the carrier of V : ( ( ) ( ) MetrStruct ) : ( ( ) ( ) set ) ) ,(f : ( ( ) ( Relation-like NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of V : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of the carrier of V : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) ) /. (i : ( ( ) ( Relation-like NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like V53() V54() V55() ) FinSequence of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) + 1 : ( ( ) ( non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of the carrier of V : ( ( ) ( ) MetrStruct ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) < p : ( ( ) ( V11() real ext-real ) Real) ) & ( for F being ( ( ) ( Relation-like NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like V53() V54() V55() ) FinSequence of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) st len F : ( ( ) ( Relation-like NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like V53() V54() V55() ) FinSequence of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) : ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) = (len f : ( ( ) ( Relation-like NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of V : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of the carrier of V : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) - 1 : ( ( ) ( non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V11() real integer ext-real ) Element of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) & ( for i being ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) st 1 : ( ( ) ( non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) <= i : ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) & i : ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) <= len F : ( ( ) ( Relation-like NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like V53() V54() V55() ) FinSequence of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) : ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) holds
F : ( ( ) ( Relation-like NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like V53() V54() V55() ) FinSequence of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) /. i : ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) = dist ((f : ( ( ) ( Relation-like NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of V : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of the carrier of V : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) ) /. i : ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of the carrier of V : ( ( ) ( ) MetrStruct ) : ( ( ) ( ) set ) ) ,(f : ( ( ) ( Relation-like NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of V : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of the carrier of V : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) ) /. (i : ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of the carrier of V : ( ( ) ( ) MetrStruct ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) ) holds
abs ((dist (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) )) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) - (Sum F : ( ( ) ( Relation-like NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like V53() V54() V55() ) FinSequence of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) < q : ( ( ) ( V11() real ext-real ) Real) ) );
end;

theorem :: VECTMETR:1
for V being ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) st V : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) is convex holds
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for p being ( ( ) ( V11() real ext-real ) Real) st p : ( ( ) ( V11() real ext-real ) Real) > 0 : ( ( ) ( empty ordinal natural V11() real integer Relation-like non-empty empty-yielding NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined RAT : ( ( ) ( non empty V34() V64() V65() V66() V67() V70() ) set ) -valued Function-like one-to-one constant functional V34() FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V53() V54() V55() V56() V63() V64() V65() V66() V67() V68() V69() V70() with_common_domain ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) holds
ex f being ( ( ) ( Relation-like NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of the carrier of V : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) st
( f : ( ( ) ( Relation-like NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) /. 1 : ( ( ) ( non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) = x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & f : ( ( ) ( Relation-like NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) /. (len f : ( ( ) ( Relation-like NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) = y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & ( for i being ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) st 1 : ( ( ) ( non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) <= i : ( ( ) ( Relation-like NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like V53() V54() V55() ) FinSequence of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) & i : ( ( ) ( Relation-like NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like V53() V54() V55() ) FinSequence of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) <= (len f : ( ( ) ( Relation-like NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) - 1 : ( ( ) ( non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V11() real integer ext-real ) Element of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) holds
dist ((f : ( ( ) ( Relation-like NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) /. i : ( ( ) ( Relation-like NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like V53() V54() V55() ) FinSequence of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ,(f : ( ( ) ( Relation-like NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) /. (i : ( ( ) ( Relation-like NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like V53() V54() V55() ) FinSequence of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) + 1 : ( ( ) ( non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) < p : ( ( ) ( V11() real ext-real ) Real) ) & ( for F being ( ( ) ( Relation-like NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like V53() V54() V55() ) FinSequence of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) st len F : ( ( ) ( Relation-like NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like V53() V54() V55() ) FinSequence of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) : ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) = (len f : ( ( ) ( Relation-like NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) - 1 : ( ( ) ( non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V11() real integer ext-real ) Element of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) & ( for i being ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) st 1 : ( ( ) ( non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) <= i : ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) & i : ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) <= len F : ( ( ) ( Relation-like NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like V53() V54() V55() ) FinSequence of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) : ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) holds
F : ( ( ) ( Relation-like NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like V53() V54() V55() ) FinSequence of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) /. i : ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) = dist ((f : ( ( ) ( Relation-like NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) /. i : ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ,(f : ( ( ) ( Relation-like NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like ) FinSequence of the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) /. (i : ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty ordinal natural V11() real integer ext-real positive non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Reflexive discerning symmetric triangle ) ( non empty Reflexive discerning symmetric triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) ) holds
dist (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) = Sum F : ( ( ) ( Relation-like NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) -valued Function-like V34() FinSequence-like FinSubsequence-like V53() V54() V55() ) FinSequence of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) ) ) ;

registration
cluster non empty Reflexive discerning symmetric triangle convex -> non empty Reflexive discerning symmetric triangle internal for ( ( ) ( ) MetrStruct ) ;
end;

registration
cluster non empty Reflexive discerning symmetric triangle Discerning convex for ( ( ) ( ) MetrStruct ) ;
end;

begin

definition
let V be ( ( non empty ) ( non empty ) MetrStruct ) ;
let f be ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of V : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of V : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ;
attr f is isometric means :: VECTMETR:def 3
 for x, y being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds dist (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) = dist ((f : ( ( ) ( ) set ) . x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of V : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,(f : ( ( ) ( ) set ) . y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of V : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) ;
end;

registration
let V be ( ( non empty ) ( non empty ) MetrStruct ) ;
cluster id V : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of V : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of V : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Element of bool [: the carrier of V : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) , the carrier of V : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) -> Function-like quasi_total onto isometric ;
end;

theorem :: VECTMETR:2
for V being ( ( non empty ) ( non empty ) MetrStruct ) holds
( id V : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total onto isometric ) Element of bool [: the carrier of b1 : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) is onto & id V : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total onto isometric ) Element of bool [: the carrier of b1 : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) is isometric ) ;

registration
let V be ( ( non empty ) ( non empty ) MetrStruct ) ;
cluster non empty Relation-like the carrier of V : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of V : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total onto isometric for ( ( ) ( ) Element of bool [: the carrier of V : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) , the carrier of V : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

definition
let V be ( ( non empty ) ( non empty ) MetrStruct ) ;
func ISOM V -> ( ( ) ( ) set ) means :: VECTMETR:def 4
 for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) in it : ( ( ) ( ) set ) iff x : ( ( ) ( ) set ) is ( ( Function-like quasi_total onto isometric ) ( non empty Relation-like the carrier of V : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of V : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total onto isometric ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) );
end;

definition
let V be ( ( non empty ) ( non empty ) MetrStruct ) ;
:: original: ISOM
redefine func ISOM V -> ( ( ) ( functional ) Subset of ( ( ) ( non empty ) set ) ) ;
end;

registration
let V be ( ( non empty Reflexive discerning ) ( non empty Reflexive discerning ) MetrStruct ) ;
cluster Function-like quasi_total isometric -> Function-like one-to-one quasi_total for ( ( ) ( ) Element of bool [: the carrier of V : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) , the carrier of V : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

theorem :: VECTMETR:3
for V being ( ( non empty Reflexive discerning ) ( non empty Reflexive discerning ) MetrStruct )
for f being ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty Reflexive discerning ) ( non empty Reflexive discerning ) MetrStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty Reflexive discerning ) ( non empty Reflexive discerning ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty Reflexive discerning ) ( non empty Reflexive discerning ) MetrStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty Reflexive discerning ) ( non empty Reflexive discerning ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is isometric holds
f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty Reflexive discerning ) ( non empty Reflexive discerning ) MetrStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty Reflexive discerning ) ( non empty Reflexive discerning ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is one-to-one ;

registration
let V be ( ( non empty Reflexive discerning ) ( non empty Reflexive discerning ) MetrStruct ) ;
let f be ( ( Function-like quasi_total onto isometric ) ( non empty Relation-like the carrier of V : ( ( non empty Reflexive discerning ) ( non empty Reflexive discerning ) MetrStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of V : ( ( non empty Reflexive discerning ) ( non empty Reflexive discerning ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued Function-like one-to-one total quasi_total onto bijective isometric ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ;
cluster f : ( ( Function-like quasi_total onto isometric ) ( non empty Relation-like the carrier of V : ( ( non empty Reflexive discerning ) ( non empty Reflexive discerning ) MetrStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of V : ( ( non empty Reflexive discerning ) ( non empty Reflexive discerning ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued Function-like one-to-one total quasi_total onto bijective isometric ) Element of bool [: the carrier of V : ( ( non empty Reflexive discerning ) ( non empty Reflexive discerning ) MetrStruct ) : ( ( ) ( non empty ) set ) , the carrier of V : ( ( non empty Reflexive discerning ) ( non empty Reflexive discerning ) MetrStruct ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) " : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of V : ( ( non empty Reflexive discerning ) ( non empty Reflexive discerning ) MetrStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of V : ( ( non empty Reflexive discerning ) ( non empty Reflexive discerning ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Element of bool [: the carrier of V : ( ( non empty Reflexive discerning ) ( non empty Reflexive discerning ) MetrStruct ) : ( ( ) ( non empty ) set ) , the carrier of V : ( ( non empty Reflexive discerning ) ( non empty Reflexive discerning ) MetrStruct ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) -> Function-like quasi_total onto isometric ;
end;

theorem :: VECTMETR:4
for V being ( ( non empty Reflexive discerning ) ( non empty Reflexive discerning ) MetrStruct )
for f being ( ( Function-like quasi_total onto isometric ) ( non empty Relation-like the carrier of b1 : ( ( non empty Reflexive discerning ) ( non empty Reflexive discerning ) MetrStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty Reflexive discerning ) ( non empty Reflexive discerning ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued Function-like one-to-one total quasi_total onto bijective isometric ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) holds
( f : ( ( Function-like quasi_total onto isometric ) ( non empty Relation-like the carrier of b1 : ( ( non empty Reflexive discerning ) ( non empty Reflexive discerning ) MetrStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty Reflexive discerning ) ( non empty Reflexive discerning ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued Function-like one-to-one total quasi_total onto bijective isometric ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) " : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty Reflexive discerning ) ( non empty Reflexive discerning ) MetrStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty Reflexive discerning ) ( non empty Reflexive discerning ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued Function-like one-to-one total quasi_total onto bijective isometric ) Element of bool [: the carrier of b1 : ( ( non empty Reflexive discerning ) ( non empty Reflexive discerning ) MetrStruct ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty Reflexive discerning ) ( non empty Reflexive discerning ) MetrStruct ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) is onto & f : ( ( Function-like quasi_total onto isometric ) ( non empty Relation-like the carrier of b1 : ( ( non empty Reflexive discerning ) ( non empty Reflexive discerning ) MetrStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty Reflexive discerning ) ( non empty Reflexive discerning ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued Function-like one-to-one total quasi_total onto bijective isometric ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) " : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty Reflexive discerning ) ( non empty Reflexive discerning ) MetrStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty Reflexive discerning ) ( non empty Reflexive discerning ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued Function-like one-to-one total quasi_total onto bijective isometric ) Element of bool [: the carrier of b1 : ( ( non empty Reflexive discerning ) ( non empty Reflexive discerning ) MetrStruct ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty Reflexive discerning ) ( non empty Reflexive discerning ) MetrStruct ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) is isometric ) ;

registration
let V be ( ( non empty ) ( non empty ) MetrStruct ) ;
let f, g be ( ( Function-like quasi_total onto isometric ) ( non empty Relation-like the carrier of V : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of V : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total onto isometric ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ;
cluster g : ( ( Function-like quasi_total onto isometric ) ( non empty Relation-like the carrier of V : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of V : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total onto isometric ) Element of bool [: the carrier of V : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) , the carrier of V : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) * f : ( ( Function-like quasi_total onto isometric ) ( non empty Relation-like the carrier of V : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of V : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total onto isometric ) Element of bool [: the carrier of V : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) , the carrier of V : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) : ( ( Relation-like ) ( Relation-like the carrier of V : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of V : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued Function-like ) set ) -> Function-like quasi_total onto isometric for ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of V : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of V : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ;
end;

theorem :: VECTMETR:5
for V being ( ( non empty ) ( non empty ) MetrStruct )
for f, g being ( ( Function-like quasi_total onto isometric ) ( non empty Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total onto isometric ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) holds
( f : ( ( Function-like quasi_total onto isometric ) ( non empty Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total onto isometric ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) * g : ( ( Function-like quasi_total onto isometric ) ( non empty Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total onto isometric ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) : ( ( Function-like ) ( non empty Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total onto isometric ) Element of bool [: the carrier of b1 : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) is onto & f : ( ( Function-like quasi_total onto isometric ) ( non empty Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total onto isometric ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) * g : ( ( Function-like quasi_total onto isometric ) ( non empty Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total onto isometric ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) : ( ( Function-like ) ( non empty Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total onto isometric ) Element of bool [: the carrier of b1 : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) is isometric ) ;

registration
let V be ( ( non empty ) ( non empty ) MetrStruct ) ;
cluster ISOM V : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( ) set ) -> non empty ;
end;

begin

definition
attr c1 is strict ;
struct RLSMetrStruct -> ( ( ) ( ) RLSStruct ) , ( ( ) ( ) MetrStruct ) ;
aggr RLSMetrStruct(# carrier, distance, ZeroF, addF, Mult #) -> ( ( strict ) ( strict ) RLSMetrStruct ) ;
end;

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

registration
let X be ( ( non empty ) ( non empty ) set ) ;
let F be ( ( Function-like quasi_total ) ( non empty Relation-like [:X : ( ( non empty ) ( non empty ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) -defined REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) -valued Function-like total quasi_total V53() V54() V55() ) Function of [:X : ( ( non empty ) ( non empty ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) , REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) ;
let O be ( ( ) ( ) Element of X : ( ( non empty ) ( non empty ) set ) ) ;
let B be ( ( Function-like quasi_total ) ( non empty Relation-like [:X : ( ( non empty ) ( non empty ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) -defined X : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) BinOp of X : ( ( non empty ) ( non empty ) set ) ) ;
let G be ( ( Function-like quasi_total ) ( non empty Relation-like [:REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) -defined X : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of [:REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) ,X : ( ( non empty ) ( non empty ) set ) ) ;
cluster RLSMetrStruct(# X : ( ( non empty ) ( non empty ) set ) ,F : ( ( Function-like quasi_total ) ( non empty Relation-like [:X : ( ( non empty ) ( non empty ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) -defined REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) -valued Function-like total quasi_total V53() V54() V55() ) Element of bool [:[:X : ( ( non empty ) ( non empty ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) ,REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) :] : ( ( ) ( non empty Relation-like V53() V54() V55() ) set ) : ( ( ) ( non empty ) set ) ) ,O : ( ( ) ( ) Element of X : ( ( non empty ) ( non empty ) set ) ) ,B : ( ( Function-like quasi_total ) ( non empty Relation-like [:X : ( ( non empty ) ( non empty ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) -defined X : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) Element of bool [:[:X : ( ( non empty ) ( non empty ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ,G : ( ( Function-like quasi_total ) ( non empty Relation-like [:REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) -defined X : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) Element of bool [:[:REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RLSMetrStruct ) -> non empty strict ;
end;

definition
let V be ( ( non empty ) ( non empty ) RLSMetrStruct ) ;
attr V is homogeneous means :: VECTMETR:def 5
 for r being ( ( ) ( V11() real ext-real ) Real)
for v, w being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds dist ((r : ( ( ) ( V11() real ext-real ) Real) * v : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of V : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) ) ,(r : ( ( ) ( V11() real ext-real ) Real) * w : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of V : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) = (abs r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) * (dist (v : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,w : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) )) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) ;
end;

definition
let V be ( ( non empty ) ( non empty ) RLSMetrStruct ) ;
attr V is translatible means :: VECTMETR:def 6
 for u, w, v being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds dist (v : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,w : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) = dist ((v : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) + u : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of V : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) ) ,(w : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) + u : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of V : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) ;
end;

definition
let V be ( ( non empty ) ( non empty ) RLSMetrStruct ) ;
let v be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
func Norm v -> ( ( ) ( V11() real ext-real ) Real) equals :: VECTMETR:def 7
 dist ((0. V : ( ( non empty ) ( non empty ) MetrStruct ) ) : ( ( ) ( ) Element of the carrier of V : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( non empty ) set ) ) ,v : ( ( ) ( ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) ;
end;

registration
cluster non empty right_complementable Reflexive discerning symmetric triangle Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict homogeneous translatible for ( ( ) ( ) RLSMetrStruct ) ;
end;

definition
mode RealLinearMetrSpace is ( ( non empty right_complementable Reflexive discerning symmetric triangle Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital homogeneous translatible ) ( non empty right_complementable Reflexive discerning symmetric triangle Discerning Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital homogeneous translatible ) RLSMetrStruct ) ;
end;

theorem :: VECTMETR:6
for V being ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital homogeneous ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital homogeneous ) RLSMetrStruct )
for r being ( ( ) ( V11() real ext-real ) Real)
for v being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds Norm (r : ( ( ) ( V11() real ext-real ) Real) * v : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital homogeneous ) ( non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital homogeneous ) RLSMetrStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V11() real ext-real ) Real) = (abs r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) * (Norm v : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V11() real ext-real ) Real) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) ;

theorem :: VECTMETR:7
for V being ( ( non empty right_complementable triangle Abelian add-associative right_zeroed translatible ) ( non empty right_complementable triangle Abelian add-associative right_zeroed translatible ) RLSMetrStruct )
for v, w being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds Norm (v : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) + w : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty right_complementable triangle Abelian add-associative right_zeroed translatible ) ( non empty right_complementable triangle Abelian add-associative right_zeroed translatible ) RLSMetrStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V11() real ext-real ) Real) <= (Norm v : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V11() real ext-real ) Real) + (Norm w : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V11() real ext-real ) Real) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) ;

theorem :: VECTMETR:8
for V being ( ( non empty right_complementable add-associative right_zeroed translatible ) ( non empty right_complementable add-associative right_zeroed translatible ) RLSMetrStruct )
for v, w being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds dist (v : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,w : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) = Norm (w : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) - v : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty right_complementable add-associative right_zeroed translatible ) ( non empty right_complementable add-associative right_zeroed translatible ) RLSMetrStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V11() real ext-real ) Real) ;

definition
let n be ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) ;
func RLMSpace n -> ( ( non empty right_complementable Reflexive discerning symmetric triangle Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict homogeneous translatible ) ( non empty right_complementable Reflexive discerning symmetric triangle Discerning Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict homogeneous translatible ) RealLinearMetrSpace) means :: VECTMETR:def 8
( the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) = REAL n : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( functional FinSequence-membered ) FinSequenceSet of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) & the distance of it : ( ( ) ( ) set ) : ( ( Function-like quasi_total ) ( Relation-like [: the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) -defined REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) -valued Function-like total quasi_total V53() V54() V55() ) Element of bool [:[: the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ,REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) :] : ( ( ) ( Relation-like V53() V54() V55() ) set ) : ( ( ) ( non empty ) set ) ) = Pitag_dist n : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( Function-like quasi_total ) ( non empty Relation-like [:(REAL n : ( ( non empty ) ( non empty ) MetrStruct ) ) : ( ( ) ( functional FinSequence-membered ) FinSequenceSet of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) ,(REAL n : ( ( non empty ) ( non empty ) MetrStruct ) ) : ( ( ) ( functional FinSequence-membered ) FinSequenceSet of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) :] : ( ( ) ( Relation-like ) set ) -defined REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) -valued Function-like total quasi_total V53() V54() V55() ) Element of bool [:[:(REAL n : ( ( non empty ) ( non empty ) MetrStruct ) ) : ( ( ) ( functional FinSequence-membered ) FinSequenceSet of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) ,(REAL n : ( ( non empty ) ( non empty ) MetrStruct ) ) : ( ( ) ( functional FinSequence-membered ) FinSequenceSet of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) :] : ( ( ) ( Relation-like ) set ) ,REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) :] : ( ( ) ( Relation-like V53() V54() V55() ) set ) : ( ( ) ( non empty ) set ) ) & 0. it : ( ( ) ( ) set ) : ( ( ) ( ) Element of the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) = 0* n : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( Relation-like NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) -valued Function-like V34() V41(n : ( ( non empty ) ( non empty ) MetrStruct ) ) FinSequence-like FinSubsequence-like V53() V54() V55() ) Element of REAL n : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( functional FinSequence-membered ) FinSequenceSet of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) ) & ( for x, y being ( ( ) ( Relation-like NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) -valued Function-like V34() V41(n : ( ( non empty ) ( non empty ) MetrStruct ) ) FinSequence-like FinSubsequence-like V53() V54() V55() ) Element of REAL n : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( functional FinSequence-membered ) FinSequenceSet of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) ) holds the addF of it : ( ( ) ( ) set ) : ( ( Function-like quasi_total ) ( Relation-like [: the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) -defined the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [:[: the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) . (x : ( ( ) ( Relation-like NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) -valued Function-like V34() V41(n : ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) ) FinSequence-like FinSubsequence-like V53() V54() V55() ) Element of REAL n : ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty functional FinSequence-membered ) FinSequenceSet of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) ) ,y : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) ) : ( ( ) ( ) set ) = x : ( ( ) ( Relation-like NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) -valued Function-like V34() V41(n : ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) ) FinSequence-like FinSubsequence-like V53() V54() V55() ) Element of REAL n : ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty functional FinSequence-membered ) FinSequenceSet of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) ) + y : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) -valued Function-like V34() V41(n : ( ( non empty ) ( non empty ) MetrStruct ) ) FinSequence-like FinSubsequence-like V53() V54() V55() ) Element of REAL n : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( functional FinSequence-membered ) FinSequenceSet of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) ) ) & ( for x being ( ( ) ( Relation-like NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) -valued Function-like V34() V41(n : ( ( non empty ) ( non empty ) MetrStruct ) ) FinSequence-like FinSubsequence-like V53() V54() V55() ) Element of REAL n : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( functional FinSequence-membered ) FinSequenceSet of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) )
for r being ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) holds the Mult of it : ( ( ) ( ) set ) : ( ( Function-like quasi_total ) ( Relation-like [:REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) -defined the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [:[:REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) . (r : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) ,x : ( ( ) ( Relation-like NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) -valued Function-like V34() V41(n : ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) ) FinSequence-like FinSubsequence-like V53() V54() V55() ) Element of REAL n : ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty functional FinSequence-membered ) FinSequenceSet of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) ) ) : ( ( ) ( ) set ) = r : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) * x : ( ( ) ( Relation-like NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) -valued Function-like V34() V41(n : ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) ) FinSequence-like FinSubsequence-like V53() V54() V55() ) Element of REAL n : ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty functional FinSequence-membered ) FinSequenceSet of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) -valued Function-like V34() V41(n : ( ( non empty ) ( non empty ) MetrStruct ) ) FinSequence-like FinSubsequence-like V53() V54() V55() ) Element of REAL n : ( ( non empty ) ( non empty ) MetrStruct ) : ( ( ) ( functional FinSequence-membered ) FinSequenceSet of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) ) ) );
end;

theorem :: VECTMETR:9
for n being ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) )
for f being ( ( Function-like quasi_total onto isometric ) ( non empty Relation-like the carrier of (RLMSpace b1 : ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty right_complementable Reflexive discerning symmetric triangle Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict homogeneous translatible ) ( non empty right_complementable Reflexive discerning symmetric triangle Discerning Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict homogeneous translatible ) RealLinearMetrSpace) : ( ( ) ( non empty ) set ) -defined the carrier of (RLMSpace b1 : ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty right_complementable Reflexive discerning symmetric triangle Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict homogeneous translatible ) ( non empty right_complementable Reflexive discerning symmetric triangle Discerning Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict homogeneous translatible ) RealLinearMetrSpace) : ( ( ) ( non empty ) set ) -valued Function-like one-to-one total quasi_total onto bijective isometric ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) holds rng f : ( ( Function-like quasi_total onto isometric ) ( non empty Relation-like the carrier of (RLMSpace b1 : ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty right_complementable Reflexive discerning symmetric triangle Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict homogeneous translatible ) ( non empty right_complementable Reflexive discerning symmetric triangle Discerning Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict homogeneous translatible ) RealLinearMetrSpace) : ( ( ) ( non empty ) set ) -defined the carrier of (RLMSpace b1 : ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty right_complementable Reflexive discerning symmetric triangle Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict homogeneous translatible ) ( non empty right_complementable Reflexive discerning symmetric triangle Discerning Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict homogeneous translatible ) RealLinearMetrSpace) : ( ( ) ( non empty ) set ) -valued Function-like one-to-one total quasi_total onto bijective isometric ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) = REAL n : ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty functional FinSequence-membered ) FinSequenceSet of REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) ) ;

begin

definition
let n be ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) ;
func IsomGroup n -> ( ( strict ) ( strict ) multMagma ) means :: VECTMETR:def 9
( the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) = ISOM (RLMSpace n : ( ( non empty ) ( non empty ) MetrStruct ) ) : ( ( non empty right_complementable Reflexive discerning symmetric triangle Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict homogeneous translatible ) ( non empty right_complementable Reflexive discerning symmetric triangle Discerning Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict homogeneous translatible ) RealLinearMetrSpace) : ( ( ) ( non empty functional ) Subset of ( ( ) ( non empty ) set ) ) & ( for f, g being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) in ISOM (RLMSpace n : ( ( non empty ) ( non empty ) MetrStruct ) ) : ( ( non empty right_complementable Reflexive discerning symmetric triangle Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict homogeneous translatible ) ( non empty right_complementable Reflexive discerning symmetric triangle Discerning Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict homogeneous translatible ) RealLinearMetrSpace) : ( ( ) ( non empty functional ) Subset of ( ( ) ( non empty ) set ) ) & g : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) in ISOM (RLMSpace n : ( ( non empty ) ( non empty ) MetrStruct ) ) : ( ( non empty right_complementable Reflexive discerning symmetric triangle Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict homogeneous translatible ) ( non empty right_complementable Reflexive discerning symmetric triangle Discerning Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict homogeneous translatible ) RealLinearMetrSpace) : ( ( ) ( non empty functional ) Subset of ( ( ) ( non empty ) set ) ) holds
the multF of it : ( ( ) ( ) set ) : ( ( Function-like quasi_total ) ( Relation-like [: the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) -defined the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [:[: the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) , the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) . (f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ,g : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( ) ( ) set ) = f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) * g : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( Relation-like ) ( Relation-like Function-like ) set ) ) );
end;

registration
let n be ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) ;
cluster IsomGroup n : ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( strict ) multMagma ) -> non empty strict ;
end;

registration
let n be ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) ;
cluster IsomGroup n : ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty strict ) multMagma ) -> strict Group-like associative ;
end;

theorem :: VECTMETR:10
for n being ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) holds 1_ (IsomGroup n : ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty strict Group-like associative ) multMagma ) : ( ( ) ( ) Element of the carrier of (IsomGroup b1 : ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty strict Group-like associative ) multMagma ) : ( ( ) ( non empty ) set ) ) = id (RLMSpace n : ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty right_complementable Reflexive discerning symmetric triangle Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict homogeneous translatible ) ( non empty right_complementable Reflexive discerning symmetric triangle Discerning Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict homogeneous translatible ) RealLinearMetrSpace) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (RLMSpace b1 : ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty right_complementable Reflexive discerning symmetric triangle Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict homogeneous translatible ) ( non empty right_complementable Reflexive discerning symmetric triangle Discerning Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict homogeneous translatible ) RealLinearMetrSpace) : ( ( ) ( non empty ) set ) -defined the carrier of (RLMSpace b1 : ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty right_complementable Reflexive discerning symmetric triangle Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict homogeneous translatible ) ( non empty right_complementable Reflexive discerning symmetric triangle Discerning Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict homogeneous translatible ) RealLinearMetrSpace) : ( ( ) ( non empty ) set ) -valued Function-like one-to-one total quasi_total onto bijective isometric ) Element of bool [: the carrier of (RLMSpace b1 : ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty right_complementable Reflexive discerning symmetric triangle Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict homogeneous translatible ) ( non empty right_complementable Reflexive discerning symmetric triangle Discerning Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict homogeneous translatible ) RealLinearMetrSpace) : ( ( ) ( non empty ) set ) , the carrier of (RLMSpace b1 : ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty right_complementable Reflexive discerning symmetric triangle Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict homogeneous translatible ) ( non empty right_complementable Reflexive discerning symmetric triangle Discerning Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict homogeneous translatible ) RealLinearMetrSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: VECTMETR:11
for n being ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) )
for f being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for g being ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (RLMSpace b1 : ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty right_complementable Reflexive discerning symmetric triangle Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict homogeneous translatible ) ( non empty right_complementable Reflexive discerning symmetric triangle Discerning Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict homogeneous translatible ) RealLinearMetrSpace) : ( ( ) ( non empty ) set ) -defined the carrier of (RLMSpace b1 : ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty right_complementable Reflexive discerning symmetric triangle Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict homogeneous translatible ) ( non empty right_complementable Reflexive discerning symmetric triangle Discerning Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict homogeneous translatible ) RealLinearMetrSpace) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st f : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = g : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (RLMSpace b1 : ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty right_complementable Reflexive discerning symmetric triangle Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict homogeneous translatible ) ( non empty right_complementable Reflexive discerning symmetric triangle Discerning Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict homogeneous translatible ) RealLinearMetrSpace) : ( ( ) ( non empty ) set ) -defined the carrier of (RLMSpace b1 : ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty right_complementable Reflexive discerning symmetric triangle Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict homogeneous translatible ) ( non empty right_complementable Reflexive discerning symmetric triangle Discerning Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict homogeneous translatible ) RealLinearMetrSpace) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) holds
f : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) " : ( ( ) ( ) Element of the carrier of (IsomGroup b1 : ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty strict Group-like associative ) multMagma ) : ( ( ) ( non empty ) set ) ) = g : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (RLMSpace b1 : ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty right_complementable Reflexive discerning symmetric triangle Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict homogeneous translatible ) ( non empty right_complementable Reflexive discerning symmetric triangle Discerning Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict homogeneous translatible ) RealLinearMetrSpace) : ( ( ) ( non empty ) set ) -defined the carrier of (RLMSpace b1 : ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty right_complementable Reflexive discerning symmetric triangle Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict homogeneous translatible ) ( non empty right_complementable Reflexive discerning symmetric triangle Discerning Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict homogeneous translatible ) RealLinearMetrSpace) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) " : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (RLMSpace b1 : ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty right_complementable Reflexive discerning symmetric triangle Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict homogeneous translatible ) ( non empty right_complementable Reflexive discerning symmetric triangle Discerning Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict homogeneous translatible ) RealLinearMetrSpace) : ( ( ) ( non empty ) set ) -defined the carrier of (RLMSpace b1 : ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty right_complementable Reflexive discerning symmetric triangle Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict homogeneous translatible ) ( non empty right_complementable Reflexive discerning symmetric triangle Discerning Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict homogeneous translatible ) RealLinearMetrSpace) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Element of bool [: the carrier of (RLMSpace b1 : ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty right_complementable Reflexive discerning symmetric triangle Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict homogeneous translatible ) ( non empty right_complementable Reflexive discerning symmetric triangle Discerning Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict homogeneous translatible ) RealLinearMetrSpace) : ( ( ) ( non empty ) set ) , the carrier of (RLMSpace b1 : ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty right_complementable Reflexive discerning symmetric triangle Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict homogeneous translatible ) ( non empty right_complementable Reflexive discerning symmetric triangle Discerning Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict homogeneous translatible ) RealLinearMetrSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ;

definition
let n be ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) ;
let G be ( ( ) ( non empty Group-like associative ) Subgroup of IsomGroup n : ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty strict Group-like associative ) multMagma ) ) ;
func SubIsomGroupRel G -> ( ( ) ( Relation-like the carrier of (RLMSpace n : ( ( non empty ) ( non empty ) MetrStruct ) ) : ( ( non empty right_complementable Reflexive discerning symmetric triangle Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict homogeneous translatible ) ( non empty right_complementable Reflexive discerning symmetric triangle Discerning Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict homogeneous translatible ) RealLinearMetrSpace) : ( ( ) ( non empty ) set ) -defined the carrier of (RLMSpace n : ( ( non empty ) ( non empty ) MetrStruct ) ) : ( ( non empty right_complementable Reflexive discerning symmetric triangle Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict homogeneous translatible ) ( non empty right_complementable Reflexive discerning symmetric triangle Discerning Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict homogeneous translatible ) RealLinearMetrSpace) : ( ( ) ( non empty ) set ) -valued ) Relation of ) means :: VECTMETR:def 10
 for A, B being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( [A : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,B : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ] : ( ( ) ( V26() ) Element of [: the carrier of (RLMSpace n : ( ( non empty ) ( non empty ) MetrStruct ) ) : ( ( non empty right_complementable Reflexive discerning symmetric triangle Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict homogeneous translatible ) ( non empty right_complementable Reflexive discerning symmetric triangle Discerning Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict homogeneous translatible ) RealLinearMetrSpace) : ( ( ) ( non empty ) set ) , the carrier of (RLMSpace n : ( ( non empty ) ( non empty ) MetrStruct ) ) : ( ( non empty right_complementable Reflexive discerning symmetric triangle Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict homogeneous translatible ) ( non empty right_complementable Reflexive discerning symmetric triangle Discerning Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict homogeneous translatible ) RealLinearMetrSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) ) in it : ( ( ) ( ) Element of n : ( ( non empty ) ( non empty ) MetrStruct ) ) iff ex f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st
( f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) in the carrier of G : ( ( ) ( ) set ) : ( ( ) ( ) set ) & f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . A : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) = B : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) );
end;

registration
let n be ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) ;
let G be ( ( ) ( non empty Group-like associative ) Subgroup of IsomGroup n : ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty strict Group-like associative ) multMagma ) ) ;
cluster SubIsomGroupRel G : ( ( ) ( non empty Group-like associative ) Subgroup of IsomGroup n : ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty strict Group-like associative ) multMagma ) ) : ( ( ) ( Relation-like the carrier of (RLMSpace n : ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty right_complementable Reflexive discerning symmetric triangle Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict homogeneous translatible ) ( non empty right_complementable Reflexive discerning symmetric triangle Discerning Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict homogeneous translatible ) RealLinearMetrSpace) : ( ( ) ( non empty ) set ) -defined the carrier of (RLMSpace n : ( ( ) ( ordinal natural V11() real integer ext-real non negative V63() V64() V65() V66() V67() V68() V69() ) Element of NAT : ( ( ) ( V64() V65() V66() V67() V68() V69() V70() ) Element of bool REAL : ( ( ) ( non empty V34() V64() V65() V66() V70() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( non empty right_complementable Reflexive discerning symmetric triangle Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict homogeneous translatible ) ( non empty right_complementable Reflexive discerning symmetric triangle Discerning Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict homogeneous translatible ) RealLinearMetrSpace) : ( ( ) ( non empty ) set ) -valued ) Relation of ) -> total symmetric transitive ;
end;