for f being ( ( Function-like quasi_total bijective ) ( Relation-like Seg 2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( non empty V40() 2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) -element ) Element of bool NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty non trivial cup-closed diff-closed preBoolean V40() ) set ) ) -defined Seg 2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( non empty V40() 2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) -element ) Element of bool NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty non trivial cup-closed diff-closed preBoolean V40() ) set ) ) -valued Function-like one-to-one non empty total quasi_total onto bijective V40() ) Permutation of Seg 2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( non empty V40() 2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) -element ) Element of bool NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty non trivial cup-closed diff-closed preBoolean V40() ) set ) ) ) holds
( f : ( ( Function-like quasi_total bijective ) ( Relation-like Seg 2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( non empty V40() 2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) -element ) Element of bool NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty non trivial cup-closed diff-closed preBoolean V40() ) set ) ) -defined Seg 2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( non empty V40() 2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) -element ) Element of bool NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty non trivial cup-closed diff-closed preBoolean V40() ) set ) ) -valued Function-like one-to-one non empty total quasi_total onto bijective V40() ) Permutation of Seg 2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( non empty V40() 2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) -element ) Element of bool NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty non trivial cup-closed diff-closed preBoolean V40() ) set ) ) ) = <*1 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ,2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) *> : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -defined Function-like non empty V40() 2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) -element FinSequence-like FinSubsequence-like ) set ) or f : ( ( Function-like quasi_total bijective ) ( Relation-like Seg 2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( non empty V40() 2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) -element ) Element of bool NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty non trivial cup-closed diff-closed preBoolean V40() ) set ) ) -defined Seg 2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( non empty V40() 2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) -element ) Element of bool NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty non trivial cup-closed diff-closed preBoolean V40() ) set ) ) -valued Function-like one-to-one non empty total quasi_total onto bijective V40() ) Permutation of Seg 2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( non empty V40() 2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) -element ) Element of bool NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty non trivial cup-closed diff-closed preBoolean V40() ) set ) ) ) = <*2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ,1 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) *> : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -defined Function-like non empty V40() 2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) -element FinSequence-like FinSubsequence-like ) set ) ) ;

for f being ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -defined Function-like V40() FinSequence-like FinSubsequence-like ) FinSequence) st ( f : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -defined Function-like V40() FinSequence-like FinSubsequence-like ) FinSequence) = <*1 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ,2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) *> : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -defined Function-like non empty V40() 2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) -element FinSequence-like FinSubsequence-like ) set ) or f : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -defined Function-like V40() FinSequence-like FinSubsequence-like ) FinSequence) = <*2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ,1 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) *> : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -defined Function-like non empty V40() 2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) -element FinSequence-like FinSubsequence-like ) set ) ) holds
f : ( ( Relation-like Function-like FinSequence-like ) ( Relation-like NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -defined Function-like V40() FinSequence-like FinSubsequence-like ) FinSequence) is ( ( Function-like quasi_total bijective ) ( Relation-like Seg 2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( non empty V40() 2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) -element ) Element of bool NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty non trivial cup-closed diff-closed preBoolean V40() ) set ) ) -defined Seg 2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( non empty V40() 2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) -element ) Element of bool NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty non trivial cup-closed diff-closed preBoolean V40() ) set ) ) -valued Function-like one-to-one non empty total quasi_total onto bijective V40() ) Permutation of Seg 2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( non empty V40() 2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) -element ) Element of bool NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty non trivial cup-closed diff-closed preBoolean V40() ) set ) ) ) ;

Permutations 2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( non empty permutational ) set ) = {<*1 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ,2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) *> : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -defined Function-like non empty V40() 2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) -element FinSequence-like FinSubsequence-like ) set ) ,<*2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ,1 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) *> : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -defined Function-like non empty V40() 2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) -element FinSequence-like FinSubsequence-like ) set ) } : ( ( ) ( functional V40() V44() ) set ) ;

