:: PARTFUN4 semantic presentation

begin

registration
let T be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
let f, g be ( ( Function-like V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) continuous ) ( non empty V19() V22( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) V23( REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) Function-like V29( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) V141() V142() V143() continuous ) RealMap of ( ( ) ( non empty ) set ) ) ;
cluster f : ( ( Function-like V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) continuous ) ( non empty V19() V22( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V23( REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) Function-like V29( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) V141() V142() V143() continuous ) Element of K6(K7( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) : ( ( ) ( V19() V141() V142() V143() ) set ) ) : ( ( ) ( ) set ) ) + g : ( ( Function-like V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) continuous ) ( non empty V19() V22( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V23( REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) Function-like V29( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) V141() V142() V143() continuous ) Element of K6(K7( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) : ( ( ) ( V19() V141() V142() V143() ) set ) ) : ( ( ) ( ) set ) ) : ( ( V19() Function-like ) ( V19() Function-like ) set ) -> Function-like V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) continuous for ( ( Function-like V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) ) ( non empty V19() V22( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V23( REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) Function-like V29( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) V141() V142() V143() ) RealMap of ( ( ) ( non empty ) set ) ) ;
cluster f : ( ( Function-like V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) continuous ) ( non empty V19() V22( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V23( REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) Function-like V29( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) V141() V142() V143() continuous ) Element of K6(K7( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) : ( ( ) ( V19() V141() V142() V143() ) set ) ) : ( ( ) ( ) set ) ) - g : ( ( Function-like V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) continuous ) ( non empty V19() V22( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V23( REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) Function-like V29( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) V141() V142() V143() continuous ) Element of K6(K7( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) : ( ( ) ( V19() V141() V142() V143() ) set ) ) : ( ( ) ( ) set ) ) : ( ( V19() Function-like ) ( V19() Function-like ) set ) -> Function-like V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) continuous for ( ( Function-like V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) ) ( non empty V19() V22( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V23( REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) Function-like V29( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) V141() V142() V143() ) RealMap of ( ( ) ( non empty ) set ) ) ;
cluster f : ( ( Function-like V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) continuous ) ( non empty V19() V22( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V23( REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) Function-like V29( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) V141() V142() V143() continuous ) Element of K6(K7( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) : ( ( ) ( V19() V141() V142() V143() ) set ) ) : ( ( ) ( ) set ) ) (#) g : ( ( Function-like V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) continuous ) ( non empty V19() V22( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V23( REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) Function-like V29( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) V141() V142() V143() continuous ) Element of K6(K7( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) : ( ( ) ( V19() V141() V142() V143() ) set ) ) : ( ( ) ( ) set ) ) : ( ( V19() Function-like ) ( V19() Function-like ) set ) -> Function-like V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) continuous for ( ( Function-like V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) ) ( non empty V19() V22( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V23( REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) Function-like V29( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) V141() V142() V143() ) RealMap of ( ( ) ( non empty ) set ) ) ;
end;

registration
let T be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
let f be ( ( Function-like V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) continuous ) ( non empty V19() V22( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) V23( REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) Function-like V29( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) V141() V142() V143() continuous ) RealMap of ( ( ) ( non empty ) set ) ) ;
cluster - f : ( ( Function-like V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) continuous ) ( non empty V19() V22( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V23( REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) Function-like V29( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) V141() V142() V143() continuous ) Element of K6(K7( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) : ( ( ) ( V19() V141() V142() V143() ) set ) ) : ( ( ) ( ) set ) ) : ( ( V19() Function-like V141() ) ( V19() Function-like V141() ) set ) -> Function-like V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) continuous for ( ( Function-like V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) ) ( non empty V19() V22( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V23( REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) Function-like V29( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) V141() V142() V143() ) RealMap of ( ( ) ( non empty ) set ) ) ;
end;

registration
let T be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
let f be ( ( Function-like V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) continuous ) ( non empty V19() V22( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) V23( REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) Function-like V29( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) V141() V142() V143() continuous ) RealMap of ( ( ) ( non empty ) set ) ) ;
cluster |.f : ( ( Function-like V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) continuous ) ( non empty V19() V22( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V23( REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) Function-like V29( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) V141() V142() V143() continuous ) Element of K6(K7( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) : ( ( ) ( V19() V141() V142() V143() ) set ) ) : ( ( ) ( ) set ) ) .| : ( ( V19() Function-like V143() ) ( V19() Function-like V141() V142() V143() nonnegative-yielding ) set ) -> Function-like V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) continuous for ( ( Function-like V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) ) ( non empty V19() V22( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V23( REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) Function-like V29( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) V141() V142() V143() ) RealMap of ( ( ) ( non empty ) set ) ) ;
end;

