GOBOARD2

:: GOBOARD2 semantic presentation

begin

for f1, f2 being ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) )
for n, m being ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) st len f1 : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) : ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) < n : ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) & n : ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) + 1 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) <= len (f1 : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) ^ f2 : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V52() FinSequence-like FinSubsequence-like ) FinSequence of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) & m : ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) + (len f1 : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) : ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) = n : ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) holds
LSeg ((f1 : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) ^ f2 : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V52() FinSequence-like FinSubsequence-like ) FinSequence of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) ,n : ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( ) ( ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) = LSeg (f2 : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) ,m : ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( ) ( ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ;

theorem :: GOBOARD2:6

for f, g being ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) holds L~ f : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) c= L~ (f : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) ^ g : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V52() FinSequence-like FinSubsequence-like ) FinSequence of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ;

theorem :: GOBOARD2:7

theorem :: GOBOARD2:8

for f1, f2 being ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) st f1 : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) is special & f2 : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) is special & ( (f1 : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) /. (len f1 : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( ) ( V35() 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) -element FinSequence-like ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V22() ext-real V26() ) Element of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) ) = (f2 : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) /. 1 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( ) ( V35() 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) -element FinSequence-like ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V22() ext-real V26() ) Element of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) ) or (f1 : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) /. (len f1 : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( ) ( V35() 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) -element FinSequence-like ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V22() ext-real V26() ) Element of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) ) = (f2 : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) /. 1 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( ) ( V35() 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) -element FinSequence-like ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( V22() ext-real V26() ) Element of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) ) ) holds
f1 : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) ^ f2 : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V52() FinSequence-like FinSubsequence-like ) FinSequence of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) is special ;

theorem :: GOBOARD2:9

theorem :: GOBOARD2:10

registration

let f be ( ( non empty ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) ;

cluster X_axis f : ( ( non empty ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V52() FinSequence-like FinSubsequence-like ) FinSequence of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) -valued Function-like V33() V34() V35() V52() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) ) -> non empty ;

cluster Y_axis f : ( ( non empty ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V52() FinSequence-like FinSubsequence-like ) FinSequence of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) -valued Function-like V33() V34() V35() V52() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) ) -> non empty ;

end;

theorem :: GOBOARD2:11

theorem :: GOBOARD2:12

for f being ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) )
for G being ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( Relation-like non empty-yielding NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined K246( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M12( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) -valued Function-like V52() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) st ( for n being ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) st n : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) in dom f : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) : ( ( ) ( V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() ) Element of bool NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) : ( ( ) ( non trivial V52() ) set ) ) holds
ex i, j being ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) st
( [i : ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ,j : ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ] : ( ( ) ( ) set ) in Indices G : ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( Relation-like non empty-yielding NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined K246( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M12( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) -valued Function-like V52() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) : ( ( ) ( ) set ) & f : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) /. n : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) : ( ( ) ( V35() 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) -element FinSequence-like ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) = G : ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( Relation-like non empty-yielding NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined K246( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M12( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) -valued Function-like V52() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) * (i : ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ,j : ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( ) ( V35() 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) -element FinSequence-like ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) ) ) & f : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) is special & ( for n being ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) st n : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) in dom f : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) : ( ( ) ( V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() ) Element of bool NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) : ( ( ) ( non trivial V52() ) set ) ) & n : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) + 1 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) : ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) in dom f : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) : ( ( ) ( V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() ) Element of bool NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) : ( ( ) ( non trivial V52() ) set ) ) holds
f : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) /. n : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) : ( ( ) ( V35() 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) -element FinSequence-like ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) <> f : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) /. (n : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) + 1 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) : ( ( ) ( V35() 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) -element FinSequence-like ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) ) holds
ex g being ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) st
( g : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) is_sequence_on G : ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( Relation-like non empty-yielding NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined K246( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M12( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) -valued Function-like V52() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) & L~ f : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) = L~ g : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) & g : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) /. 1 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) : ( ( ) ( V35() 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) -element FinSequence-like ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) = f : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) /. 1 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) : ( ( ) ( V35() 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) -element FinSequence-like ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) & g : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) /. (len g : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) : ( ( ) ( V35() 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) -element FinSequence-like ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) = f : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) /. (len f : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) : ( ( ) ( V35() 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) -element FinSequence-like ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) & len f : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) : ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) <= len g : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) : ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) ;

definition

let v1, v2 be ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) -valued Function-like V33() V34() V35() V52() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) ) ;
assume v1 : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) -valued Function-like V33() V34() V35() V52() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) ) <> {} : ( ( ) ( ) set ) ;

