:: TOPALG_2 semantic presentation

begin

registration
let n be ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) ;
cluster non empty convex for ( ( ) ( ) Element of bool the carrier of (TOP-REAL n : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous V240() V241() ) RLTopStruct ) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) ;
end;

definition
let n be ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) ;
let T be ( ( ) ( TopSpace-like ) SubSpace of TOP-REAL n : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous V240() V241() ) RLTopStruct ) ) ;
attr T is convex means :: TOPALG_2:def 1
 [#] T : ( ( ) ( natural V11() real ext-real V36() V37() ) Element of n : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of bool the carrier of T : ( ( ) ( natural V11() real ext-real V36() V37() ) Element of n : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) is ( ( convex ) ( convex ) Subset of ) ;
end;

registration
let n be ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) ;
cluster non empty convex -> non empty pathwise_connected for ( ( ) ( ) SubSpace of TOP-REAL n : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous V240() V241() ) RLTopStruct ) ) ;
end;

registration
let n be ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) ;
cluster non empty strict TopSpace-like convex for ( ( ) ( ) SubSpace of TOP-REAL n : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous V240() V241() ) RLTopStruct ) ) ;
end;

theorem :: TOPALG_2:1
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for Y being ( ( non empty ) ( non empty TopSpace-like ) SubSpace of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) )
for x1, x2 being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) )
for y1, y2 being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) )
for f being ( ( ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Path of y1 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,y2 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) st x1 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) = y1 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) & x2 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) = y2 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) & y1 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,y2 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) are_connected holds
f : ( ( ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Path of b5 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b6 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) is ( ( ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Path of x1 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,x2 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) ;

definition
let n be ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) ;
let T be ( ( non empty convex ) ( non empty TopSpace-like pathwise_connected convex ) SubSpace of TOP-REAL n : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous V240() V241() ) RLTopStruct ) ) ;
let P, Q be ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of T : ( ( non empty convex ) ( non empty TopSpace-like pathwise_connected convex ) SubSpace of TOP-REAL n : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous V240() V241() ) RLTopStruct ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty V166() V167() V168() ) set ) , ( ( ) ( non empty ) set ) ) ;
func ConvexHomotopy (P,Q) -> ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of [:I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) ,I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of T : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( ) set ) ) means :: TOPALG_2:def 2
 for s, t being ( ( ) ( V11() real ext-real ) Element of ( ( ) ( non empty V166() V167() V168() ) set ) )