registration
let T be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
cluster non empty V19() V22( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V23( REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) Function-like V29( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) V141() V142() V143() continuous positive-yielding for ( ( ) ( ) Element of K6(K7( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) : ( ( ) ( V19() V141() V142() V143() ) set ) ) : ( ( ) ( ) set ) ) ;
cluster non empty V19() V22( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V23( REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) Function-like V29( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) V141() V142() V143() continuous negative-yielding for ( ( ) ( ) Element of K6(K7( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) : ( ( ) ( V19() V141() V142() V143() ) set ) ) : ( ( ) ( ) set ) ) ;
end;

registration
let T be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
let f be ( ( Function-like V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) continuous nonnegative-yielding ) ( non empty V19() V22( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) V23( REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) Function-like V29( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) V141() V142() V143() continuous nonnegative-yielding ) RealMap of ( ( ) ( non empty ) set ) ) ;
cluster sqrt f : ( ( Function-like V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) continuous nonnegative-yielding ) ( non empty V19() V22( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V23( REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) Function-like V29( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) V141() V142() V143() continuous nonnegative-yielding ) Element of K6(K7( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) : ( ( ) ( V19() V141() V142() V143() ) set ) ) : ( ( ) ( ) set ) ) : ( ( V19() Function-like ) ( V19() Function-like V141() V142() V143() nonnegative-yielding ) set ) -> Function-like V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) continuous for ( ( Function-like V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) ) ( non empty V19() V22( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V23( REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) Function-like V29( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) V141() V142() V143() ) RealMap of ( ( ) ( non empty ) set ) ) ;
end;

registration
let T be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
let f be ( ( Function-like V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) continuous ) ( non empty V19() V22( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) V23( REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) Function-like V29( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) V141() V142() V143() continuous ) RealMap of ( ( ) ( non empty ) set ) ) ;
let r be ( ( real ) ( V11() real ext-real ) number ) ;
cluster r : ( ( real ) ( V11() real ext-real ) set ) (#) f : ( ( Function-like V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) continuous ) ( non empty V19() V22( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V23( REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) Function-like V29( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) V141() V142() V143() continuous ) Element of K6(K7( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) : ( ( ) ( V19() V141() V142() V143() ) set ) ) : ( ( ) ( ) set ) ) : ( ( V19() Function-like ) ( V19() Function-like ) set ) -> Function-like V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) continuous for ( ( Function-like V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) ) ( non empty V19() V22( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V23( REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) Function-like V29( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) V141() V142() V143() ) RealMap of ( ( ) ( non empty ) set ) ) ;
end;

registration
let T be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
let f be ( ( non-empty Function-like V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) continuous ) ( non empty V19() non-empty V22( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) V23( REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) Function-like V29( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) V141() V142() V143() continuous ) RealMap of ( ( ) ( non empty ) set ) ) ;
cluster K498(f : ( ( non-empty Function-like V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) continuous ) ( non empty V19() non-empty V22( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V23( REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) Function-like V29( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) V141() V142() V143() continuous ) Element of K6(K7( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) : ( ( ) ( V19() V141() V142() V143() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V19() Function-like ) ( V19() non-empty Function-like ) set ) -> Function-like V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) continuous for ( ( Function-like V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) ) ( non empty V19() V22( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V23( REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) Function-like V29( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) V141() V142() V143() ) RealMap of ( ( ) ( non empty ) set ) ) ;
end;

registration
let T be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
let f be ( ( Function-like V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) continuous ) ( non empty V19() V22( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) V23( REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) Function-like V29( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) V141() V142() V143() continuous ) RealMap of ( ( ) ( non empty ) set ) ) ;
let g be ( ( non-empty Function-like V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) continuous ) ( non empty V19() non-empty V22( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) V23( REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) Function-like V29( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) V141() V142() V143() continuous ) RealMap of ( ( ) ( non empty ) set ) ) ;
cluster K495(f : ( ( Function-like V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) continuous ) ( non empty V19() V22( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V23( REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) Function-like V29( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) V141() V142() V143() continuous ) Element of K6(K7( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) : ( ( ) ( V19() V141() V142() V143() ) set ) ) : ( ( ) ( ) set ) ) ,g : ( ( non-empty Function-like V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) continuous ) ( non empty V19() non-empty V22( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V23( REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) Function-like V29( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) V141() V142() V143() continuous ) Element of K6(K7( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) : ( ( ) ( V19() V141() V142() V143() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V19() Function-like ) ( V19() Function-like ) set ) -> Function-like V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) continuous for ( ( Function-like V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) ) ( non empty V19() V22( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V23( REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) Function-like V29( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V33( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty V40() V151() V152() V153() V157() ) set ) ) V141() V142() V143() ) RealMap of ( ( ) ( non empty ) set ) ) ;
end;