func GoB (v1,v2) -> ( ( tabular ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined K246( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M12( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) -valued Function-like V52() FinSequence-like FinSubsequence-like tabular ) Matrix of ) means :: GOBOARD2:def 1
( len it : ( ( Function-like V30([:v1 : ( ( ) ( ) set ) ,v1 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ,v1 : ( ( ) ( ) set ) ) ) ( Relation-like [:v1 : ( ( ) ( ) set ) ,v1 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) -defined v1 : ( ( ) ( ) set ) -valued Function-like V30([:v1 : ( ( ) ( ) set ) ,v1 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ,v1 : ( ( ) ( ) set ) ) ) Element of bool [:[:v1 : ( ( ) ( ) set ) ,v1 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ,v1 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) = len v1 : ( ( ) ( ) set ) : ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) & width it : ( ( Function-like V30([:v1 : ( ( ) ( ) set ) ,v1 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ,v1 : ( ( ) ( ) set ) ) ) ( Relation-like [:v1 : ( ( ) ( ) set ) ,v1 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) -defined v1 : ( ( ) ( ) set ) -valued Function-like V30([:v1 : ( ( ) ( ) set ) ,v1 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ,v1 : ( ( ) ( ) set ) ) ) Element of bool [:[:v1 : ( ( ) ( ) set ) ,v1 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ,v1 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) = len v2 : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) & ( for n, m being ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) st [n : ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ,m : ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ] : ( ( ) ( ) set ) in Indices it : ( ( Function-like V30([:v1 : ( ( ) ( ) set ) ,v1 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ,v1 : ( ( ) ( ) set ) ) ) ( Relation-like [:v1 : ( ( ) ( ) set ) ,v1 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) -defined v1 : ( ( ) ( ) set ) -valued Function-like V30([:v1 : ( ( ) ( ) set ) ,v1 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ,v1 : ( ( ) ( ) set ) ) ) Element of bool [:[:v1 : ( ( ) ( ) set ) ,v1 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ,v1 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) holds
it : ( ( Function-like V30([:v1 : ( ( ) ( ) set ) ,v1 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ,v1 : ( ( ) ( ) set ) ) ) ( Relation-like [:v1 : ( ( ) ( ) set ) ,v1 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) -defined v1 : ( ( ) ( ) set ) -valued Function-like V30([:v1 : ( ( ) ( ) set ) ,v1 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ,v1 : ( ( ) ( ) set ) ) ) Element of bool [:[:v1 : ( ( ) ( ) set ) ,v1 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ,v1 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) * (n : ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ,m : ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( ) ( V35() 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) -element FinSequence-like ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) = |[(v1 : ( ( ) ( ) set ) . n : ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( ) ( V22() ext-real V26() ) Element of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) ) ,(v2 : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) . m : ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( ) ( V22() ext-real V26() ) Element of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) ) ]| : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined Function-like non empty V33() V34() V35() V52() 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) -element FinSequence-like FinSubsequence-like ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) ) );

end;

registration

let v1, v2 be ( ( non empty ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) -valued Function-like non empty V33() V34() V35() V52() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) ) ;

cluster GoB (v1 : ( ( non empty ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) -valued Function-like non empty V33() V34() V35() V52() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) ) ,v2 : ( ( non empty ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) -valued Function-like non empty V33() V34() V35() V52() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) ) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined K246( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M12( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) -valued Function-like V52() FinSequence-like FinSubsequence-like tabular ) Matrix of ) -> V3() tabular X_equal-in-line Y_equal-in-column ;

end;

registration

let v1, v2 be ( ( non empty increasing ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) -valued Function-like one-to-one non empty V33() V34() V35() increasing V39() V52() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) ) ;

cluster GoB (v1 : ( ( non empty increasing ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) -valued Function-like one-to-one non empty V33() V34() V35() increasing V39() V52() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) ) ,v2 : ( ( non empty increasing ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) -valued Function-like one-to-one non empty V33() V34() V35() increasing V39() V52() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) ) ) : ( ( tabular ) ( Relation-like V3() NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined K246( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M12( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) -valued Function-like V52() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column ) Matrix of ) -> tabular Y_increasing-in-line X_increasing-in-column ;

end;

definition

func GoB f -> ( ( tabular ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined K246( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M12( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) -valued Function-like V52() FinSequence-like FinSubsequence-like tabular ) Matrix of ) equals :: GOBOARD2:def 2
GoB ((Incr (X_axis f : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) -valued Function-like V33() V34() V35() V52() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) ) ) : ( ( increasing ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) -valued Function-like one-to-one V33() V34() V35() increasing V39() V52() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) ) ,(Incr (Y_axis f : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) -valued Function-like V33() V34() V35() V52() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) ) ) : ( ( increasing ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) -valued Function-like one-to-one V33() V34() V35() increasing V39() V52() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) ) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined K246( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M12( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) -valued Function-like V52() FinSequence-like FinSubsequence-like tabular ) Matrix of ) ;