for a1, b1 being ( ( ) ( Relation-like REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) -valued Function-like V47(n : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V158() ) Point of ( ( ) ( non empty ) set ) ) st a1 : ( ( ) ( Relation-like REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) -valued Function-like V47(n : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V158() ) Point of ( ( ) ( non empty ) set ) ) = P : ( ( Function-like quasi_total ) ( Relation-like [:n : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) ,n : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( ) set ) -defined n : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) -valued Function-like quasi_total ) Element of bool [:[:n : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) ,n : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( ) set ) ,n : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) . s : ( ( ) ( V11() real ext-real ) Element of ( ( ) ( non empty V166() V167() V168() ) set ) ) : ( ( ) ( ) Element of the carrier of T : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) & b1 : ( ( ) ( Relation-like REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) -valued Function-like V47(n : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V158() ) Point of ( ( ) ( non empty ) set ) ) = Q : ( ( Function-like quasi_total ) ( Relation-like [:REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) ,n : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( ) set ) -defined n : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) -valued Function-like quasi_total ) Element of bool [:[:REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) ,n : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( ) set ) ,n : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) . s : ( ( ) ( V11() real ext-real ) Element of ( ( ) ( non empty V166() V167() V168() ) set ) ) : ( ( ) ( ) Element of the carrier of T : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) holds
it : ( ( ) ( ) Element of bool (bool n : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) . (s : ( ( ) ( V11() real ext-real ) Element of ( ( ) ( non empty V166() V167() V168() ) set ) ) ,t : ( ( ) ( V11() real ext-real ) Element of ( ( ) ( non empty V166() V167() V168() ) set ) ) ) : ( ( ) ( ) set ) = ((1 : ( ( ) ( non empty natural V11() real ext-real positive V36() V37() V166() V167() V168() V169() V170() V171() V257() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) - t : ( ( ) ( V11() real ext-real ) Element of ( ( ) ( non empty V166() V167() V168() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) ) * a1 : ( ( ) ( Relation-like REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) -valued Function-like V47(n : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V158() ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) -valued Function-like V47(n : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V158() ) Element of the carrier of (TOP-REAL n : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous V240() V241() ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) + (t : ( ( ) ( V11() real ext-real ) Element of ( ( ) ( non empty V166() V167() V168() ) set ) ) * b1 : ( ( ) ( Relation-like REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) -valued Function-like V47(n : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V158() ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) -valued Function-like V47(n : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V158() ) Element of the carrier of (TOP-REAL n : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous V240() V241() ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) -valued Function-like V47(n : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V158() ) Element of the carrier of (TOP-REAL n : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous V240() V241() ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) ;
end;

theorem :: TOPALG_2:2
for n being ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) )
for T being ( ( non empty convex ) ( non empty TopSpace-like pathwise_connected convex ) SubSpace of TOP-REAL n : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous V240() V241() ) RLTopStruct ) )
for a, b being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) )
for P, Q being ( ( ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of b2 : ( ( non empty convex ) ( non empty TopSpace-like pathwise_connected convex ) SubSpace of TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous V240() V241() ) RLTopStruct ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total continuous ) Path of a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) holds P : ( ( ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of b2 : ( ( non empty convex ) ( non empty TopSpace-like pathwise_connected convex ) SubSpace of TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous V240() V241() ) RLTopStruct ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total continuous ) Path of b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b4 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) ,Q : ( ( ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of b2 : ( ( non empty convex ) ( non empty TopSpace-like pathwise_connected convex ) SubSpace of TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous V240() V241() ) RLTopStruct ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total continuous ) Path of b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b4 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) are_homotopic ;

registration
let n be ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) ;
let T be ( ( non empty convex ) ( non empty TopSpace-like pathwise_connected convex ) SubSpace of TOP-REAL n : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous V240() V241() ) RLTopStruct ) ) ;
let a, b be ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ;
let P, Q be ( ( ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of T : ( ( non empty convex ) ( non empty TopSpace-like pathwise_connected convex ) SubSpace of TOP-REAL n : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous V240() V241() ) RLTopStruct ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total continuous ) Path of a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) ;
cluster -> continuous for ( ( ) ( ) Homotopy of P : ( ( ) ( ) Element of bool (bool n : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,Q : ( ( ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of n : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) -valued Function-like total quasi_total continuous ) Path of a : ( ( Function-like quasi_total ) ( Relation-like [:n : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) ,n : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( ) set ) -defined n : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) -valued Function-like quasi_total ) Element of bool [:[:n : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) ,n : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( ) set ) ,n : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,b : ( ( Function-like quasi_total ) ( Relation-like [:REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) ,n : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( ) set ) -defined n : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) -valued Function-like quasi_total ) Element of bool [:[:REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) ,n : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( ) set ) ,n : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ) ;
end;

theorem :: TOPALG_2:3
for n being ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) )
for T being ( ( non empty convex ) ( non empty TopSpace-like pathwise_connected convex ) SubSpace of TOP-REAL n : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous V240() V241() ) RLTopStruct ) )
for a being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) )
for C being ( ( ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of b2 : ( ( non empty convex ) ( non empty TopSpace-like pathwise_connected convex ) SubSpace of TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous V240() V241() ) RLTopStruct ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total continuous ) Loop of a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) holds the carrier of (pi_1 (T : ( ( non empty convex ) ( non empty TopSpace-like pathwise_connected convex ) SubSpace of TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous V240() V241() ) RLTopStruct ) ) ,a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) )) : ( ( V134() ) ( non empty V134() V220() V221() V222() V250() V251() V252() V253() V254() V255() ) L10()) : ( ( ) ( non empty ) set ) = {(Class ((EqRel (T : ( ( non empty convex ) ( non empty TopSpace-like pathwise_connected convex ) SubSpace of TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous V240() V241() ) RLTopStruct ) ) ,a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) )) : ( ( ) ( non empty Relation-like Loops b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) -defined Loops b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) -valued total quasi_total V97() V102() ) Element of bool [:(Loops b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) ,(Loops b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,C : ( ( ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of b2 : ( ( non empty convex ) ( non empty TopSpace-like pathwise_connected convex ) SubSpace of TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous V240() V241() ) RLTopStruct ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total continuous ) Loop of b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) )) : ( ( ) ( ) Element of bool (Loops b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) } : ( ( ) ( trivial ) set ) ;

