:: PARTFUN3 semantic presentation

begin

registration
let r be ( ( real ) ( complex real ext-real ) number ) ;
cluster r : ( ( real ) ( complex real ext-real ) set ) / r : ( ( real ) ( complex real ext-real ) set ) : ( ( ) ( complex real ext-real ) set ) -> non negative ;
end;

registration
let r be ( ( real ) ( complex real ext-real ) number ) ;
cluster r : ( ( real ) ( complex real ext-real ) set ) * r : ( ( real ) ( complex real ext-real ) set ) : ( ( ) ( complex real ext-real ) set ) -> non negative ;
cluster r : ( ( real ) ( complex real ext-real ) set ) * (r : ( ( real ) ( complex real ext-real ) set ) ") : ( ( complex ) ( complex real ext-real ) set ) : ( ( ) ( complex real ext-real ) set ) -> non negative ;
end;

registration
let r be ( ( real non negative ) ( complex real ext-real non negative ) number ) ;
cluster sqrt r : ( ( real non negative ) ( complex real ext-real non negative ) set ) : ( ( real ) ( complex real ext-real ) set ) -> real non negative ;
end;

registration
let r be ( ( real positive ) ( non empty complex real ext-real positive non negative ) number ) ;
cluster sqrt r : ( ( real positive ) ( non empty complex real ext-real positive non negative ) set ) : ( ( real ) ( complex real ext-real non negative ) set ) -> real positive ;
end;

theorem :: PARTFUN3:1
for f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function)
for A being ( ( ) ( ) set ) st f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) is one-to-one & A : ( ( ) ( ) set ) c= dom (f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ") : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( ) set ) holds
f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) .: ((f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ") : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) .: A : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) = A : ( ( ) ( ) set ) ;

registration
let f be ( ( Relation-like non-empty Function-like ) ( Relation-like non-empty Function-like ) Function) ;
cluster f : ( ( Relation-like non-empty Function-like ) ( Relation-like non-empty Function-like ) set ) " {0 : ( ( ) ( empty natural complex real ext-real non positive non negative Function-like functional complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52() V63() V64() ) Element of NAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52() V58() ) Element of K6(REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( ) set ) ) ) } : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) : ( ( ) ( ) set ) -> empty ;
end;

definition
let R be ( ( Relation-like ) ( Relation-like ) Relation) ;
attr R is positive-yielding means :: PARTFUN3:def 1
 for r being ( ( real ) ( complex real ext-real ) number ) st r : ( ( real ) ( complex real ext-real ) number ) in rng R : ( ( ) ( ) set ) : ( ( ) ( ) set ) holds
0 : ( ( ) ( empty natural complex real ext-real non positive non negative Function-like functional complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52() V63() V64() ) Element of NAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52() V58() ) Element of K6(REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( ) set ) ) ) < r : ( ( real ) ( complex real ext-real ) number ) ;
attr R is negative-yielding means :: PARTFUN3:def 2
 for r being ( ( real ) ( complex real ext-real ) number ) st r : ( ( real ) ( complex real ext-real ) number ) in rng R : ( ( ) ( ) set ) : ( ( ) ( ) set ) holds
0 : ( ( ) ( empty natural complex real ext-real non positive non negative Function-like functional complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52() V63() V64() ) Element of NAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52() V58() ) Element of K6(REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( ) set ) ) ) > r : ( ( real ) ( complex real ext-real ) number ) ;
attr R is nonpositive-yielding means :: PARTFUN3:def 3
 for r being ( ( real ) ( complex real ext-real ) number ) st r : ( ( real ) ( complex real ext-real ) number ) in rng R : ( ( ) ( ) set ) : ( ( ) ( ) set ) holds
0 : ( ( ) ( empty natural complex real ext-real non positive non negative Function-like functional complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52() V63() V64() ) Element of NAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52() V58() ) Element of K6(REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( ) set ) ) ) >= r : ( ( real ) ( complex real ext-real ) number ) ;
attr R is nonnegative-yielding means :: PARTFUN3:def 4
 for r being ( ( real ) ( complex real ext-real ) number ) st r : ( ( real ) ( complex real ext-real ) number ) in rng R : ( ( ) ( ) set ) : ( ( ) ( ) set ) holds
0 : ( ( ) ( empty natural complex real ext-real non positive non negative Function-like functional complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52() V63() V64() ) Element of NAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52() V58() ) Element of K6(REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( ) set ) ) ) <= r : ( ( real ) ( complex real ext-real ) number ) ;
end;

registration
let X be ( ( ) ( ) set ) ;
let r be ( ( real positive ) ( non empty complex real ext-real positive non negative ) number ) ;
cluster X : ( ( ) ( ) set ) --> r : ( ( real positive ) ( non empty complex real ext-real positive non negative ) set ) : ( ( ) ( Relation-like non-empty X : ( ( ) ( ) set ) -defined Function-like constant total complex-valued ext-real-valued real-valued ) set ) -> positive-yielding ;
end;

registration
let X be ( ( ) ( ) set ) ;
let r be ( ( real negative ) ( non empty complex real ext-real non positive negative ) number ) ;
cluster X : ( ( ) ( ) set ) --> r : ( ( real negative ) ( non empty complex real ext-real non positive negative ) set ) : ( ( ) ( Relation-like non-empty X : ( ( ) ( ) set ) -defined Function-like constant total complex-valued ext-real-valued real-valued ) set ) -> negative-yielding ;
end;

registration
let X be ( ( ) ( ) set ) ;
let r be ( ( real non positive ) ( complex real ext-real non positive ) number ) ;
cluster X : ( ( ) ( ) set ) --> r : ( ( real non positive ) ( complex real ext-real non positive ) set ) : ( ( ) ( Relation-like X : ( ( ) ( ) set ) -defined Function-like constant total complex-valued ext-real-valued real-valued ) set ) -> nonpositive-yielding ;
end;

registration
let X be ( ( ) ( ) set ) ;
let r be ( ( real non negative ) ( complex real ext-real non negative ) number ) ;
cluster X : ( ( ) ( ) set ) --> r : ( ( real non negative ) ( complex real ext-real non negative ) set ) : ( ( ) ( Relation-like X : ( ( ) ( ) set ) -defined Function-like constant total complex-valued ext-real-valued real-valued ) set ) -> nonnegative-yielding ;
end;