for p being ( ( Function-like quasi_total bijective ) ( Relation-like Seg 2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( non empty V40() 2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) -element ) Element of bool NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty non trivial cup-closed diff-closed preBoolean V40() ) set ) ) -defined Seg 2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( non empty V40() 2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) -element ) Element of bool NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty non trivial cup-closed diff-closed preBoolean V40() ) set ) ) -valued Function-like one-to-one non empty total quasi_total onto bijective V40() ) Permutation of Seg 2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( non empty V40() 2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) -element ) Element of bool NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty non trivial cup-closed diff-closed preBoolean V40() ) set ) ) ) st p : ( ( Function-like quasi_total bijective ) ( Relation-like Seg 2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( non empty V40() 2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) -element ) Element of bool NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty non trivial cup-closed diff-closed preBoolean V40() ) set ) ) -defined Seg 2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( non empty V40() 2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) -element ) Element of bool NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty non trivial cup-closed diff-closed preBoolean V40() ) set ) ) -valued Function-like one-to-one non empty total quasi_total onto bijective V40() ) Permutation of Seg 2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( non empty V40() 2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) -element ) Element of bool NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty non trivial cup-closed diff-closed preBoolean V40() ) set ) ) ) is being_transposition holds
p : ( ( Function-like quasi_total bijective ) ( Relation-like Seg 2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( non empty V40() 2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) -element ) Element of bool NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty non trivial cup-closed diff-closed preBoolean V40() ) set ) ) -defined Seg 2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( non empty V40() 2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) -element ) Element of bool NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty non trivial cup-closed diff-closed preBoolean V40() ) set ) ) -valued Function-like one-to-one non empty total quasi_total onto bijective V40() ) Permutation of Seg 2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( non empty V40() 2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) -element ) Element of bool NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty non trivial cup-closed diff-closed preBoolean V40() ) set ) ) ) = <*2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ,1 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) *> : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -defined Function-like non empty V40() 2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) -element FinSequence-like FinSubsequence-like ) set ) ;

for D being ( ( non empty ) ( non empty ) set )
for f being ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like V40() FinSequence-like FinSubsequence-like ) FinSequence of D : ( ( non empty ) ( non empty ) set ) )
for k2 being ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) st 1 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) <= k2 : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) & k2 : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) < len f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like V40() FinSequence-like FinSubsequence-like ) FinSequence of b₁ : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) holds
f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like V40() FinSequence-like FinSubsequence-like ) FinSequence of b₁ : ( ( non empty ) ( non empty ) set ) ) = (mid (f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like V40() FinSequence-like FinSubsequence-like ) FinSequence of b₁ : ( ( non empty ) ( non empty ) set ) ) ,1 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ,k2 : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) )) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like V40() FinSequence-like FinSubsequence-like ) FinSequence of b₁ : ( ( non empty ) ( non empty ) set ) ) ^ (mid (f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like V40() FinSequence-like FinSubsequence-like ) FinSequence of b₁ : ( ( non empty ) ( non empty ) set ) ) ,(k2 : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) + 1 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ,(len f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like V40() FinSequence-like FinSubsequence-like ) FinSequence of b₁ : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) )) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like V40() FinSequence-like FinSubsequence-like ) FinSequence of b₁ : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like V40() FinSequence-like FinSubsequence-like ) FinSequence of b₁ : ( ( non empty ) ( non empty ) set ) ) ;

for D being ( ( non empty ) ( non empty ) set )
for f being ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like V40() FinSequence-like FinSubsequence-like ) FinSequence of D : ( ( non empty ) ( non empty ) set ) ) st 2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) <= len f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like V40() FinSequence-like FinSubsequence-like ) FinSequence of b₁ : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) holds
f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like V40() FinSequence-like FinSubsequence-like ) FinSequence of b₁ : ( ( non empty ) ( non empty ) set ) ) = (f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like V40() FinSequence-like FinSubsequence-like ) FinSequence of b₁ : ( ( non empty ) ( non empty ) set ) ) | ((len f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like V40() FinSequence-like FinSubsequence-like ) FinSequence of b₁ : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) -' 2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like V40() FinSequence-like FinSubsequence-like ) FinSequence of b₁ : ( ( non empty ) ( non empty ) set ) ) ^ (mid (f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like V40() FinSequence-like FinSubsequence-like ) FinSequence of b₁ : ( ( non empty ) ( non empty ) set ) ) ,((len f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like V40() FinSequence-like FinSubsequence-like ) FinSequence of b₁ : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) -' 1 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ,(len f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like V40() FinSequence-like FinSubsequence-like ) FinSequence of b₁ : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) )) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like V40() FinSequence-like FinSubsequence-like ) FinSequence of b₁ : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like V40() FinSequence-like FinSubsequence-like ) FinSequence of b₁ : ( ( non empty ) ( non empty ) set ) ) ;