registration
let n be ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) ;
let T be ( ( non empty convex ) ( non empty TopSpace-like pathwise_connected convex ) SubSpace of TOP-REAL n : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous V240() V241() ) RLTopStruct ) ) ;
let a be ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ;
cluster FundamentalGroup (T : ( ( non empty convex ) ( non empty TopSpace-like pathwise_connected convex ) SubSpace of TOP-REAL n : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous V240() V241() ) RLTopStruct ) ) ,a : ( ( ) ( ) Element of the carrier of T : ( ( non empty convex ) ( non empty TopSpace-like pathwise_connected convex ) SubSpace of TOP-REAL n : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous V240() V241() ) RLTopStruct ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( V134() ) ( non empty V134() V220() V221() V222() V250() V251() V252() V253() V254() V255() ) L10()) -> trivial V134() ;
end;

begin

theorem :: TOPALG_2:4
for a being ( ( real ) ( V11() real ext-real ) number ) holds |[a : ( ( real ) ( V11() real ext-real ) number ) ]| : ( ( ) ( Relation-like REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) -valued Function-like V47(1 : ( ( ) ( non empty natural V11() real ext-real positive V36() V37() V166() V167() V168() V169() V170() V171() V257() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V158() ) Element of the carrier of (TOP-REAL 1 : ( ( ) ( non empty natural V11() real ext-real positive V36() V37() V166() V167() V168() V169() V170() V171() V257() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous V240() V241() ) RLTopStruct ) : ( ( ) ( non empty ) set ) ) /. 1 : ( ( ) ( non empty natural V11() real ext-real positive V36() V37() V166() V167() V168() V169() V170() V171() V257() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) ) = a : ( ( real ) ( V11() real ext-real ) number ) ;

theorem :: TOPALG_2:5
for a, b being ( ( real ) ( V11() real ext-real ) number ) st a : ( ( real ) ( V11() real ext-real ) number ) <= b : ( ( real ) ( V11() real ext-real ) number ) holds
[.a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) .] : ( ( ) ( V166() V167() V168() interval ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) = { (((1 : ( ( ) ( non empty natural V11() real ext-real positive V36() V37() V166() V167() V168() V169() V170() V171() V257() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) - l : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) ) * a : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) ) + (l : ( ( ) ( V11() real ext-real ) Real) * b : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) ) where l is ( ( ) ( V11() real ext-real ) Real) : ( 0 : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) <= l : ( ( ) ( V11() real ext-real ) Real) & l : ( ( ) ( V11() real ext-real ) Real) <= 1 : ( ( ) ( non empty natural V11() real ext-real positive V36() V37() V166() V167() V168() V169() V170() V171() V257() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) ) } ;

theorem :: TOPALG_2:6
for F being ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of [:R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ,I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty V166() V167() V168() ) set ) ) st ( for x being ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) )
for i being ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) holds F : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of [:R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ,I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty V166() V167() V168() ) set ) ) . (x : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) ,i : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) ) : ( ( ) ( ) set ) = (1 : ( ( ) ( non empty natural V11() real ext-real positive V36() V37() V166() V167() V168() V169() V170() V171() V257() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) - i : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) ) * x : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) ) ) holds
F : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of [:R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ,I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty V166() V167() V168() ) set ) ) is continuous ;

theorem :: TOPALG_2:7
for F being ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of [:R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ,I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty V166() V167() V168() ) set ) ) st ( for x being ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) )
for i being ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) holds F : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of [:R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ,I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty V166() V167() V168() ) set ) ) . (x : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) ,i : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) ) : ( ( ) ( ) set ) = i : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) * x : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) : ( ( ) ( V11() real ext-real ) set ) ) holds
F : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of [:R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ,I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty V166() V167() V168() ) set ) ) is continuous ;

registration
cluster non empty V166() V167() V168() interval for ( ( ) ( ) Element of bool the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) : ( ( ) ( non empty V166() V167() V168() ) set ) : ( ( ) ( ) set ) ) ;
end;

registration
let T be ( ( real-membered ) ( real-membered ) TopStruct ) ;
cluster V166() V167() V168() interval for ( ( ) ( ) Element of bool the carrier of T : ( ( real-membered ) ( real-membered ) TopStruct ) : ( ( ) ( V166() V167() V168() ) set ) : ( ( ) ( ) set ) ) ;
end;