registration
let X be ( ( non empty ) ( non empty ) set ) ;
cluster X : ( ( non empty ) ( non empty ) set ) --> 0 : ( ( ) ( empty natural complex real ext-real non positive non negative Function-like functional complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52() V63() V64() ) Element of NAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52() V58() ) Element of K6(REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty Relation-like X : ( ( non empty ) ( non empty ) set ) -defined RAT : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered V52() V53() ) set ) -valued INT : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered integer-membered V52() V53() ) set ) -valued Function-like constant total complex-valued ext-real-valued real-valued natural-valued nonpositive-yielding nonnegative-yielding ) set ) -> non non-empty ;
end;

registration
cluster Relation-like positive-yielding -> Relation-like non-empty nonnegative-yielding for ( ( ) ( ) set ) ;
cluster Relation-like negative-yielding -> Relation-like non-empty nonpositive-yielding for ( ( ) ( ) set ) ;
end;

registration
let X be ( ( ) ( ) set ) ;
cluster Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like total V33(X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) complex-valued ext-real-valued real-valued negative-yielding for ( ( ) ( ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) ;
cluster Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like total V33(X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) complex-valued ext-real-valued real-valued positive-yielding for ( ( ) ( ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) ;
end;

registration
cluster Relation-like non-empty Function-like real-valued for ( ( ) ( ) set ) ;
end;

theorem :: PARTFUN3:2
for f being ( ( Relation-like non-empty Function-like real-valued ) ( Relation-like non-empty Function-like complex-valued ext-real-valued real-valued ) Function) holds dom (f : ( ( Relation-like non-empty Function-like real-valued ) ( Relation-like non-empty Function-like complex-valued ext-real-valued real-valued ) Function) ^) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( ) set ) = dom f : ( ( Relation-like non-empty Function-like real-valued ) ( Relation-like non-empty Function-like complex-valued ext-real-valued real-valued ) Function) : ( ( ) ( ) set ) ;

theorem :: PARTFUN3:3
for X being ( ( non empty ) ( non empty ) set )
for f being ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,)
for g being ( ( non-empty Function-like ) ( Relation-like non-empty b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) holds dom (f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) / g : ( ( non-empty Function-like ) ( Relation-like non-empty b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K6(K7(b1 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of K6(b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) = (dom f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( ) Element of K6(b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) /\ (dom g : ( ( non-empty Function-like ) ( Relation-like non-empty b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( ) Element of K6(b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of K6(b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ;

registration
let X be ( ( ) ( ) set ) ;
let f, g be ( ( Function-like nonpositive-yielding ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued nonpositive-yielding ) PartFunc of ,) ;
cluster f : ( ( Function-like nonpositive-yielding ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued nonpositive-yielding ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) + g : ( ( Function-like nonpositive-yielding ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued nonpositive-yielding ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like X : ( ( ) ( ) set ) -defined Function-like complex-valued ext-real-valued real-valued ) set ) -> Relation-like Function-like nonpositive-yielding ;
end;

registration
let X be ( ( ) ( ) set ) ;
let f, g be ( ( Function-like nonnegative-yielding ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued nonnegative-yielding ) PartFunc of ,) ;
cluster f : ( ( Function-like nonnegative-yielding ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued nonnegative-yielding ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) + g : ( ( Function-like nonnegative-yielding ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued nonnegative-yielding ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like X : ( ( ) ( ) set ) -defined Function-like complex-valued ext-real-valued real-valued ) set ) -> Relation-like Function-like nonnegative-yielding ;
end;

registration
let X be ( ( ) ( ) set ) ;
let f be ( ( Function-like positive-yielding ) ( Relation-like non-empty X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued positive-yielding nonnegative-yielding ) PartFunc of ,) ;
let g be ( ( Function-like nonnegative-yielding ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued nonnegative-yielding ) PartFunc of ,) ;
cluster f : ( ( Function-like positive-yielding ) ( Relation-like non-empty X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued positive-yielding nonnegative-yielding ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) + g : ( ( Function-like nonnegative-yielding ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued nonnegative-yielding ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like X : ( ( ) ( ) set ) -defined Function-like complex-valued ext-real-valued real-valued nonnegative-yielding ) set ) -> Relation-like Function-like positive-yielding ;
end;

registration
let X be ( ( ) ( ) set ) ;
let f be ( ( Function-like nonnegative-yielding ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued nonnegative-yielding ) PartFunc of ,) ;
let g be ( ( Function-like positive-yielding ) ( Relation-like non-empty X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued positive-yielding nonnegative-yielding ) PartFunc of ,) ;
cluster f : ( ( Function-like nonnegative-yielding ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued nonnegative-yielding ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) + g : ( ( Function-like positive-yielding ) ( Relation-like non-empty X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued positive-yielding nonnegative-yielding ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like non-empty X : ( ( ) ( ) set ) -defined Function-like complex-valued ext-real-valued real-valued positive-yielding nonnegative-yielding ) set ) -> Relation-like Function-like positive-yielding ;
end;

registration
let X be ( ( ) ( ) set ) ;
let f be ( ( Function-like nonpositive-yielding ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued nonpositive-yielding ) PartFunc of ,) ;
let g be ( ( Function-like negative-yielding ) ( Relation-like non-empty X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued negative-yielding nonpositive-yielding ) PartFunc of ,) ;
cluster f : ( ( Function-like nonpositive-yielding ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued nonpositive-yielding ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) + g : ( ( Function-like negative-yielding ) ( Relation-like non-empty X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued negative-yielding nonpositive-yielding ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like X : ( ( ) ( ) set ) -defined Function-like complex-valued ext-real-valued real-valued nonpositive-yielding ) set ) -> Relation-like Function-like negative-yielding ;
end;

registration
let X be ( ( ) ( ) set ) ;
let f be ( ( Function-like negative-yielding ) ( Relation-like non-empty X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued negative-yielding nonpositive-yielding ) PartFunc of ,) ;
let g be ( ( Function-like nonpositive-yielding ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued nonpositive-yielding ) PartFunc of ,) ;
cluster f : ( ( Function-like negative-yielding ) ( Relation-like non-empty X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued negative-yielding nonpositive-yielding ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) + g : ( ( Function-like nonpositive-yielding ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued nonpositive-yielding ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like non-empty X : ( ( ) ( ) set ) -defined Function-like complex-valued ext-real-valued real-valued negative-yielding nonpositive-yielding ) set ) -> Relation-like Function-like negative-yielding ;
end;

registration
let X be ( ( ) ( ) set ) ;
let f be ( ( Function-like nonnegative-yielding ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued nonnegative-yielding ) PartFunc of ,) ;
let g be ( ( Function-like nonpositive-yielding ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued nonpositive-yielding ) PartFunc of ,) ;
cluster f : ( ( Function-like nonnegative-yielding ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued nonnegative-yielding ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) - g : ( ( Function-like nonpositive-yielding ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued nonpositive-yielding ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like X : ( ( ) ( ) set ) -defined Function-like complex-valued ext-real-valued real-valued ) set ) -> Relation-like Function-like nonnegative-yielding ;
end;

registration
let X be ( ( ) ( ) set ) ;
let f be ( ( Function-like nonpositive-yielding ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued nonpositive-yielding ) PartFunc of ,) ;
let g be ( ( Function-like nonnegative-yielding ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued nonnegative-yielding ) PartFunc of ,) ;
cluster f : ( ( Function-like nonpositive-yielding ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued nonpositive-yielding ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) - g : ( ( Function-like nonnegative-yielding ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued nonnegative-yielding ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like X : ( ( ) ( ) set ) -defined Function-like complex-valued ext-real-valued real-valued ) set ) -> Relation-like Function-like nonpositive-yielding ;
end;

registration
let X be ( ( ) ( ) set ) ;
let f be ( ( Function-like positive-yielding ) ( Relation-like non-empty X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued positive-yielding nonnegative-yielding ) PartFunc of ,) ;
let g be ( ( Function-like nonpositive-yielding ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued nonpositive-yielding ) PartFunc of ,) ;
cluster f : ( ( Function-like positive-yielding ) ( Relation-like non-empty X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued positive-yielding nonnegative-yielding ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) - g : ( ( Function-like nonpositive-yielding ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued nonpositive-yielding ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like X : ( ( ) ( ) set ) -defined Function-like complex-valued ext-real-valued real-valued nonnegative-yielding ) set ) -> Relation-like Function-like positive-yielding ;
end;

registration
let X be ( ( ) ( ) set ) ;
let f be ( ( Function-like nonpositive-yielding ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued nonpositive-yielding ) PartFunc of ,) ;
let g be ( ( Function-like positive-yielding ) ( Relation-like non-empty X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued positive-yielding nonnegative-yielding ) PartFunc of ,) ;
cluster f : ( ( Function-like nonpositive-yielding ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued nonpositive-yielding ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) - g : ( ( Function-like positive-yielding ) ( Relation-like non-empty X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued positive-yielding nonnegative-yielding ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like X : ( ( ) ( ) set ) -defined Function-like complex-valued ext-real-valued real-valued nonpositive-yielding ) set ) -> Relation-like Function-like negative-yielding ;
end;

registration
let X be ( ( ) ( ) set ) ;
let f be ( ( Function-like negative-yielding ) ( Relation-like non-empty X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued negative-yielding nonpositive-yielding ) PartFunc of ,) ;
let g be ( ( Function-like nonnegative-yielding ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued nonnegative-yielding ) PartFunc of ,) ;
cluster f : ( ( Function-like negative-yielding ) ( Relation-like non-empty X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued negative-yielding nonpositive-yielding ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) - g : ( ( Function-like nonnegative-yielding ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued nonnegative-yielding ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like X : ( ( ) ( ) set ) -defined Function-like complex-valued ext-real-valued real-valued nonpositive-yielding ) set ) -> Relation-like Function-like negative-yielding ;
end;

registration
let X be ( ( ) ( ) set ) ;
let f be ( ( Function-like nonnegative-yielding ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued nonnegative-yielding ) PartFunc of ,) ;
let g be ( ( Function-like negative-yielding ) ( Relation-like non-empty X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued negative-yielding nonpositive-yielding ) PartFunc of ,) ;
cluster f : ( ( Function-like nonnegative-yielding ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued nonnegative-yielding ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) - g : ( ( Function-like negative-yielding ) ( Relation-like non-empty X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued negative-yielding nonpositive-yielding ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like X : ( ( ) ( ) set ) -defined Function-like complex-valued ext-real-valued real-valued nonnegative-yielding ) set ) -> Relation-like Function-like positive-yielding ;
end;

registration
let X be ( ( ) ( ) set ) ;
let f, g be ( ( Function-like nonpositive-yielding ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued nonpositive-yielding ) PartFunc of ,) ;
cluster f : ( ( Function-like nonpositive-yielding ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued nonpositive-yielding ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) (#) g : ( ( Function-like nonpositive-yielding ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued nonpositive-yielding ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like X : ( ( ) ( ) set ) -defined Function-like complex-valued ext-real-valued real-valued ) set ) -> Relation-like Function-like nonnegative-yielding ;
end;

registration
let X be ( ( ) ( ) set ) ;
let f, g be ( ( Function-like nonnegative-yielding ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued nonnegative-yielding ) PartFunc of ,) ;
cluster f : ( ( Function-like nonnegative-yielding ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued nonnegative-yielding ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) (#) g : ( ( Function-like nonnegative-yielding ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued nonnegative-yielding ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like X : ( ( ) ( ) set ) -defined Function-like complex-valued ext-real-valued real-valued ) set ) -> Relation-like Function-like nonnegative-yielding ;
end;

registration
let X be ( ( ) ( ) set ) ;
let f be ( ( Function-like nonpositive-yielding ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued nonpositive-yielding ) PartFunc of ,) ;
let g be ( ( Function-like nonnegative-yielding ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued nonnegative-yielding ) PartFunc of ,) ;
cluster f : ( ( Function-like nonpositive-yielding ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued nonpositive-yielding ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) (#) g : ( ( Function-like nonnegative-yielding ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued nonnegative-yielding ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like X : ( ( ) ( ) set ) -defined Function-like complex-valued ext-real-valued real-valued ) set ) -> Relation-like Function-like nonpositive-yielding ;
end;

registration
let X be ( ( ) ( ) set ) ;
let f be ( ( Function-like nonnegative-yielding ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued nonnegative-yielding ) PartFunc of ,) ;
let g be ( ( Function-like nonpositive-yielding ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued nonpositive-yielding ) PartFunc of ,) ;
cluster f : ( ( Function-like nonnegative-yielding ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued nonnegative-yielding ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) (#) g : ( ( Function-like nonpositive-yielding ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued nonpositive-yielding ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like X : ( ( ) ( ) set ) -defined Function-like complex-valued ext-real-valued real-valued nonpositive-yielding ) set ) -> Relation-like Function-like nonpositive-yielding ;
end;

registration
let X be ( ( ) ( ) set ) ;
let f be ( ( Function-like positive-yielding ) ( Relation-like non-empty X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued positive-yielding nonnegative-yielding ) PartFunc of ,) ;
let g be ( ( Function-like negative-yielding ) ( Relation-like non-empty X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued negative-yielding nonpositive-yielding ) PartFunc of ,) ;
cluster f : ( ( Function-like positive-yielding ) ( Relation-like non-empty X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued positive-yielding nonnegative-yielding ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) (#) g : ( ( Function-like negative-yielding ) ( Relation-like non-empty X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued negative-yielding nonpositive-yielding ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like X : ( ( ) ( ) set ) -defined Function-like complex-valued ext-real-valued real-valued nonpositive-yielding ) set ) -> Relation-like Function-like negative-yielding ;
end;

registration
let X be ( ( ) ( ) set ) ;
let f be ( ( Function-like negative-yielding ) ( Relation-like non-empty X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued negative-yielding nonpositive-yielding ) PartFunc of ,) ;
let g be ( ( Function-like positive-yielding ) ( Relation-like non-empty X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued positive-yielding nonnegative-yielding ) PartFunc of ,) ;
cluster f : ( ( Function-like negative-yielding ) ( Relation-like non-empty X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued negative-yielding nonpositive-yielding ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) (#) g : ( ( Function-like positive-yielding ) ( Relation-like non-empty X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued positive-yielding nonnegative-yielding ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like non-empty X : ( ( ) ( ) set ) -defined Function-like complex-valued ext-real-valued real-valued negative-yielding nonpositive-yielding ) set ) -> Relation-like Function-like negative-yielding ;
end;

registration
let X be ( ( ) ( ) set ) ;
let f, g be ( ( Function-like positive-yielding ) ( Relation-like non-empty X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued positive-yielding nonnegative-yielding ) PartFunc of ,) ;
cluster f : ( ( Function-like positive-yielding ) ( Relation-like non-empty X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued positive-yielding nonnegative-yielding ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) (#) g : ( ( Function-like positive-yielding ) ( Relation-like non-empty X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued positive-yielding nonnegative-yielding ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like X : ( ( ) ( ) set ) -defined Function-like complex-valued ext-real-valued real-valued nonnegative-yielding ) set ) -> Relation-like Function-like positive-yielding ;
end;

registration
let X be ( ( ) ( ) set ) ;
let f, g be ( ( Function-like negative-yielding ) ( Relation-like non-empty X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued negative-yielding nonpositive-yielding ) PartFunc of ,) ;
cluster f : ( ( Function-like negative-yielding ) ( Relation-like non-empty X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued negative-yielding nonpositive-yielding ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) (#) g : ( ( Function-like negative-yielding ) ( Relation-like non-empty X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued negative-yielding nonpositive-yielding ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like X : ( ( ) ( ) set ) -defined Function-like complex-valued ext-real-valued real-valued nonnegative-yielding ) set ) -> Relation-like Function-like positive-yielding ;
end;

registration
let X be ( ( ) ( ) set ) ;
let f, g be ( ( non-empty Function-like ) ( Relation-like non-empty X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ;
cluster f : ( ( non-empty Function-like ) ( Relation-like non-empty X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) (#) g : ( ( non-empty Function-like ) ( Relation-like non-empty X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like X : ( ( ) ( ) set ) -defined Function-like complex-valued ext-real-valued real-valued ) set ) -> Relation-like non-empty Function-like ;
end;

registration
let X be ( ( ) ( ) set ) ;
let f be ( ( Function-like ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ;
cluster f : ( ( Function-like ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) (#) f : ( ( Function-like ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like X : ( ( ) ( ) set ) -defined Function-like complex-valued ext-real-valued real-valued ) set ) -> Relation-like Function-like nonnegative-yielding ;
end;

registration
let X be ( ( ) ( ) set ) ;
let r be ( ( real non positive ) ( complex real ext-real non positive ) number ) ;
let f be ( ( Function-like nonpositive-yielding ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued nonpositive-yielding ) PartFunc of ,) ;
cluster r : ( ( real non positive ) ( complex real ext-real non positive ) set ) (#) f : ( ( Function-like nonpositive-yielding ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued nonpositive-yielding ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like X : ( ( ) ( ) set ) -defined Function-like complex-valued ext-real-valued real-valued ) set ) -> Relation-like Function-like nonnegative-yielding ;
end;

registration
let X be ( ( ) ( ) set ) ;
let r be ( ( real non negative ) ( complex real ext-real non negative ) number ) ;
let f be ( ( Function-like nonnegative-yielding ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued nonnegative-yielding ) PartFunc of ,) ;
cluster r : ( ( real non negative ) ( complex real ext-real non negative ) set ) (#) f : ( ( Function-like nonnegative-yielding ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued nonnegative-yielding ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like X : ( ( ) ( ) set ) -defined Function-like complex-valued ext-real-valued real-valued ) set ) -> Relation-like Function-like nonnegative-yielding ;
end;

registration
let X be ( ( ) ( ) set ) ;
let r be ( ( real non positive ) ( complex real ext-real non positive ) number ) ;
let f be ( ( Function-like nonnegative-yielding ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued nonnegative-yielding ) PartFunc of ,) ;
cluster r : ( ( real non positive ) ( complex real ext-real non positive ) set ) (#) f : ( ( Function-like nonnegative-yielding ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued nonnegative-yielding ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like X : ( ( ) ( ) set ) -defined Function-like complex-valued ext-real-valued real-valued ) set ) -> Relation-like Function-like nonpositive-yielding ;
end;

registration
let X be ( ( ) ( ) set ) ;
let r be ( ( real non negative ) ( complex real ext-real non negative ) number ) ;
let f be ( ( Function-like nonpositive-yielding ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued nonpositive-yielding ) PartFunc of ,) ;
cluster r : ( ( real non negative ) ( complex real ext-real non negative ) set ) (#) f : ( ( Function-like nonpositive-yielding ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued nonpositive-yielding ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like X : ( ( ) ( ) set ) -defined Function-like complex-valued ext-real-valued real-valued ) set ) -> Relation-like Function-like nonpositive-yielding ;
end;

registration
let X be ( ( ) ( ) set ) ;
let r be ( ( real positive ) ( non empty complex real ext-real positive non negative ) number ) ;
let f be ( ( Function-like negative-yielding ) ( Relation-like non-empty X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued negative-yielding nonpositive-yielding ) PartFunc of ,) ;
cluster r : ( ( real positive ) ( non empty complex real ext-real positive non negative ) set ) (#) f : ( ( Function-like negative-yielding ) ( Relation-like non-empty X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued negative-yielding nonpositive-yielding ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like X : ( ( ) ( ) set ) -defined Function-like complex-valued ext-real-valued real-valued nonpositive-yielding ) set ) -> Relation-like Function-like negative-yielding ;
end;

registration
let X be ( ( ) ( ) set ) ;
let r be ( ( real negative ) ( non empty complex real ext-real non positive negative ) number ) ;
let f be ( ( Function-like positive-yielding ) ( Relation-like non-empty X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued positive-yielding nonnegative-yielding ) PartFunc of ,) ;
cluster r : ( ( real negative ) ( non empty complex real ext-real non positive negative ) set ) (#) f : ( ( Function-like positive-yielding ) ( Relation-like non-empty X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued positive-yielding nonnegative-yielding ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like X : ( ( ) ( ) set ) -defined Function-like complex-valued ext-real-valued real-valued nonpositive-yielding ) set ) -> Relation-like Function-like negative-yielding ;
end;

registration
let X be ( ( ) ( ) set ) ;
let r be ( ( real positive ) ( non empty complex real ext-real positive non negative ) number ) ;
let f be ( ( Function-like positive-yielding ) ( Relation-like non-empty X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued positive-yielding nonnegative-yielding ) PartFunc of ,) ;
cluster r : ( ( real positive ) ( non empty complex real ext-real positive non negative ) set ) (#) f : ( ( Function-like positive-yielding ) ( Relation-like non-empty X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued positive-yielding nonnegative-yielding ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like X : ( ( ) ( ) set ) -defined Function-like complex-valued ext-real-valued real-valued nonnegative-yielding ) set ) -> Relation-like Function-like positive-yielding ;
end;

registration
let X be ( ( ) ( ) set ) ;
let r be ( ( real negative ) ( non empty complex real ext-real non positive negative ) number ) ;
let f be ( ( Function-like negative-yielding ) ( Relation-like non-empty X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued negative-yielding nonpositive-yielding ) PartFunc of ,) ;
cluster r : ( ( real negative ) ( non empty complex real ext-real non positive negative ) set ) (#) f : ( ( Function-like negative-yielding ) ( Relation-like non-empty X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued negative-yielding nonpositive-yielding ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like X : ( ( ) ( ) set ) -defined Function-like complex-valued ext-real-valued real-valued nonnegative-yielding ) set ) -> Relation-like Function-like positive-yielding ;
end;

registration
let X be ( ( ) ( ) set ) ;
let r be ( ( non zero real ) ( non zero complex real ext-real ) number ) ;
let f be ( ( non-empty Function-like ) ( Relation-like non-empty X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ;
cluster r : ( ( non zero real ) ( non zero complex real ext-real ) set ) (#) f : ( ( non-empty Function-like ) ( Relation-like non-empty X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like X : ( ( ) ( ) set ) -defined Function-like complex-valued ext-real-valued real-valued ) set ) -> Relation-like non-empty Function-like ;
end;

registration
let X be ( ( non empty ) ( non empty ) set ) ;
let f, g be ( ( Function-like nonpositive-yielding ) ( Relation-like X : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued nonpositive-yielding ) PartFunc of ,) ;
cluster f : ( ( Function-like nonpositive-yielding ) ( Relation-like X : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued nonpositive-yielding ) Element of K6(K7(X : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) / g : ( ( Function-like nonpositive-yielding ) ( Relation-like X : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued nonpositive-yielding ) Element of K6(K7(X : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) -> Relation-like Function-like nonnegative-yielding ;
end;

registration
let X be ( ( non empty ) ( non empty ) set ) ;
let f, g be ( ( Function-like nonnegative-yielding ) ( Relation-like X : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued nonnegative-yielding ) PartFunc of ,) ;
cluster f : ( ( Function-like nonnegative-yielding ) ( Relation-like X : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued nonnegative-yielding ) Element of K6(K7(X : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) / g : ( ( Function-like nonnegative-yielding ) ( Relation-like X : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued nonnegative-yielding ) Element of K6(K7(X : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) -> Relation-like Function-like nonnegative-yielding ;
end;

registration
let X be ( ( non empty ) ( non empty ) set ) ;
let f be ( ( Function-like nonpositive-yielding ) ( Relation-like X : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued nonpositive-yielding ) PartFunc of ,) ;
let g be ( ( Function-like nonnegative-yielding ) ( Relation-like X : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued nonnegative-yielding ) PartFunc of ,) ;
cluster f : ( ( Function-like nonpositive-yielding ) ( Relation-like X : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued nonpositive-yielding ) Element of K6(K7(X : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) / g : ( ( Function-like nonnegative-yielding ) ( Relation-like X : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued nonnegative-yielding ) Element of K6(K7(X : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) -> Relation-like Function-like nonpositive-yielding ;
end;

registration
let X be ( ( non empty ) ( non empty ) set ) ;
let f be ( ( Function-like nonnegative-yielding ) ( Relation-like X : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued nonnegative-yielding ) PartFunc of ,) ;
let g be ( ( Function-like nonpositive-yielding ) ( Relation-like X : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued nonpositive-yielding ) PartFunc of ,) ;
cluster f : ( ( Function-like nonnegative-yielding ) ( Relation-like X : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued nonnegative-yielding ) Element of K6(K7(X : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) / g : ( ( Function-like nonpositive-yielding ) ( Relation-like X : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued nonpositive-yielding ) Element of K6(K7(X : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) -> Relation-like Function-like nonpositive-yielding ;
end;

registration
let X be ( ( non empty ) ( non empty ) set ) ;
let f be ( ( Function-like positive-yielding ) ( Relation-like non-empty X : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued positive-yielding nonnegative-yielding ) PartFunc of ,) ;
let g be ( ( Function-like negative-yielding ) ( Relation-like non-empty X : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued negative-yielding nonpositive-yielding ) PartFunc of ,) ;
cluster f : ( ( Function-like positive-yielding ) ( Relation-like non-empty X : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued positive-yielding nonnegative-yielding ) Element of K6(K7(X : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) / g : ( ( Function-like negative-yielding ) ( Relation-like non-empty X : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued negative-yielding nonpositive-yielding ) Element of K6(K7(X : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like nonpositive-yielding ) set ) -> Relation-like Function-like negative-yielding ;
end;

registration
let X be ( ( non empty ) ( non empty ) set ) ;
let f be ( ( Function-like negative-yielding ) ( Relation-like non-empty X : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued negative-yielding nonpositive-yielding ) PartFunc of ,) ;
let g be ( ( Function-like positive-yielding ) ( Relation-like non-empty X : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued positive-yielding nonnegative-yielding ) PartFunc of ,) ;
cluster f : ( ( Function-like negative-yielding ) ( Relation-like non-empty X : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued negative-yielding nonpositive-yielding ) Element of K6(K7(X : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) / g : ( ( Function-like positive-yielding ) ( Relation-like non-empty X : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued positive-yielding nonnegative-yielding ) Element of K6(K7(X : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like nonpositive-yielding ) set ) -> Relation-like Function-like negative-yielding ;
end;

registration
let X be ( ( non empty ) ( non empty ) set ) ;
let f, g be ( ( Function-like positive-yielding ) ( Relation-like non-empty X : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued positive-yielding nonnegative-yielding ) PartFunc of ,) ;
cluster f : ( ( Function-like positive-yielding ) ( Relation-like non-empty X : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued positive-yielding nonnegative-yielding ) Element of K6(K7(X : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) / g : ( ( Function-like positive-yielding ) ( Relation-like non-empty X : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued positive-yielding nonnegative-yielding ) Element of K6(K7(X : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like nonnegative-yielding ) set ) -> Relation-like Function-like positive-yielding ;
end;

registration
let X be ( ( non empty ) ( non empty ) set ) ;
let f, g be ( ( Function-like negative-yielding ) ( Relation-like non-empty X : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued negative-yielding nonpositive-yielding ) PartFunc of ,) ;
cluster f : ( ( Function-like negative-yielding ) ( Relation-like non-empty X : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued negative-yielding nonpositive-yielding ) Element of K6(K7(X : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) / g : ( ( Function-like negative-yielding ) ( Relation-like non-empty X : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued negative-yielding nonpositive-yielding ) Element of K6(K7(X : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like nonnegative-yielding ) set ) -> Relation-like Function-like positive-yielding ;
end;

registration
let X be ( ( non empty ) ( non empty ) set ) ;
let f be ( ( Function-like ) ( Relation-like X : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ;
cluster f : ( ( Function-like ) ( Relation-like X : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K6(K7(X : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) / f : ( ( Function-like ) ( Relation-like X : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K6(K7(X : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) -> Relation-like Function-like nonnegative-yielding ;
end;

registration
let X be ( ( non empty ) ( non empty ) set ) ;
let f, g be ( ( non-empty Function-like ) ( Relation-like non-empty X : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ;
cluster f : ( ( non-empty Function-like ) ( Relation-like non-empty X : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K6(K7(X : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) / g : ( ( non-empty Function-like ) ( Relation-like non-empty X : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K6(K7(X : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) -> Relation-like non-empty Function-like ;
end;

registration
let X be ( ( ) ( ) set ) ;
let f be ( ( Function-like V33(X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) nonpositive-yielding ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like total V33(X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) complex-valued ext-real-valued real-valued nonpositive-yielding ) Function of X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) ;
cluster Inv f : ( ( Function-like V33(X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) nonpositive-yielding ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like total V33(X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) complex-valued ext-real-valued real-valued nonpositive-yielding ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like complex-valued ) ( Relation-like X : ( ( ) ( ) set ) -defined Function-like total complex-valued ext-real-valued real-valued ) set ) -> Relation-like Function-like complex-valued nonpositive-yielding ;
end;

registration
let X be ( ( ) ( ) set ) ;
let f be ( ( Function-like V33(X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) nonnegative-yielding ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like total V33(X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) complex-valued ext-real-valued real-valued nonnegative-yielding ) Function of X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) ;
cluster Inv f : ( ( Function-like V33(X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) nonnegative-yielding ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like total V33(X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) complex-valued ext-real-valued real-valued nonnegative-yielding ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like complex-valued ) ( Relation-like X : ( ( ) ( ) set ) -defined Function-like total complex-valued ext-real-valued real-valued ) set ) -> Relation-like Function-like complex-valued nonnegative-yielding ;
end;

registration
let X be ( ( ) ( ) set ) ;
let f be ( ( Function-like V33(X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) positive-yielding ) ( Relation-like non-empty X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like total V33(X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) complex-valued ext-real-valued real-valued positive-yielding nonnegative-yielding ) Function of X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) ;
cluster Inv f : ( ( Function-like V33(X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) positive-yielding ) ( Relation-like non-empty X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like total V33(X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) complex-valued ext-real-valued real-valued positive-yielding nonnegative-yielding ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like complex-valued ) ( Relation-like X : ( ( ) ( ) set ) -defined Function-like total complex-valued ext-real-valued real-valued nonnegative-yielding ) set ) -> Relation-like Function-like complex-valued positive-yielding ;
end;

registration
let X be ( ( ) ( ) set ) ;
let f be ( ( Function-like V33(X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) negative-yielding ) ( Relation-like non-empty X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like total V33(X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) complex-valued ext-real-valued real-valued negative-yielding nonpositive-yielding ) Function of X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) ;
cluster Inv f : ( ( Function-like V33(X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) negative-yielding ) ( Relation-like non-empty X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like total V33(X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) complex-valued ext-real-valued real-valued negative-yielding nonpositive-yielding ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like complex-valued ) ( Relation-like X : ( ( ) ( ) set ) -defined Function-like total complex-valued ext-real-valued real-valued nonpositive-yielding ) set ) -> Relation-like Function-like complex-valued negative-yielding ;
end;

registration
let X be ( ( ) ( ) set ) ;
let f be ( ( non-empty Function-like V33(X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) ) ( Relation-like non-empty X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like total V33(X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Function of X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) ;
cluster Inv f : ( ( non-empty Function-like V33(X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) ) ( Relation-like non-empty X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like total V33(X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like complex-valued ) ( Relation-like X : ( ( ) ( ) set ) -defined Function-like total complex-valued ext-real-valued real-valued ) set ) -> Relation-like non-empty Function-like complex-valued ;
end;

registration
let X be ( ( ) ( ) set ) ;
let f be ( ( non-empty Function-like V33(X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) ) ( Relation-like non-empty X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like total V33(X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Function of X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) ;
cluster - f : ( ( non-empty Function-like V33(X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) ) ( Relation-like non-empty X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like total V33(X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like complex-valued ) ( Relation-like X : ( ( ) ( ) set ) -defined Function-like total complex-valued ext-real-valued real-valued ) set ) -> Relation-like non-empty Function-like complex-valued ;
end;

registration
let X be ( ( ) ( ) set ) ;
let f be ( ( Function-like V33(X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) nonpositive-yielding ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like total V33(X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) complex-valued ext-real-valued real-valued nonpositive-yielding ) Function of X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) ;
cluster - f : ( ( Function-like V33(X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) nonpositive-yielding ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like total V33(X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) complex-valued ext-real-valued real-valued nonpositive-yielding ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like complex-valued ) ( Relation-like X : ( ( ) ( ) set ) -defined Function-like total complex-valued ext-real-valued real-valued ) set ) -> Relation-like Function-like complex-valued nonnegative-yielding ;
end;

registration
let X be ( ( ) ( ) set ) ;
let f be ( ( Function-like V33(X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) nonnegative-yielding ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like total V33(X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) complex-valued ext-real-valued real-valued nonnegative-yielding ) Function of X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) ;
cluster - f : ( ( Function-like V33(X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) nonnegative-yielding ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like total V33(X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) complex-valued ext-real-valued real-valued nonnegative-yielding ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like complex-valued ) ( Relation-like X : ( ( ) ( ) set ) -defined Function-like total complex-valued ext-real-valued real-valued ) set ) -> Relation-like Function-like complex-valued nonpositive-yielding ;
end;

registration
let X be ( ( ) ( ) set ) ;
let f be ( ( Function-like V33(X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) positive-yielding ) ( Relation-like non-empty X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like total V33(X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) complex-valued ext-real-valued real-valued positive-yielding nonnegative-yielding ) Function of X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) ;
cluster - f : ( ( Function-like V33(X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) positive-yielding ) ( Relation-like non-empty X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like total V33(X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) complex-valued ext-real-valued real-valued positive-yielding nonnegative-yielding ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like complex-valued ) ( Relation-like non-empty X : ( ( ) ( ) set ) -defined Function-like total complex-valued ext-real-valued real-valued nonpositive-yielding ) set ) -> Relation-like Function-like complex-valued negative-yielding ;
end;

registration
let X be ( ( ) ( ) set ) ;
let f be ( ( Function-like V33(X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) negative-yielding ) ( Relation-like non-empty X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like total V33(X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) complex-valued ext-real-valued real-valued negative-yielding nonpositive-yielding ) Function of X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) ;
cluster - f : ( ( Function-like V33(X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) negative-yielding ) ( Relation-like non-empty X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like total V33(X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) complex-valued ext-real-valued real-valued negative-yielding nonpositive-yielding ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like complex-valued ) ( Relation-like non-empty X : ( ( ) ( ) set ) -defined Function-like total complex-valued ext-real-valued real-valued nonnegative-yielding ) set ) -> Relation-like Function-like complex-valued positive-yielding ;
end;

registration
let X be ( ( ) ( ) set ) ;
let f be ( ( Function-like V33(X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like total V33(X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Function of X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) ;
cluster |.f : ( ( Function-like V33(X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like total V33(X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) .| : ( ( Relation-like Function-like real-valued ) ( Relation-like X : ( ( ) ( ) set ) -defined Function-like total complex-valued ext-real-valued real-valued ) set ) -> Relation-like Function-like real-valued nonnegative-yielding ;
end;

registration
let X be ( ( ) ( ) set ) ;
let f be ( ( non-empty Function-like V33(X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) ) ( Relation-like non-empty X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like total V33(X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Function of X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) ;
cluster |.f : ( ( non-empty Function-like V33(X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) ) ( Relation-like non-empty X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like total V33(X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) .| : ( ( Relation-like Function-like real-valued ) ( Relation-like X : ( ( ) ( ) set ) -defined Function-like total complex-valued ext-real-valued real-valued nonnegative-yielding ) set ) -> Relation-like Function-like real-valued positive-yielding ;
end;

registration
let X be ( ( non empty ) ( non empty ) set ) ;
let f be ( ( Function-like V33(X : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) nonpositive-yielding ) ( non empty Relation-like X : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like total V33(X : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) complex-valued ext-real-valued real-valued nonpositive-yielding ) Function of X : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) ;
cluster f : ( ( Function-like V33(X : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) nonpositive-yielding ) ( non empty Relation-like X : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like total V33(X : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) complex-valued ext-real-valued real-valued nonpositive-yielding ) Element of K6(K7(X : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) ^ : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) -> Relation-like Function-like nonpositive-yielding ;
end;

registration
let X be ( ( non empty ) ( non empty ) set ) ;
let f be ( ( Function-like V33(X : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) nonnegative-yielding ) ( non empty Relation-like X : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like total V33(X : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) complex-valued ext-real-valued real-valued nonnegative-yielding ) Function of X : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) ;
cluster f : ( ( Function-like V33(X : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) nonnegative-yielding ) ( non empty Relation-like X : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like total V33(X : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) complex-valued ext-real-valued real-valued nonnegative-yielding ) Element of K6(K7(X : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) ^ : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) -> Relation-like Function-like nonnegative-yielding ;
end;

registration
let X be ( ( non empty ) ( non empty ) set ) ;
let f be ( ( Function-like V33(X : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) positive-yielding ) ( non empty Relation-like non-empty X : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like total V33(X : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) complex-valued ext-real-valued real-valued positive-yielding nonnegative-yielding ) Function of X : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) ;
cluster f : ( ( Function-like V33(X : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) positive-yielding ) ( non empty Relation-like non-empty X : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like total V33(X : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) complex-valued ext-real-valued real-valued positive-yielding nonnegative-yielding ) Element of K6(K7(X : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) ^ : ( ( Relation-like Function-like ) ( Relation-like Function-like nonnegative-yielding ) set ) -> Relation-like Function-like positive-yielding ;
end;

registration
let X be ( ( non empty ) ( non empty ) set ) ;
let f be ( ( Function-like V33(X : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) negative-yielding ) ( non empty Relation-like non-empty X : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like total V33(X : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) complex-valued ext-real-valued real-valued negative-yielding nonpositive-yielding ) Function of X : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) ;
cluster f : ( ( Function-like V33(X : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) negative-yielding ) ( non empty Relation-like non-empty X : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like total V33(X : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) complex-valued ext-real-valued real-valued negative-yielding nonpositive-yielding ) Element of K6(K7(X : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) ^ : ( ( Relation-like Function-like ) ( Relation-like Function-like nonpositive-yielding ) set ) -> Relation-like Function-like negative-yielding ;
end;

registration
let X be ( ( non empty ) ( non empty ) set ) ;
let f be ( ( non-empty Function-like V33(X : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) ) ( non empty Relation-like non-empty X : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like total V33(X : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Function of X : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) ;
cluster f : ( ( non-empty Function-like V33(X : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) ) ( non empty Relation-like non-empty X : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like total V33(X : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Element of K6(K7(X : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) ^ : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) -> Relation-like non-empty Function-like ;
end;

definition
let f be ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) ;
func sqrt f -> ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) means :: PARTFUN3:def 5
( dom it : ( ( ) ( ) set ) : ( ( ) ( ) set ) = dom f : ( ( ) ( ) set ) : ( ( ) ( ) set ) & ( for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in dom it : ( ( ) ( ) set ) : ( ( ) ( ) set ) holds
it : ( ( ) ( ) set ) . x : ( ( ) ( ) set ) : ( ( ) ( ) set ) = sqrt (f : ( ( ) ( ) set ) . x : ( ( ) ( ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex real ext-real ) Element of REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) ) );
end;

registration
let f be ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) ;
cluster sqrt f : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) -> Relation-like Function-like real-valued ;
end;

definition
let C be ( ( ) ( ) set ) ;
let D be ( ( real-membered ) ( complex-membered ext-real-membered real-membered ) set ) ;
let f be ( ( Function-like ) ( Relation-like C : ( ( ) ( ) set ) -defined D : ( ( real-membered ) ( complex-membered ext-real-membered real-membered ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ;
:: original: sqrt
redefine func sqrt f -> ( ( Function-like ) ( Relation-like C : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ;
end;

registration
let X be ( ( ) ( ) set ) ;
let f be ( ( Function-like V33(X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) nonnegative-yielding ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like total V33(X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) complex-valued ext-real-valued real-valued nonnegative-yielding ) Function of X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) ;
cluster sqrt f : ( ( Function-like V33(X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) nonnegative-yielding ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like total V33(X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) complex-valued ext-real-valued real-valued nonnegative-yielding ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) -> Relation-like Function-like nonnegative-yielding ;
end;

registration
let X be ( ( ) ( ) set ) ;
let f be ( ( Function-like V33(X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) positive-yielding ) ( Relation-like non-empty X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like total V33(X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) complex-valued ext-real-valued real-valued positive-yielding nonnegative-yielding ) Function of X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) ;
cluster sqrt f : ( ( Function-like V33(X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) positive-yielding ) ( Relation-like non-empty X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like total V33(X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) complex-valued ext-real-valued real-valued positive-yielding nonnegative-yielding ) Element of K6(K7(X : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued nonnegative-yielding ) Function) -> Relation-like Function-like positive-yielding ;
end;

definition
let X be ( ( ) ( ) set ) ;
let f be ( ( Function-like V33(X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like total V33(X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Function of X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) ;
:: original: sqrt
redefine func sqrt f -> ( ( Function-like V33(X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like total V33(X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Function of X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) ;
end;

definition
let X be ( ( ) ( ) set ) ;
let f be ( ( non-empty Function-like V33(X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) ) ( Relation-like non-empty X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like total V33(X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Function of X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) ;
:: original: ^
redefine func f ^ -> ( ( Function-like V33(X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) ) ( Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like total V33(X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Function of X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) ;
end;

definition
let X be ( ( non empty ) ( non empty ) set ) ;
let f be ( ( Function-like V33(X : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) ) ( non empty Relation-like X : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like total V33(X : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Function of X : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) ;
let g be ( ( non-empty Function-like V33(X : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) ) ( non empty Relation-like non-empty X : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like total V33(X : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Function of X : ( ( non empty ) ( non empty ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) ;
:: original: /
redefine func f / g -> ( ( Function-like V33(X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) ) ( non empty Relation-like X : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) -valued Function-like total V33(X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) complex-valued ext-real-valued real-valued ) Function of X : ( ( ) ( ) set ) , REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V53() V58() ) set ) ) ;
end;