end;

registration

cluster GoB f : ( ( non empty ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V52() FinSequence-like FinSubsequence-like ) FinSequence of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( tabular ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined K246( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M12( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) -valued Function-like V52() FinSequence-like FinSubsequence-like tabular ) Matrix of ) -> V3() tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ;

end;

theorem :: GOBOARD2:13

for f being ( ( non empty ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) holds
( len (GoB f : ( ( non empty ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) ) : ( ( tabular ) ( Relation-like V3() NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined K246( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M12( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) -valued Function-like V52() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Matrix of ) : ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) = card (rng (X_axis f : ( ( non empty ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) -valued Function-like non empty V33() V34() V35() V52() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) ) ) : ( ( ) ( non empty V45() V46() V47() V52() V61() V62() V63() V64() V65() ) set ) : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) set ) ) & width (GoB f : ( ( non empty ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) ) : ( ( tabular ) ( Relation-like V3() NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined K246( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M12( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) -valued Function-like V52() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Matrix of ) : ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) = card (rng (Y_axis f : ( ( non empty ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) -valued Function-like non empty V33() V34() V35() V52() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) ) ) : ( ( ) ( non empty V45() V46() V47() V52() V61() V62() V63() V64() V65() ) set ) : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) set ) ) ) ;

theorem :: GOBOARD2:14