for D being ( ( non empty ) ( non empty ) set )
for f being ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like V40() FinSequence-like FinSubsequence-like ) FinSequence of D : ( ( non empty ) ( non empty ) set ) ) st 1 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) <= len f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like V40() FinSequence-like FinSubsequence-like ) FinSequence of b₁ : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) holds
f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like V40() FinSequence-like FinSubsequence-like ) FinSequence of b₁ : ( ( non empty ) ( non empty ) set ) ) = (f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like V40() FinSequence-like FinSubsequence-like ) FinSequence of b₁ : ( ( non empty ) ( non empty ) set ) ) | ((len f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like V40() FinSequence-like FinSubsequence-like ) FinSequence of b₁ : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) -' 1 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like V40() FinSequence-like FinSubsequence-like ) FinSequence of b₁ : ( ( non empty ) ( non empty ) set ) ) ^ (mid (f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like V40() FinSequence-like FinSubsequence-like ) FinSequence of b₁ : ( ( non empty ) ( non empty ) set ) ) ,(len f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like V40() FinSequence-like FinSubsequence-like ) FinSequence of b₁ : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ,(len f : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like V40() FinSequence-like FinSubsequence-like ) FinSequence of b₁ : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) )) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like V40() FinSequence-like FinSubsequence-like ) FinSequence of b₁ : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like V40() FinSequence-like FinSubsequence-like ) FinSequence of b₁ : ( ( non empty ) ( non empty ) set ) ) ;

for a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st ex q being ( ( ) ( Relation-like Seg (len (Permutations 2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( non empty permutational ) set ) ) : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( V40() len (Permutations 2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( non empty permutational ) set ) : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) -element ) Element of bool NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty non trivial cup-closed diff-closed preBoolean V40() ) set ) ) -defined Seg (len (Permutations 2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( non empty permutational ) set ) ) : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( V40() len (Permutations 2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( non empty permutational ) set ) : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) -element ) Element of bool NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty non trivial cup-closed diff-closed preBoolean V40() ) set ) ) -valued Function-like one-to-one total quasi_total onto bijective V40() ) Element of Permutations 2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( non empty permutational ) set ) ) st
( q : ( ( ) ( Relation-like Seg (len (Permutations 2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( non empty permutational ) set ) ) : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( V40() len (Permutations 2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( non empty permutational ) set ) : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) -element ) Element of bool NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty non trivial cup-closed diff-closed preBoolean V40() ) set ) ) -defined Seg (len (Permutations 2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( non empty permutational ) set ) ) : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( V40() len (Permutations 2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( non empty permutational ) set ) : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) -element ) Element of bool NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty non trivial cup-closed diff-closed preBoolean V40() ) set ) ) -valued Function-like one-to-one total quasi_total onto bijective V40() ) Element of Permutations 2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( non empty permutational ) set ) ) = a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & q : ( ( ) ( Relation-like Seg (len (Permutations 2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( non empty permutational ) set ) ) : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( V40() len (Permutations 2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( non empty permutational ) set ) : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) -element ) Element of bool NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty non trivial cup-closed diff-closed preBoolean V40() ) set ) ) -defined Seg (len (Permutations 2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( non empty permutational ) set ) ) : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( V40() len (Permutations 2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( non empty permutational ) set ) : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) -element ) Element of bool NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty non trivial cup-closed diff-closed preBoolean V40() ) set ) ) -valued Function-like one-to-one total quasi_total onto bijective V40() ) Element of Permutations 2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( non empty permutational ) set ) ) is being_transposition ) holds
a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = <*2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ,1 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) *> : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -defined Function-like non empty V40() 2 : ( ( ) ( non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) -element FinSequence-like FinSubsequence-like ) set ) ;

