let E be ( ( non empty ) ( non empty ) set ) ;
let S be ( ( non empty ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) ;
let F be ( ( Function-like V43(E : ( ( non empty ) ( non empty ) set ) ,S : ( ( non empty ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) ) ) ( V1() V4(E : ( ( non empty ) ( non empty ) set ) ) V5(S : ( ( non empty ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) ) Function-like V43(E : ( ( non empty ) ( non empty ) set ) ,S : ( ( non empty ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) ) ) Function of E : ( ( non empty ) ( non empty ) set ) ,S : ( ( non empty ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) ) ;
let e be ( ( ) ( ) Element of E : ( ( non empty ) ( non empty ) set ) ) ;
:: original: .
redefine func F . e -> ( ( ) ( V1() V4( NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) Function-like V24() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) ;

for f being ( ( ) ( V1() V4( NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) Function-like V24() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) )
for G being ( ( tabular ) ( V1() V4( NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) ) Function-like V24() FinSequence-like FinSubsequence-like tabular ) Matrix of ) st f : ( ( ) ( V1() V4( NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) Function-like V24() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) is_sequence_on G : ( ( tabular ) ( V1() V4( NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) ) Function-like V24() FinSequence-like FinSubsequence-like tabular ) Matrix of ) holds
rng f : ( ( ) ( V1() V4( NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) Function-like V24() FinSequence-like FinSubsequence-like ) FinSequence of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) c= Values G : ( ( tabular ) ( V1() V4( NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) ) Function-like V24() FinSequence-like FinSubsequence-like tabular ) Matrix of ) : ( ( ) ( ) set ) ;

for i1, j1, j2 being ( ( ) ( V14() V15() V16() V20() V35() V36() ext-real ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) )
for G1, G2 being ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( V1() non empty-yielding V4( NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) st Values G1 : ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( V1() non empty-yielding V4( NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) : ( ( ) ( ) set ) c= Values G2 : ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( V1() non empty-yielding V4( NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) : ( ( ) ( ) set ) & [i1 : ( ( ) ( V14() V15() V16() V20() V35() V36() ext-real ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ,j1 : ( ( ) ( V14() V15() V16() V20() V35() V36() ext-real ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ] : ( ( ) ( ) set ) in Indices G1 : ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( V1() non empty-yielding V4( NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) : ( ( ) ( ) set ) & 1 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) <= j2 : ( ( ) ( V14() V15() V16() V20() V35() V36() ext-real ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & j2 : ( ( ) ( V14() V15() V16() V20() V35() V36() ext-real ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) <= width G2 : ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( V1() non empty-yielding V4( NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) : ( ( ) ( V14() V15() V16() V20() V35() V36() ext-real ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & G1 : ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( V1() non empty-yielding V4( NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) * (i1 : ( ( ) ( V14() V15() V16() V20() V35() V36() ext-real ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ,j1 : ( ( ) ( V14() V15() V16() V20() V35() V36() ext-real ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V31(2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V48() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) = G2 : ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( V1() non empty-yielding V4( NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) * (1 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ,j2 : ( ( ) ( V14() V15() V16() V20() V35() V36() ext-real ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V31(2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V48() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) holds
i1 : ( ( ) ( V14() V15() V16() V20() V35() V36() ext-real ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) = 1 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ;

for i1, j1, j2 being ( ( ) ( V14() V15() V16() V20() V35() V36() ext-real ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) )
for G1, G2 being ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( V1() non empty-yielding V4( NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) st Values G1 : ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( V1() non empty-yielding V4( NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) : ( ( ) ( ) set ) c= Values G2 : ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( V1() non empty-yielding V4( NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) : ( ( ) ( ) set ) & [i1 : ( ( ) ( V14() V15() V16() V20() V35() V36() ext-real ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ,j1 : ( ( ) ( V14() V15() V16() V20() V35() V36() ext-real ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ] : ( ( ) ( ) set ) in Indices G1 : ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( V1() non empty-yielding V4( NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) : ( ( ) ( ) set ) & 1 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) <= j2 : ( ( ) ( V14() V15() V16() V20() V35() V36() ext-real ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & j2 : ( ( ) ( V14() V15() V16() V20() V35() V36() ext-real ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) <= width G2 : ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( V1() non empty-yielding V4( NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) : ( ( ) ( V14() V15() V16() V20() V35() V36() ext-real ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & G1 : ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( V1() non empty-yielding V4( NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) * (i1 : ( ( ) ( V14() V15() V16() V20() V35() V36() ext-real ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ,j1 : ( ( ) ( V14() V15() V16() V20() V35() V36() ext-real ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V31(2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V48() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) = G2 : ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( V1() non empty-yielding V4( NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) * ((len G2 : ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( V1() non empty-yielding V4( NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) ) : ( ( ) ( V14() V15() V16() V20() V35() V36() ext-real ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ,j2 : ( ( ) ( V14() V15() V16() V20() V35() V36() ext-real ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V31(2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V48() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) holds
i1 : ( ( ) ( V14() V15() V16() V20() V35() V36() ext-real ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) = len G1 : ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( V1() non empty-yielding V4( NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) : ( ( ) ( V14() V15() V16() V20() V35() V36() ext-real ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ;

for i1, j1, i2 being ( ( ) ( V14() V15() V16() V20() V35() V36() ext-real ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) )
for G1, G2 being ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( V1() non empty-yielding V4( NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) st Values G1 : ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( V1() non empty-yielding V4( NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) : ( ( ) ( ) set ) c= Values G2 : ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( V1() non empty-yielding V4( NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) : ( ( ) ( ) set ) & [i1 : ( ( ) ( V14() V15() V16() V20() V35() V36() ext-real ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ,j1 : ( ( ) ( V14() V15() V16() V20() V35() V36() ext-real ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ] : ( ( ) ( ) set ) in Indices G1 : ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( V1() non empty-yielding V4( NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) : ( ( ) ( ) set ) & 1 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) <= i2 : ( ( ) ( V14() V15() V16() V20() V35() V36() ext-real ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & i2 : ( ( ) ( V14() V15() V16() V20() V35() V36() ext-real ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) <= len G2 : ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( V1() non empty-yielding V4( NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) : ( ( ) ( V14() V15() V16() V20() V35() V36() ext-real ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & G1 : ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( V1() non empty-yielding V4( NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) * (i1 : ( ( ) ( V14() V15() V16() V20() V35() V36() ext-real ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ,j1 : ( ( ) ( V14() V15() V16() V20() V35() V36() ext-real ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V31(2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V48() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) = G2 : ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( V1() non empty-yielding V4( NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) * (i2 : ( ( ) ( V14() V15() V16() V20() V35() V36() ext-real ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ,1 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V31(2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V48() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) holds
j1 : ( ( ) ( V14() V15() V16() V20() V35() V36() ext-real ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) = 1 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ;

for i1, j1, i2 being ( ( ) ( V14() V15() V16() V20() V35() V36() ext-real ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) )
for G1, G2 being ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( V1() non empty-yielding V4( NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) st Values G1 : ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( V1() non empty-yielding V4( NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) : ( ( ) ( ) set ) c= Values G2 : ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( V1() non empty-yielding V4( NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) : ( ( ) ( ) set ) & [i1 : ( ( ) ( V14() V15() V16() V20() V35() V36() ext-real ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ,j1 : ( ( ) ( V14() V15() V16() V20() V35() V36() ext-real ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ] : ( ( ) ( ) set ) in Indices G1 : ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( V1() non empty-yielding V4( NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) : ( ( ) ( ) set ) & 1 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) <= i2 : ( ( ) ( V14() V15() V16() V20() V35() V36() ext-real ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & i2 : ( ( ) ( V14() V15() V16() V20() V35() V36() ext-real ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) <= len G2 : ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( V1() non empty-yielding V4( NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) : ( ( ) ( V14() V15() V16() V20() V35() V36() ext-real ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & G1 : ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( V1() non empty-yielding V4( NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) * (i1 : ( ( ) ( V14() V15() V16() V20() V35() V36() ext-real ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ,j1 : ( ( ) ( V14() V15() V16() V20() V35() V36() ext-real ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V31(2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V48() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) = G2 : ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( V1() non empty-yielding V4( NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) * (i2 : ( ( ) ( V14() V15() V16() V20() V35() V36() ext-real ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ,(width G2 : ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( V1() non empty-yielding V4( NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) ) : ( ( ) ( V14() V15() V16() V20() V35() V36() ext-real ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V31(2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V48() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) holds
j1 : ( ( ) ( V14() V15() V16() V20() V35() V36() ext-real ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) = width G1 : ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( V1() non empty-yielding V4( NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) : ( ( ) ( V14() V15() V16() V20() V35() V36() ext-real ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ;

for i1, j1, i2, j2 being ( ( ) ( V14() V15() V16() V20() V35() V36() ext-real ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) )
for G1, G2 being ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( V1() non empty-yielding V4( NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) st Values G1 : ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( V1() non empty-yielding V4( NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) : ( ( ) ( ) set ) c= Values G2 : ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( V1() non empty-yielding V4( NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) : ( ( ) ( ) set ) & 1 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) <= i1 : ( ( ) ( V14() V15() V16() V20() V35() V36() ext-real ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & i1 : ( ( ) ( V14() V15() V16() V20() V35() V36() ext-real ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) < len G1 : ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( V1() non empty-yielding V4( NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) : ( ( ) ( V14() V15() V16() V20() V35() V36() ext-real ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & 1 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) <= j1 : ( ( ) ( V14() V15() V16() V20() V35() V36() ext-real ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & j1 : ( ( ) ( V14() V15() V16() V20() V35() V36() ext-real ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) <= width G1 : ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( V1() non empty-yielding V4( NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) : ( ( ) ( V14() V15() V16() V20() V35() V36() ext-real ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & 1 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) <= i2 : ( ( ) ( V14() V15() V16() V20() V35() V36() ext-real ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & i2 : ( ( ) ( V14() V15() V16() V20() V35() V36() ext-real ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) < len G2 : ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( V1() non empty-yielding V4( NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) : ( ( ) ( V14() V15() V16() V20() V35() V36() ext-real ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & 1 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) <= j2 : ( ( ) ( V14() V15() V16() V20() V35() V36() ext-real ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & j2 : ( ( ) ( V14() V15() V16() V20() V35() V36() ext-real ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) <= width G2 : ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( V1() non empty-yielding V4( NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) : ( ( ) ( V14() V15() V16() V20() V35() V36() ext-real ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & G1 : ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( V1() non empty-yielding V4( NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) * (i1 : ( ( ) ( V14() V15() V16() V20() V35() V36() ext-real ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ,j1 : ( ( ) ( V14() V15() V16() V20() V35() V36() ext-real ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V31(2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V48() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) = G2 : ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( V1() non empty-yielding V4( NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) * (i2 : ( ( ) ( V14() V15() V16() V20() V35() V36() ext-real ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ,j2 : ( ( ) ( V14() V15() V16() V20() V35() V36() ext-real ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V31(2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V48() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) holds
(G2 : ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( V1() non empty-yielding V4( NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) * ((i2 : ( ( ) ( V14() V15() V16() V20() V35() V36() ext-real ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V14() V15() V16() V20() V35() V36() ext-real ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ,j2 : ( ( ) ( V14() V15() V16() V20() V35() V36() ext-real ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( ) ( V31(2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V48() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V35() V36() ext-real ) Element of REAL : ( ( ) ( ) set ) ) <= (G1 : ( ( non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) ( V1() non empty-yielding V4( NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) * : ( ( ) ( functional non empty FinSequence-membered ) FinSequenceSet of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) ) Function-like V24() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ) Go-board) * ((i1 : ( ( ) ( V14() V15() V16() V20() V35() V36() ext-real ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V14() V15() V16() V20() V35() V36() ext-real ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ,j1 : ( ( ) ( V14() V15() V16() V20() V35() V36() ext-real ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( ) ( V31(2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V48() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty V14() V15() V16() V20() V35() V36() ext-real positive ) Element of NAT : ( ( ) ( non empty V14() V15() V16() ) Element of K19(REAL : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V122() V147() V148() V149() V150() V151() V152() V153() strict ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) `1 : ( ( ) ( V35() V36() ext-real ) Element of REAL : ( ( ) ( ) set ) ) ;