for f being ( ( non empty ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) )
for n being ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) st n : ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) in dom f : ( ( non empty ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() ) Element of bool NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) : ( ( ) ( non trivial V52() ) set ) ) holds
ex i, j being ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) st
( [i : ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ,j : ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ] : ( ( ) ( ) set ) in Indices (GoB f : ( ( non empty ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) ) : ( ( tabular ) ( Relation-like V3() NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined K246( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M12( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) -valued Function-like V52() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Matrix of ) : ( ( ) ( ) set ) & f : ( ( non empty ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) /. n : ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) : ( ( ) ( V35() 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) -element FinSequence-like ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) = (GoB f : ( ( non empty ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) ) : ( ( tabular ) ( Relation-like V3() NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined K246( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M12( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) -valued Function-like V52() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Matrix of ) * (i : ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ,j : ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( ) ( V35() 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) -element FinSequence-like ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: GOBOARD2:15

for n being ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) )
for f being ( ( non empty ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) st n : ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) in dom f : ( ( non empty ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() ) Element of bool NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) : ( ( ) ( non trivial V52() ) set ) ) & ( for m being ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) st m : ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) in dom f : ( ( non empty ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() ) Element of bool NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) : ( ( ) ( non trivial V52() ) set ) ) holds
(X_axis f : ( ( non empty ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) -valued Function-like non empty V33() V34() V35() V52() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) ) . n : ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) : ( ( ) ( V22() ext-real V26() ) Element of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) ) <= (X_axis f : ( ( non empty ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) -valued Function-like non empty V33() V34() V35() V52() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) ) . m : ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) : ( ( ) ( V22() ext-real V26() ) Element of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) ) ) holds
f : ( ( non empty ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) /. n : ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) : ( ( ) ( V35() 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) -element FinSequence-like ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) in rng (Line ((GoB f : ( ( non empty ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) ) : ( ( tabular ) ( Relation-like V3() NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined K246( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M12( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) -valued Function-like V52() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Matrix of ) ,1 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) )) : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V52() FinSequence-like FinSubsequence-like ) M13( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ,K247((width (GoB b₂ : ( ( non empty ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) ) : ( ( tabular ) ( Relation-like V3() NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined K246( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M12( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) -valued Function-like V52() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Matrix of ) ) : ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional FinSequence-membered ) M12( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) )) : ( ( ) ( V52() ) set ) ;

theorem :: GOBOARD2:16

for n being ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) )
for f being ( ( non empty ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) st n : ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) in dom f : ( ( non empty ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() ) Element of bool NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) : ( ( ) ( non trivial V52() ) set ) ) & ( for m being ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) st m : ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) in dom f : ( ( non empty ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() ) Element of bool NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) : ( ( ) ( non trivial V52() ) set ) ) holds
(X_axis f : ( ( non empty ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) -valued Function-like non empty V33() V34() V35() V52() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) ) . m : ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) : ( ( ) ( V22() ext-real V26() ) Element of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) ) <= (X_axis f : ( ( non empty ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) -valued Function-like non empty V33() V34() V35() V52() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) ) . n : ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) : ( ( ) ( V22() ext-real V26() ) Element of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) ) ) holds
f : ( ( non empty ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) /. n : ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) : ( ( ) ( V35() 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) -element FinSequence-like ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) in rng (Line ((GoB f : ( ( non empty ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) ) : ( ( tabular ) ( Relation-like V3() NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined K246( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M12( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) -valued Function-like V52() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Matrix of ) ,(len (GoB f : ( ( non empty ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) ) : ( ( tabular ) ( Relation-like V3() NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined K246( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M12( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) -valued Function-like V52() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Matrix of ) ) : ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) )) : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V52() FinSequence-like FinSubsequence-like ) M13( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ,K247((width (GoB b₂ : ( ( non empty ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) ) : ( ( tabular ) ( Relation-like V3() NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined K246( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M12( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) -valued Function-like V52() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Matrix of ) ) : ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional FinSequence-membered ) M12( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) )) : ( ( ) ( V52() ) set ) ;

theorem :: GOBOARD2:17

for n being ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) )
for f being ( ( non empty ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) st n : ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) in dom f : ( ( non empty ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() ) Element of bool NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) : ( ( ) ( non trivial V52() ) set ) ) & ( for m being ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) st m : ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) in dom f : ( ( non empty ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() ) Element of bool NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) : ( ( ) ( non trivial V52() ) set ) ) holds
(Y_axis f : ( ( non empty ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) -valued Function-like non empty V33() V34() V35() V52() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) ) . n : ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) : ( ( ) ( V22() ext-real V26() ) Element of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) ) <= (Y_axis f : ( ( non empty ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) -valued Function-like non empty V33() V34() V35() V52() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) ) . m : ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) : ( ( ) ( V22() ext-real V26() ) Element of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) ) ) holds
f : ( ( non empty ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) /. n : ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) : ( ( ) ( V35() 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) -element FinSequence-like ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) in rng (Col ((GoB f : ( ( non empty ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) ) : ( ( tabular ) ( Relation-like V3() NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined K246( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M12( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) -valued Function-like V52() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Matrix of ) ,1 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) )) : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V52() FinSequence-like FinSubsequence-like ) M13( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ,K247((len (GoB b₂ : ( ( non empty ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) ) : ( ( tabular ) ( Relation-like V3() NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined K246( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M12( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) -valued Function-like V52() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Matrix of ) ) : ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional FinSequence-membered ) M12( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) )) : ( ( ) ( V52() ) set ) ;

theorem :: GOBOARD2:18

for n being ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) )
for f being ( ( non empty ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) st n : ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) in dom f : ( ( non empty ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() ) Element of bool NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) : ( ( ) ( non trivial V52() ) set ) ) & ( for m being ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) st m : ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) in dom f : ( ( non empty ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() ) Element of bool NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) : ( ( ) ( non trivial V52() ) set ) ) holds
(Y_axis f : ( ( non empty ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) -valued Function-like non empty V33() V34() V35() V52() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) ) . m : ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) : ( ( ) ( V22() ext-real V26() ) Element of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) ) <= (Y_axis f : ( ( non empty ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) -valued Function-like non empty V33() V34() V35() V52() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) ) . n : ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) : ( ( ) ( V22() ext-real V26() ) Element of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) ) ) holds
f : ( ( non empty ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) /. n : ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) : ( ( ) ( V35() 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) -element FinSequence-like ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) in rng (Col ((GoB f : ( ( non empty ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) ) : ( ( tabular ) ( Relation-like V3() NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined K246( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M12( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) -valued Function-like V52() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Matrix of ) ,(width (GoB f : ( ( non empty ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) ) : ( ( tabular ) ( Relation-like V3() NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined K246( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M12( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) -valued Function-like V52() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Matrix of ) ) : ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) )) : ( ( ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V52() FinSequence-like FinSubsequence-like ) M13( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ,K247((len (GoB b₂ : ( ( non empty ) ( Relation-like NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V52() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) ) : ( ( tabular ) ( Relation-like V3() NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) -defined K246( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty FinSequence-membered ) M12( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) -valued Function-like V52() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Matrix of ) ) : ( ( ) ( V17() V21() V22() ext-real non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional FinSequence-membered ) M12( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V17() V21() V22() ext-real positive non negative V26() V43() V44() V45() V46() V47() V48() V49() V50() V52() V61() V62() V63() V64() V65() cardinal ) Element of NAT : ( ( ) ( non trivial V17() V45() V46() V47() V48() V49() V50() V51() V52() V63() cardinal limit_cardinal ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V52() V63() V64() V66() ) set ) : ( ( ) ( non trivial V52() ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V129() V154() V155() V156() V157() V158() V159() V160() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) )) )) : ( ( ) ( V52() ) set ) ;