definition
let T be ( ( real-membered ) ( real-membered ) TopStruct ) ;
attr T is interval means :: TOPALG_2:def 3
 [#] T : ( ( real-membered ) ( real-membered ) TopStruct ) : ( ( ) ( non proper V166() V167() V168() ) Element of bool the carrier of T : ( ( real-membered ) ( real-membered ) TopStruct ) : ( ( ) ( V166() V167() V168() ) set ) : ( ( ) ( ) set ) ) is interval ;
end;

registration
cluster non empty strict TopSpace-like real-membered interval for ( ( ) ( ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) ;
end;

definition
:: original: R^1
redefine func R^1 -> ( ( interval ) ( TopSpace-like real-membered interval ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) ;
end;

theorem :: TOPALG_2:8
for T being ( ( non empty interval ) ( non empty TopSpace-like real-membered interval ) SubSpace of R^1 : ( ( interval ) ( non empty strict TopSpace-like real-membered interval ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) )
for a, b being ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) holds [.a : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) ,b : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) .] : ( ( ) ( V166() V167() V168() interval ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) c= the carrier of T : ( ( non empty interval ) ( non empty TopSpace-like real-membered interval ) SubSpace of R^1 : ( ( interval ) ( non empty strict TopSpace-like real-membered interval ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) ;

registration
cluster non empty interval -> non empty pathwise_connected for ( ( ) ( ) SubSpace of R^1 : ( ( interval ) ( non empty strict TopSpace-like real-membered interval ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) ) ;
end;

theorem :: TOPALG_2:9
for a, b being ( ( real ) ( V11() real ext-real ) number ) st a : ( ( real ) ( V11() real ext-real ) number ) <= b : ( ( real ) ( V11() real ext-real ) number ) holds
Closed-Interval-TSpace (a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( non empty strict ) ( non empty strict TopSpace-like real-membered ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) is interval ;

theorem :: TOPALG_2:10
I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) is interval ;

theorem :: TOPALG_2:11
for a, b being ( ( real ) ( V11() real ext-real ) number ) st a : ( ( real ) ( V11() real ext-real ) number ) <= b : ( ( real ) ( V11() real ext-real ) number ) holds
Closed-Interval-TSpace (a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( non empty strict ) ( non empty strict TopSpace-like real-membered ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) is pathwise_connected ;

definition
let T be ( ( non empty interval ) ( non empty TopSpace-like real-membered pathwise_connected interval ) SubSpace of R^1 : ( ( interval ) ( non empty strict TopSpace-like real-membered pathwise_connected interval ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) ) ;
let P, Q be ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of T : ( ( non empty interval ) ( non empty TopSpace-like real-membered pathwise_connected interval ) SubSpace of R^1 : ( ( interval ) ( non empty strict TopSpace-like real-membered pathwise_connected interval ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty V166() V167() V168() ) set ) , ( ( ) ( non empty V166() V167() V168() ) set ) ) ;
func R1Homotopy (P,Q) -> ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of [:I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) ,I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of T : ( ( real-membered ) ( real-membered ) TopStruct ) : ( ( ) ( V166() V167() V168() ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( V166() V167() V168() ) set ) ) means :: TOPALG_2:def 4
 for s, t being ( ( ) ( V11() real ext-real ) Element of ( ( ) ( non empty V166() V167() V168() ) set ) ) holds it : ( ( Function-like quasi_total ) ( Relation-like [:REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) ,T : ( ( real-membered ) ( real-membered ) TopStruct ) :] : ( ( ) ( ) set ) -defined T : ( ( real-membered ) ( real-membered ) TopStruct ) -valued Function-like quasi_total ) Element of bool [:[:REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) ,T : ( ( real-membered ) ( real-membered ) TopStruct ) :] : ( ( ) ( ) set ) ,T : ( ( real-membered ) ( real-membered ) TopStruct ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) . (s : ( ( ) ( V11() real ext-real ) Element of ( ( ) ( non empty V166() V167() V168() ) set ) ) ,t : ( ( ) ( V11() real ext-real ) Element of ( ( ) ( non empty V166() V167() V168() ) set ) ) ) : ( ( ) ( ) set ) = ((1 : ( ( ) ( non empty natural V11() real ext-real positive V36() V37() V166() V167() V168() V169() V170() V171() V257() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) - t : ( ( ) ( V11() real ext-real ) Element of ( ( ) ( non empty V166() V167() V168() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) ) * (P : ( ( ) ( ) set ) . s : ( ( ) ( V11() real ext-real ) Element of ( ( ) ( non empty V166() V167() V168() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of the carrier of T : ( ( real-membered ) ( real-membered ) TopStruct ) : ( ( ) ( V166() V167() V168() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) ) + (t : ( ( ) ( V11() real ext-real ) Element of ( ( ) ( non empty V166() V167() V168() ) set ) ) * (Q : ( ( ) ( ) Element of the carrier of P : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) . s : ( ( ) ( V11() real ext-real ) Element of ( ( ) ( non empty V166() V167() V168() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of the carrier of T : ( ( real-membered ) ( real-membered ) TopStruct ) : ( ( ) ( V166() V167() V168() ) set ) ) ) : ( ( ) ( V11() real ext-real ) set ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) ) ;
end;

theorem :: TOPALG_2:12
for T being ( ( non empty interval ) ( non empty TopSpace-like real-membered pathwise_connected interval ) SubSpace of R^1 : ( ( interval ) ( non empty strict TopSpace-like real-membered pathwise_connected interval ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) )
for a, b being ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) )
for P, Q being ( ( ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of b1 : ( ( non empty interval ) ( non empty TopSpace-like real-membered pathwise_connected interval ) SubSpace of R^1 : ( ( interval ) ( non empty strict TopSpace-like real-membered pathwise_connected interval ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total quasi_total continuous ) Path of a : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) ,b : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) ) holds P : ( ( ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of b1 : ( ( non empty interval ) ( non empty TopSpace-like real-membered pathwise_connected interval ) SubSpace of R^1 : ( ( interval ) ( non empty strict TopSpace-like real-membered pathwise_connected interval ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total quasi_total continuous ) Path of b2 : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) ,b3 : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) ) ,Q : ( ( ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of b1 : ( ( non empty interval ) ( non empty TopSpace-like real-membered pathwise_connected interval ) SubSpace of R^1 : ( ( interval ) ( non empty strict TopSpace-like real-membered pathwise_connected interval ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total quasi_total continuous ) Path of b2 : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) ,b3 : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) ) are_homotopic ;

registration
let T be ( ( non empty interval ) ( non empty TopSpace-like real-membered pathwise_connected interval ) SubSpace of R^1 : ( ( interval ) ( non empty strict TopSpace-like real-membered pathwise_connected interval ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) ) ;
let a, b be ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) ;
let P, Q be ( ( ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of T : ( ( non empty interval ) ( non empty TopSpace-like real-membered pathwise_connected interval ) SubSpace of R^1 : ( ( interval ) ( non empty strict TopSpace-like real-membered pathwise_connected interval ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total quasi_total continuous ) Path of a : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) ,b : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) ) ;
cluster -> continuous for ( ( ) ( ) Homotopy of P : ( ( Function-like quasi_total ) ( Relation-like [:REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) ,T : ( ( real-membered ) ( real-membered ) TopStruct ) :] : ( ( ) ( ) set ) -defined T : ( ( real-membered ) ( real-membered ) TopStruct ) -valued Function-like quasi_total ) Element of bool [:[:REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) ,T : ( ( real-membered ) ( real-membered ) TopStruct ) :] : ( ( ) ( ) set ) ,T : ( ( real-membered ) ( real-membered ) TopStruct ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,Q : ( ( ) ( ) Element of bool (bool T : ( ( real-membered ) ( real-membered ) TopStruct ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) ;
end;

theorem :: TOPALG_2:13
for T being ( ( non empty interval ) ( non empty TopSpace-like real-membered pathwise_connected interval ) SubSpace of R^1 : ( ( interval ) ( non empty strict TopSpace-like real-membered pathwise_connected interval ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) )
for a being ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) )
for C being ( ( ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of b1 : ( ( non empty interval ) ( non empty TopSpace-like real-membered pathwise_connected interval ) SubSpace of R^1 : ( ( interval ) ( non empty strict TopSpace-like real-membered pathwise_connected interval ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total quasi_total continuous ) Loop of a : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) ) holds the carrier of (pi_1 (T : ( ( non empty interval ) ( non empty TopSpace-like real-membered pathwise_connected interval ) SubSpace of R^1 : ( ( interval ) ( non empty strict TopSpace-like real-membered pathwise_connected interval ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) ) ,a : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) )) : ( ( V134() ) ( non empty V134() V220() V221() V222() V250() V251() V252() V253() V254() V255() ) L10()) : ( ( ) ( non empty ) set ) = {(Class ((EqRel (T : ( ( non empty interval ) ( non empty TopSpace-like real-membered pathwise_connected interval ) SubSpace of R^1 : ( ( interval ) ( non empty strict TopSpace-like real-membered pathwise_connected interval ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) ) ,a : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) )) : ( ( ) ( non empty Relation-like Loops b2 : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) : ( ( ) ( non empty ) set ) -defined Loops b2 : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) : ( ( ) ( non empty ) set ) -valued total quasi_total V97() V102() ) Element of bool [:(Loops b2 : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) ) : ( ( ) ( non empty ) set ) ,(Loops b2 : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,C : ( ( ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of b1 : ( ( non empty interval ) ( non empty TopSpace-like real-membered pathwise_connected interval ) SubSpace of R^1 : ( ( interval ) ( non empty strict TopSpace-like real-membered pathwise_connected interval ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total quasi_total continuous ) Loop of b2 : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) ) )) : ( ( ) ( ) Element of bool (Loops b2 : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) } : ( ( ) ( trivial ) set ) ;

registration
let T be ( ( non empty interval ) ( non empty TopSpace-like real-membered pathwise_connected interval ) SubSpace of R^1 : ( ( interval ) ( non empty strict TopSpace-like real-membered pathwise_connected interval ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) ) ;
let a be ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) ;
cluster FundamentalGroup (T : ( ( non empty interval ) ( non empty TopSpace-like real-membered pathwise_connected interval ) SubSpace of R^1 : ( ( interval ) ( non empty strict TopSpace-like real-membered pathwise_connected interval ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) ) ,a : ( ( ) ( V11() real ext-real ) Element of the carrier of T : ( ( non empty interval ) ( non empty TopSpace-like real-membered pathwise_connected interval ) SubSpace of R^1 : ( ( interval ) ( non empty strict TopSpace-like real-membered pathwise_connected interval ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) ) : ( ( V134() ) ( non empty V134() V220() V221() V222() V250() V251() V252() V253() V254() V255() ) L10()) -> trivial V134() ;
end;

theorem :: TOPALG_2:14
for a, b being ( ( real ) ( V11() real ext-real ) number ) st a : ( ( real ) ( V11() real ext-real ) number ) <= b : ( ( real ) ( V11() real ext-real ) number ) holds
for x, y being ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) )
for P, Q being ( ( ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like real-membered ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total quasi_total ) Path of x : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) ,y : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) ) holds P : ( ( ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like real-membered ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total quasi_total ) Path of b3 : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) ,b4 : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) ) ,Q : ( ( ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like real-membered ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total quasi_total ) Path of b3 : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) ,b4 : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) ) are_homotopic ;

theorem :: TOPALG_2:15
for a, b being ( ( real ) ( V11() real ext-real ) number ) st a : ( ( real ) ( V11() real ext-real ) number ) <= b : ( ( real ) ( V11() real ext-real ) number ) holds
for x being ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) )
for C being ( ( ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like real-membered ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total quasi_total ) Loop of x : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) ) holds the carrier of (pi_1 ((Closed-Interval-TSpace (a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like real-membered ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) ,x : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) )) : ( ( V134() ) ( non empty V134() V220() V221() V222() V250() V251() V252() V253() V254() V255() ) L10()) : ( ( ) ( non empty ) set ) = {(Class ((EqRel ((Closed-Interval-TSpace (a : ( ( real ) ( V11() real ext-real ) number ) ,b : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like real-membered ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) ,x : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) )) : ( ( ) ( non empty Relation-like Loops b3 : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) : ( ( ) ( non empty ) set ) -defined Loops b3 : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) : ( ( ) ( non empty ) set ) -valued total quasi_total V97() V102() ) Element of bool [:(Loops b3 : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) ) : ( ( ) ( non empty ) set ) ,(Loops b3 : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,C : ( ( ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of (Closed-Interval-TSpace (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( non empty strict ) ( non empty strict TopSpace-like real-membered ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total quasi_total ) Loop of b3 : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) ) )) : ( ( ) ( ) Element of bool (Loops b3 : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) } : ( ( ) ( trivial ) set ) ;

theorem :: TOPALG_2:16
for x, y being ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) )
for P, Q being ( ( ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total quasi_total continuous ) Path of x : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) ,y : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) ) holds P : ( ( ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total quasi_total continuous ) Path of b1 : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) ,b2 : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) ) ,Q : ( ( ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total quasi_total continuous ) Path of b1 : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) ,b2 : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) ) are_homotopic ;

theorem :: TOPALG_2:17
for x being ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) )
for C being ( ( ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total quasi_total continuous ) Loop of x : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) ) holds the carrier of (pi_1 (I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) ,x : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) )) : ( ( V134() ) ( non empty V134() V220() V221() V222() V250() V251() V252() V253() V254() V255() ) L10()) : ( ( ) ( non empty ) set ) = {(Class ((EqRel (I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) ,x : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) )) : ( ( ) ( non empty Relation-like Loops b1 : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) : ( ( ) ( non empty ) set ) -defined Loops b1 : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) : ( ( ) ( non empty ) set ) -valued total quasi_total V97() V102() ) Element of bool [:(Loops b1 : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) ) : ( ( ) ( non empty ) set ) ,(Loops b1 : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,C : ( ( ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total quasi_total continuous ) Loop of b1 : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) ) )) : ( ( ) ( ) Element of bool (Loops b1 : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ) } : ( ( ) ( trivial ) set ) ;

registration
let x be ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) ;
cluster FundamentalGroup (I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) ,x : ( ( ) ( V11() real ext-real ) Element of the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) ) ) : ( ( V134() ) ( non empty V134() V220() V221() V222() V250() V251() V252() V253() V254() V255() ) L10()) -> trivial V134() ;
end;

registration
let n be ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) ;
let T be ( ( non empty convex ) ( non empty TopSpace-like pathwise_connected convex ) SubSpace of TOP-REAL n : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous V240() V241() ) RLTopStruct ) ) ;
let P, Q be ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of T : ( ( non empty convex ) ( non empty TopSpace-like pathwise_connected convex ) SubSpace of TOP-REAL n : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous V240() V241() ) RLTopStruct ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total continuous ) Function of ( ( ) ( non empty V166() V167() V168() ) set ) , ( ( ) ( non empty ) set ) ) ;
cluster ConvexHomotopy (P : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of T : ( ( non empty convex ) ( non empty TopSpace-like pathwise_connected convex ) SubSpace of TOP-REAL n : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous V240() V241() ) RLTopStruct ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total continuous ) Element of bool [: the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) , the carrier of T : ( ( non empty convex ) ( non empty TopSpace-like pathwise_connected convex ) SubSpace of TOP-REAL n : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous V240() V241() ) RLTopStruct ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,Q : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of T : ( ( non empty convex ) ( non empty TopSpace-like pathwise_connected convex ) SubSpace of TOP-REAL n : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous V240() V241() ) RLTopStruct ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total continuous ) Element of bool [: the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) , the carrier of T : ( ( non empty convex ) ( non empty TopSpace-like pathwise_connected convex ) SubSpace of TOP-REAL n : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous V240() V241() ) RLTopStruct ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of [:I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) ,I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of T : ( ( non empty convex ) ( non empty TopSpace-like pathwise_connected convex ) SubSpace of TOP-REAL n : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous V240() V241() ) RLTopStruct ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) -> Function-like quasi_total continuous ;
end;