for n being ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) )
for a, b being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for pa, pb being ( ( ) ( Relation-like Seg (len (Permutations b₁ : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( non empty permutational ) set ) ) : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( V40() len (Permutations b₁ : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( non empty permutational ) set ) : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) -element ) Element of bool NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty non trivial cup-closed diff-closed preBoolean V40() ) set ) ) -defined Seg (len (Permutations b₁ : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( non empty permutational ) set ) ) : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( V40() len (Permutations b₁ : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( non empty permutational ) set ) : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) -element ) Element of bool NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty non trivial cup-closed diff-closed preBoolean V40() ) set ) ) -valued Function-like one-to-one total quasi_total onto bijective V40() ) Element of Permutations n : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( non empty permutational ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = pa : ( ( ) ( Relation-like Seg (len (Permutations b₁ : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( non empty permutational ) set ) ) : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( V40() len (Permutations b₁ : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( non empty permutational ) set ) : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) -element ) Element of bool NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty non trivial cup-closed diff-closed preBoolean V40() ) set ) ) -defined Seg (len (Permutations b₁ : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( non empty permutational ) set ) ) : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( V40() len (Permutations b₁ : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( non empty permutational ) set ) : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) -element ) Element of bool NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty non trivial cup-closed diff-closed preBoolean V40() ) set ) ) -valued Function-like one-to-one total quasi_total onto bijective V40() ) Element of Permutations b₁ : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( non empty permutational ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = pb : ( ( ) ( Relation-like Seg (len (Permutations b₁ : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( non empty permutational ) set ) ) : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( V40() len (Permutations b₁ : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( non empty permutational ) set ) : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) -element ) Element of bool NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty non trivial cup-closed diff-closed preBoolean V40() ) set ) ) -defined Seg (len (Permutations b₁ : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( non empty permutational ) set ) ) : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( V40() len (Permutations b₁ : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( non empty permutational ) set ) : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) -element ) Element of bool NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty non trivial cup-closed diff-closed preBoolean V40() ) set ) ) -valued Function-like one-to-one total quasi_total onto bijective V40() ) Element of Permutations b₁ : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( non empty permutational ) set ) ) holds
a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (Group_of_Perm b₁ : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( strict ) ( non empty strict unital Group-like associative ) multMagma ) : ( ( ) ( non empty ) set ) ) = pb : ( ( ) ( Relation-like Seg (len (Permutations b₁ : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( non empty permutational ) set ) ) : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( V40() len (Permutations b₁ : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( non empty permutational ) set ) : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) -element ) Element of bool NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty non trivial cup-closed diff-closed preBoolean V40() ) set ) ) -defined Seg (len (Permutations b₁ : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( non empty permutational ) set ) ) : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( V40() len (Permutations b₁ : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( non empty permutational ) set ) : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) -element ) Element of bool NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty non trivial cup-closed diff-closed preBoolean V40() ) set ) ) -valued Function-like one-to-one total quasi_total onto bijective V40() ) Element of Permutations b₁ : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( non empty permutational ) set ) ) * pa : ( ( ) ( Relation-like Seg (len (Permutations b₁ : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( non empty permutational ) set ) ) : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( V40() len (Permutations b₁ : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( non empty permutational ) set ) : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) -element ) Element of bool NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty non trivial cup-closed diff-closed preBoolean V40() ) set ) ) -defined Seg (len (Permutations b₁ : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( non empty permutational ) set ) ) : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( V40() len (Permutations b₁ : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( non empty permutational ) set ) : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) -element ) Element of bool NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty non trivial cup-closed diff-closed preBoolean V40() ) set ) ) -valued Function-like one-to-one total quasi_total onto bijective V40() ) Element of Permutations b₁ : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( non empty permutational ) set ) ) : ( ( Function-like ) ( Relation-like Seg (len (Permutations b₁ : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( non empty permutational ) set ) ) : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( V40() len (Permutations b₁ : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( non empty permutational ) set ) : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) -element ) Element of bool NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty non trivial cup-closed diff-closed preBoolean V40() ) set ) ) -defined Seg (len (Permutations b₁ : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( non empty permutational ) set ) ) : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( V40() len (Permutations b₁ : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( non empty permutational ) set ) : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) -element ) Element of bool NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty non trivial cup-closed diff-closed preBoolean V40() ) set ) ) -valued Function-like one-to-one total quasi_total onto bijective V40() ) Element of bool [:(Seg (len (Permutations b₁ : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( non empty permutational ) set ) ) : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( V40() len (Permutations b₁ : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( non empty permutational ) set ) : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) -element ) Element of bool NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty non trivial cup-closed diff-closed preBoolean V40() ) set ) ) ,(Seg (len (Permutations b₁ : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( non empty permutational ) set ) ) : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( V40() len (Permutations b₁ : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( non empty permutational ) set ) : ( ( ) ( V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal ) Element of NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) -element ) Element of bool NAT : ( ( ) ( non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty non trivial cup-closed diff-closed preBoolean V40() ) set ) ) :] : ( ( ) ( V40() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean V40() V44() ) set ) ) ;