theorem :: TOPALG_2:18
for n being ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) )
for T being ( ( non empty convex ) ( non empty TopSpace-like pathwise_connected convex ) SubSpace of TOP-REAL n : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous V240() V241() ) RLTopStruct ) )
for a, b being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) )
for P, Q being ( ( ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of b2 : ( ( non empty convex ) ( non empty TopSpace-like pathwise_connected convex ) SubSpace of TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous V240() V241() ) RLTopStruct ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total continuous ) Path of a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) holds ConvexHomotopy (P : ( ( ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of b2 : ( ( non empty convex ) ( non empty TopSpace-like pathwise_connected convex ) SubSpace of TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous V240() V241() ) RLTopStruct ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total continuous ) Path of b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b4 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) ,Q : ( ( ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of b2 : ( ( non empty convex ) ( non empty TopSpace-like pathwise_connected convex ) SubSpace of TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous V240() V241() ) RLTopStruct ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total continuous ) Path of b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b4 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of [:I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) ,I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty convex ) ( non empty TopSpace-like pathwise_connected convex ) SubSpace of TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous V240() V241() ) RLTopStruct ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is ( ( ) ( non empty Relation-like the carrier of [:I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) ,I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty convex ) ( non empty TopSpace-like pathwise_connected convex ) SubSpace of TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous V240() V241() ) RLTopStruct ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total continuous ) Homotopy of P : ( ( ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of b2 : ( ( non empty convex ) ( non empty TopSpace-like pathwise_connected convex ) SubSpace of TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous V240() V241() ) RLTopStruct ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total continuous ) Path of b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b4 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) ,Q : ( ( ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of b2 : ( ( non empty convex ) ( non empty TopSpace-like pathwise_connected convex ) SubSpace of TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V36() V37() V166() V167() V168() V169() V170() V171() V259() ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V259() ) Element of bool REAL : ( ( ) ( non empty V40() V166() V167() V168() V172() V259() V260() interval ) set ) : ( ( ) ( ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous V240() V241() ) RLTopStruct ) ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total continuous ) Path of b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b4 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) ) ;

registration
let T be ( ( non empty interval ) ( non empty TopSpace-like real-membered pathwise_connected interval ) SubSpace of R^1 : ( ( interval ) ( non empty strict TopSpace-like real-membered pathwise_connected interval ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) ) ;
let P, Q be ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of T : ( ( non empty interval ) ( non empty TopSpace-like real-membered pathwise_connected interval ) SubSpace of R^1 : ( ( interval ) ( non empty strict TopSpace-like real-membered pathwise_connected interval ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total quasi_total continuous ) Function of ( ( ) ( non empty V166() V167() V168() ) set ) , ( ( ) ( non empty V166() V167() V168() ) set ) ) ;
cluster R1Homotopy (P : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of T : ( ( non empty interval ) ( non empty TopSpace-like real-membered pathwise_connected interval ) SubSpace of R^1 : ( ( interval ) ( non empty strict TopSpace-like real-membered pathwise_connected interval ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total quasi_total continuous ) Element of bool [: the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) , the carrier of T : ( ( non empty interval ) ( non empty TopSpace-like real-membered pathwise_connected interval ) SubSpace of R^1 : ( ( interval ) ( non empty strict TopSpace-like real-membered pathwise_connected interval ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ,Q : ( ( Function-like quasi_total continuous ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of T : ( ( non empty interval ) ( non empty TopSpace-like real-membered pathwise_connected interval ) SubSpace of R^1 : ( ( interval ) ( non empty strict TopSpace-like real-membered pathwise_connected interval ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total quasi_total continuous ) Element of bool [: the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) , the carrier of T : ( ( non empty interval ) ( non empty TopSpace-like real-membered pathwise_connected interval ) SubSpace of R^1 : ( ( interval ) ( non empty strict TopSpace-like real-membered pathwise_connected interval ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of [:I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) ,I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of T : ( ( non empty interval ) ( non empty TopSpace-like real-membered pathwise_connected interval ) SubSpace of R^1 : ( ( interval ) ( non empty strict TopSpace-like real-membered pathwise_connected interval ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty V166() V167() V168() ) set ) ) -> Function-like quasi_total continuous ;
end;

theorem :: TOPALG_2:19
for T being ( ( non empty interval ) ( non empty TopSpace-like real-membered pathwise_connected interval ) SubSpace of R^1 : ( ( interval ) ( non empty strict TopSpace-like real-membered pathwise_connected interval ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) )
for a, b being ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) )
for P, Q being ( ( ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of b1 : ( ( non empty interval ) ( non empty TopSpace-like real-membered pathwise_connected interval ) SubSpace of R^1 : ( ( interval ) ( non empty strict TopSpace-like real-membered pathwise_connected interval ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total quasi_total continuous ) Path of a : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) ,b : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) ) holds R1Homotopy (P : ( ( ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of b1 : ( ( non empty interval ) ( non empty TopSpace-like real-membered pathwise_connected interval ) SubSpace of R^1 : ( ( interval ) ( non empty strict TopSpace-like real-membered pathwise_connected interval ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total quasi_total continuous ) Path of b2 : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) ,b3 : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) ) ,Q : ( ( ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of b1 : ( ( non empty interval ) ( non empty TopSpace-like real-membered pathwise_connected interval ) SubSpace of R^1 : ( ( interval ) ( non empty strict TopSpace-like real-membered pathwise_connected interval ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total quasi_total continuous ) Path of b2 : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) ,b3 : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of [:I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) ,I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty interval ) ( non empty TopSpace-like real-membered pathwise_connected interval ) SubSpace of R^1 : ( ( interval ) ( non empty strict TopSpace-like real-membered pathwise_connected interval ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total quasi_total continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty V166() V167() V168() ) set ) ) is ( ( ) ( non empty Relation-like the carrier of [:I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) ,I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty interval ) ( non empty TopSpace-like real-membered pathwise_connected interval ) SubSpace of R^1 : ( ( interval ) ( non empty strict TopSpace-like real-membered pathwise_connected interval ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total quasi_total continuous ) Homotopy of P : ( ( ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of b1 : ( ( non empty interval ) ( non empty TopSpace-like real-membered pathwise_connected interval ) SubSpace of R^1 : ( ( interval ) ( non empty strict TopSpace-like real-membered pathwise_connected interval ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total quasi_total continuous ) Path of b2 : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) ,b3 : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) ) ,Q : ( ( ) ( non empty Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like real-membered pathwise_connected ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of b1 : ( ( non empty interval ) ( non empty TopSpace-like real-membered pathwise_connected interval ) SubSpace of R^1 : ( ( interval ) ( non empty strict TopSpace-like real-membered pathwise_connected interval ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like real-membered ) TopStruct ) ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -valued Function-like total quasi_total continuous ) Path of b2 : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) ,b3 : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V166() V167() V168() ) set ) ) ) ) ;