RFUNCT

:: RFUNCT_2 semantic presentation

begin

theorem :: RFUNCT_2:2

theorem :: RFUNCT_2:3

theorem :: RFUNCT_2:4

theorem :: RFUNCT_2:5

theorem :: RFUNCT_2:6

theorem :: RFUNCT_2:7

theorem :: RFUNCT_2:8

for W being ( ( non empty ) ( non empty ) set )
for h1, h2 being ( ( Function-like ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,)
for seq being ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) sequence of W : ( ( non empty ) ( non empty ) set ) ) st rng seq : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) sequence of b₁ : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool b₁ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) c= (dom h1 : ( ( Function-like ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( ) Element of bool b₁ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) /\ (dom h2 : ( ( Function-like ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( ) Element of bool b₁ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of bool b₁ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) holds
( (h1 : ( ( Function-like ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) + h2 : ( ( Function-like ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:b₁ : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) /* seq : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) sequence of b₁ : ( ( non empty ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) = (h1 : ( ( Function-like ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) /* seq : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) sequence of b₁ : ( ( non empty ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) + (h2 : ( ( Function-like ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) /* seq : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) sequence of b₁ : ( ( non empty ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) & (h1 : ( ( Function-like ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) - h2 : ( ( Function-like ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:b₁ : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) /* seq : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) sequence of b₁ : ( ( non empty ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) = (h1 : ( ( Function-like ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) /* seq : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) sequence of b₁ : ( ( non empty ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) - (h2 : ( ( Function-like ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) /* seq : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) sequence of b₁ : ( ( non empty ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) & (h1 : ( ( Function-like ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) (#) h2 : ( ( Function-like ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:b₁ : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) /* seq : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) sequence of b₁ : ( ( non empty ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) = (h1 : ( ( Function-like ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) /* seq : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) sequence of b₁ : ( ( non empty ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) (#) (h2 : ( ( Function-like ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) /* seq : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) sequence of b₁ : ( ( non empty ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) ) ;

theorem :: RFUNCT_2:9

theorem :: RFUNCT_2:10

for W being ( ( non empty ) ( non empty ) set )
for h being ( ( Function-like ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,)
for seq being ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) sequence of W : ( ( non empty ) ( non empty ) set ) ) st rng seq : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) sequence of b₁ : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool b₁ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) c= dom h : ( ( Function-like ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( ) Element of bool b₁ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) holds
( abs (h : ( ( Function-like ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) /* seq : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) sequence of b₁ : ( ( non empty ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) = (abs h : ( ( Function-like ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:b₁ : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) /* seq : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) sequence of b₁ : ( ( non empty ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) & - (h : ( ( Function-like ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) /* seq : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) sequence of b₁ : ( ( non empty ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) = (- h : ( ( Function-like ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:b₁ : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) /* seq : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) sequence of b₁ : ( ( non empty ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) ) ;

theorem :: RFUNCT_2:11

theorem :: RFUNCT_2:12

theorem :: RFUNCT_2:13

for W being ( ( non empty ) ( non empty ) set )
for h1, h2 being ( ( Function-like ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,)
for seq being ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) sequence of W : ( ( non empty ) ( non empty ) set ) ) st h1 : ( ( Function-like ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) is total & h2 : ( ( Function-like ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) is total holds
( (h1 : ( ( Function-like ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) + h2 : ( ( Function-like ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:b₁ : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) /* seq : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) sequence of b₁ : ( ( non empty ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) = (h1 : ( ( Function-like ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) /* seq : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) sequence of b₁ : ( ( non empty ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) + (h2 : ( ( Function-like ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) /* seq : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) sequence of b₁ : ( ( non empty ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) & (h1 : ( ( Function-like ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) - h2 : ( ( Function-like ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:b₁ : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) /* seq : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) sequence of b₁ : ( ( non empty ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) = (h1 : ( ( Function-like ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) /* seq : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) sequence of b₁ : ( ( non empty ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) - (h2 : ( ( Function-like ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) /* seq : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) sequence of b₁ : ( ( non empty ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) & (h1 : ( ( Function-like ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) (#) h2 : ( ( Function-like ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:b₁ : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) /* seq : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) sequence of b₁ : ( ( non empty ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) = (h1 : ( ( Function-like ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) /* seq : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) sequence of b₁ : ( ( non empty ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) (#) (h2 : ( ( Function-like ) ( Relation-like b₁ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) /* seq : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined b₁ : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) sequence of b₁ : ( ( non empty ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) ) ;

theorem :: RFUNCT_2:14

for r being ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) )
for W being ( ( non empty ) ( non empty ) set )
for h being ( ( Function-like ) ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,)
for seq being ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined b₂ : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) sequence of W : ( ( non empty ) ( non empty ) set ) ) st h : ( ( Function-like ) ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) is total holds
(r : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) (#) h : ( ( Function-like ) ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:b₂ : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) /* seq : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined b₂ : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) sequence of b₂ : ( ( non empty ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) = r : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) (#) (h : ( ( Function-like ) ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) /* seq : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined b₂ : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) sequence of b₂ : ( ( non empty ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) ;

theorem :: RFUNCT_2:15

for X being ( ( ) ( ) set )
for W being ( ( non empty ) ( non empty ) set )
for h being ( ( Function-like ) ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,)
for seq being ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined b₂ : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) sequence of W : ( ( non empty ) ( non empty ) set ) ) st rng seq : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined b₂ : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) sequence of b₂ : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool b₂ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) c= dom (h : ( ( Function-like ) ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:b₂ : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of bool b₂ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) holds
abs ((h : ( ( Function-like ) ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:b₂ : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) /* seq : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined b₂ : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) sequence of b₂ : ( ( non empty ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) = ((abs h : ( ( Function-like ) ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:b₂ : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) | X : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:b₂ : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) /* seq : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined b₂ : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) sequence of b₂ : ( ( non empty ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) ;

theorem :: RFUNCT_2:16

for X being ( ( ) ( ) set )
for W being ( ( non empty ) ( non empty ) set )
for h being ( ( Function-like ) ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,)
for seq being ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined b₂ : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) sequence of W : ( ( non empty ) ( non empty ) set ) ) st rng seq : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined b₂ : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) sequence of b₂ : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool b₂ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) c= dom (h : ( ( Function-like ) ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:b₂ : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of bool b₂ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) & h : ( ( Function-like ) ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) " {0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V46() V47() V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) ) } : ( ( ) ( trivial V48() V49() V50() V51() V52() V53() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of bool b₂ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) = {} : ( ( ) ( ) set ) holds
((h : ( ( Function-like ) ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ^) : ( ( Function-like ) ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:b₂ : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) | X : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:b₂ : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) /* seq : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined b₂ : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) sequence of b₂ : ( ( non empty ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) = ((h : ( ( Function-like ) ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:b₂ : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) /* seq : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined b₂ : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) sequence of b₂ : ( ( non empty ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) " : ( ( Function-like ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) ;

registration

let Z be ( ( ) ( ) set ) ;
let f be ( ( Relation-like Function-like one-to-one ) ( Relation-like Function-like one-to-one ) Function) ;

cluster f : ( ( Relation-like Function-like one-to-one ) ( Relation-like Function-like one-to-one ) set ) | Z : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like ) set ) -> Relation-like one-to-one ;

end;

theorem :: RFUNCT_2:17

theorem :: RFUNCT_2:18

theorem :: RFUNCT_2:19

for Y being ( ( ) ( ) set )
for W being ( ( non empty ) ( non empty ) set )
for h being ( ( Function-like ) ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st h : ( ( Function-like ) ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) .: Y : ( ( ) ( ) set ) : ( ( ) ( V48() V49() V50() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) is real-bounded & upper_bound (h : ( ( Function-like ) ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) .: Y : ( ( ) ( ) set ) ) : ( ( ) ( V48() V49() V50() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) = lower_bound (h : ( ( Function-like ) ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) .: Y : ( ( ) ( ) set ) ) : ( ( ) ( V48() V49() V50() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) holds
h : ( ( Function-like ) ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | Y : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b₂ : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:b₂ : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is V8() ;

definition

let h be ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ;

redefine attr h is increasing means :: RFUNCT_2:def 1
for r1, r2 being ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) st r1 : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) in dom h : ( ( ) ( ) set ) : ( ( ) ( V48() V49() V50() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) & r2 : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) in dom h : ( ( ) ( ) set ) : ( ( ) ( V48() V49() V50() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) & r1 : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) < r2 : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) holds
h : ( ( ) ( ) set ) . r1 : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) < h : ( ( ) ( ) set ) . r2 : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) ;

redefine attr h is decreasing means :: RFUNCT_2:def 2
for r1, r2 being ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) st r1 : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) in dom h : ( ( ) ( ) set ) : ( ( ) ( V48() V49() V50() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) & r2 : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) in dom h : ( ( ) ( ) set ) : ( ( ) ( V48() V49() V50() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) & r1 : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) < r2 : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) holds
h : ( ( ) ( ) set ) . r2 : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) < h : ( ( ) ( ) set ) . r1 : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) ;

redefine attr h is non-decreasing means :: RFUNCT_2:def 3
for r1, r2 being ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) st r1 : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) in dom h : ( ( ) ( ) set ) : ( ( ) ( V48() V49() V50() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) & r2 : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) in dom h : ( ( ) ( ) set ) : ( ( ) ( V48() V49() V50() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) & r1 : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) < r2 : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) holds
h : ( ( ) ( ) set ) . r1 : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) <= h : ( ( ) ( ) set ) . r2 : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) ;

redefine attr h is non-increasing means :: RFUNCT_2:def 4
for r1, r2 being ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) st r1 : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) in dom h : ( ( ) ( ) set ) : ( ( ) ( V48() V49() V50() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) & r2 : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) in dom h : ( ( ) ( ) set ) : ( ( ) ( V48() V49() V50() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) & r1 : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) < r2 : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) holds
h : ( ( ) ( ) set ) . r2 : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) <= h : ( ( ) ( ) set ) . r1 : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) ;

end;

theorem :: RFUNCT_2:20

for Y being ( ( ) ( ) set )
for h being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) holds
( h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | Y : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is increasing iff for r1, r2 being ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) st r1 : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) in Y : ( ( ) ( ) set ) /\ (dom h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V48() V49() V50() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( V48() V49() V50() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) & r2 : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) in Y : ( ( ) ( ) set ) /\ (dom h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V48() V49() V50() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( V48() V49() V50() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) & r1 : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) < r2 : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) holds
h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . r1 : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) < h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . r2 : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) ) ;

theorem :: RFUNCT_2:21

for Y being ( ( ) ( ) set )
for h being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) holds
( h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | Y : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is decreasing iff for r1, r2 being ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) st r1 : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) in Y : ( ( ) ( ) set ) /\ (dom h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V48() V49() V50() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( V48() V49() V50() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) & r2 : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) in Y : ( ( ) ( ) set ) /\ (dom h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V48() V49() V50() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( V48() V49() V50() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) & r1 : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) < r2 : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) holds
h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . r2 : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) < h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . r1 : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) ) ;

theorem :: RFUNCT_2:22

for Y being ( ( ) ( ) set )
for h being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) holds
( h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | Y : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is non-decreasing iff for r1, r2 being ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) st r1 : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) in Y : ( ( ) ( ) set ) /\ (dom h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V48() V49() V50() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( V48() V49() V50() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) & r2 : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) in Y : ( ( ) ( ) set ) /\ (dom h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V48() V49() V50() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( V48() V49() V50() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) & r1 : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) < r2 : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) holds
h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . r1 : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) <= h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . r2 : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) ) ;

theorem :: RFUNCT_2:23

for Y being ( ( ) ( ) set )
for h being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) holds
( h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | Y : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is non-increasing iff for r1, r2 being ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) st r1 : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) in Y : ( ( ) ( ) set ) /\ (dom h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V48() V49() V50() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( V48() V49() V50() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) & r2 : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) in Y : ( ( ) ( ) set ) /\ (dom h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V48() V49() V50() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( V48() V49() V50() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) & r1 : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) < r2 : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) holds
h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . r2 : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) <= h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . r1 : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) ) ;

definition

attr h is monotone means :: RFUNCT_2:def 5
( h : ( ( ) ( ) set ) is non-decreasing or h : ( ( ) ( ) set ) is non-increasing );

end;

registration

cluster Function-like non-decreasing -> Function-like monotone for ( ( ) ( ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) ;

cluster Function-like non-increasing -> Function-like monotone for ( ( ) ( ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) ;

cluster Function-like non monotone -> Function-like non non-decreasing non non-increasing for ( ( ) ( ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) ;

end;

theorem :: RFUNCT_2:24

for Y being ( ( ) ( ) set )
for h being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) holds
( h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | Y : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is non-decreasing iff for r1, r2 being ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) st r1 : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) in Y : ( ( ) ( ) set ) /\ (dom h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V48() V49() V50() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( V48() V49() V50() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) & r2 : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) in Y : ( ( ) ( ) set ) /\ (dom h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V48() V49() V50() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( V48() V49() V50() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) & r1 : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) <= r2 : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) holds
h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . r1 : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) <= h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . r2 : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) ) ;

theorem :: RFUNCT_2:25

for Y being ( ( ) ( ) set )
for h being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) holds
( h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | Y : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is non-increasing iff for r1, r2 being ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) st r1 : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) in Y : ( ( ) ( ) set ) /\ (dom h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V48() V49() V50() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( V48() V49() V50() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) & r2 : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) in Y : ( ( ) ( ) set ) /\ (dom h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V48() V49() V50() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( V48() V49() V50() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) & r1 : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) <= r2 : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) holds
h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . r2 : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) <= h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . r1 : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) ) ;

registration

cluster Function-like non-decreasing non-increasing -> Function-like V8() for ( ( ) ( ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) ;

end;

registration

cluster Function-like V8() -> Function-like non-decreasing non-increasing for ( ( ) ( ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) ;

end;

registration

cluster Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like trivial complex-valued ext-real-valued real-valued for ( ( ) ( ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) ;

end;

registration

let h be ( ( Function-like increasing ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued increasing non-decreasing monotone ) PartFunc of ,) ;
let X be ( ( ) ( ) set ) ;

cluster h : ( ( Function-like increasing ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued increasing non-decreasing monotone ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) | X : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) -> Function-like increasing for ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ;

end;

registration

let h be ( ( Function-like decreasing ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued decreasing non-increasing monotone ) PartFunc of ,) ;
let X be ( ( ) ( ) set ) ;

cluster h : ( ( Function-like decreasing ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued decreasing non-increasing monotone ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) | X : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) -> Function-like decreasing for ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ;

end;

registration

let h be ( ( Function-like non-decreasing ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued non-decreasing monotone ) PartFunc of ,) ;
let X be ( ( ) ( ) set ) ;

cluster h : ( ( Function-like non-decreasing ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued non-decreasing monotone ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) | X : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) -> Function-like non-decreasing for ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ;

end;

theorem :: RFUNCT_2:26

for Y being ( ( ) ( ) set )
for h being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st Y : ( ( ) ( ) set ) misses dom h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( V48() V49() V50() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) holds
( h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | Y : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is increasing & h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | Y : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is decreasing & h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | Y : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is non-decreasing & h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | Y : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is non-increasing & h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | Y : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is monotone ) ;

theorem :: RFUNCT_2:27

for Y, X being ( ( ) ( ) set )
for h being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | Y : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is non-decreasing & h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is non-increasing holds
h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | (Y : ( ( ) ( ) set ) /\ X : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is V8() ;

theorem :: RFUNCT_2:28

for X, Y being ( ( ) ( ) set )
for h being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st X : ( ( ) ( ) set ) c= Y : ( ( ) ( ) set ) & h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | Y : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is increasing holds
h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is increasing ;

theorem :: RFUNCT_2:29

for X, Y being ( ( ) ( ) set )
for h being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st X : ( ( ) ( ) set ) c= Y : ( ( ) ( ) set ) & h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | Y : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is decreasing holds
h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is decreasing ;

theorem :: RFUNCT_2:30

for X, Y being ( ( ) ( ) set )
for h being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st X : ( ( ) ( ) set ) c= Y : ( ( ) ( ) set ) & h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | Y : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is non-decreasing holds
h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is non-decreasing ;

theorem :: RFUNCT_2:31

for X, Y being ( ( ) ( ) set )
for h being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st X : ( ( ) ( ) set ) c= Y : ( ( ) ( ) set ) & h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | Y : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is non-increasing holds
h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is non-increasing ;

theorem :: RFUNCT_2:32

for Y being ( ( ) ( ) set )
for r being ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) )
for h being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) holds
( ( h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | Y : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is increasing & 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V46() V47() V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) ) < r : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) implies (r : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) (#) h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) | Y : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is increasing ) & ( r : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) = 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V46() V47() V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) ) implies (r : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) (#) h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) | Y : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is V8() ) & ( h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | Y : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is increasing & r : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) < 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V46() V47() V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) ) implies (r : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) (#) h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) | Y : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is decreasing ) ) ;

theorem :: RFUNCT_2:33

for Y being ( ( ) ( ) set )
for r being ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) )
for h being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) holds
( ( h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | Y : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is decreasing & 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V46() V47() V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) ) < r : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) implies (r : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) (#) h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) | Y : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is decreasing ) & ( h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | Y : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is decreasing & r : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) < 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V46() V47() V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) ) implies (r : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) (#) h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) | Y : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is increasing ) ) ;

theorem :: RFUNCT_2:34

for Y being ( ( ) ( ) set )
for r being ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) )
for h being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) holds
( ( h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | Y : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is non-decreasing & 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V46() V47() V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) ) <= r : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) implies (r : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) (#) h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) | Y : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is non-decreasing ) & ( h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | Y : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is non-decreasing & r : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) <= 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V46() V47() V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) ) implies (r : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) (#) h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) | Y : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is non-increasing ) ) ;

theorem :: RFUNCT_2:35

for Y being ( ( ) ( ) set )
for r being ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) )
for h being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) holds
( ( h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | Y : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is non-increasing & 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V46() V47() V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) ) <= r : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) implies (r : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) (#) h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) | Y : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is non-increasing ) & ( h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | Y : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is non-increasing & r : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) <= 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real V46() V47() V48() V49() V50() V51() V52() V53() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V48() V49() V50() V51() V52() V53() V54() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) ) implies (r : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) (#) h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) | Y : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is non-decreasing ) ) ;

theorem :: RFUNCT_2:36

for X, Y being ( ( ) ( ) set )
for r being ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) )
for h1, h2 being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st r : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) in (X : ( ( ) ( ) set ) /\ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) /\ (dom (h1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) + h2 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V48() V49() V50() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( V48() V49() V50() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) holds
( r : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) in X : ( ( ) ( ) set ) /\ (dom h1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V48() V49() V50() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( V48() V49() V50() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) & r : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) in Y : ( ( ) ( ) set ) /\ (dom h2 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( V48() V49() V50() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( V48() V49() V50() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) ) ;

theorem :: RFUNCT_2:37

for X, Y being ( ( ) ( ) set )
for h1, h2 being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) holds
( ( h1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is increasing & h2 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | Y : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is increasing implies (h1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) + h2 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) | (X : ( ( ) ( ) set ) /\ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is increasing ) & ( h1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is decreasing & h2 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | Y : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is decreasing implies (h1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) + h2 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) | (X : ( ( ) ( ) set ) /\ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is decreasing ) & ( h1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is non-decreasing & h2 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | Y : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is non-decreasing implies (h1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) + h2 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) | (X : ( ( ) ( ) set ) /\ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is non-decreasing ) & ( h1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is non-increasing & h2 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | Y : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is non-increasing implies (h1 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) + h2 : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) | (X : ( ( ) ( ) set ) /\ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is non-increasing ) ) ;

theorem :: RFUNCT_2:38

theorem :: RFUNCT_2:39

theorem :: RFUNCT_2:40

theorem :: RFUNCT_2:41

theorem :: RFUNCT_2:42

theorem :: RFUNCT_2:43

for x being ( ( ) ( ) set )
for h being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) holds h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | {x : ( ( ) ( ) set ) } : ( ( ) ( trivial ) set ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is non-increasing ;

theorem :: RFUNCT_2:44

theorem :: RFUNCT_2:45

theorem :: RFUNCT_2:46

theorem :: RFUNCT_2:47

for R being ( ( ) ( V48() V49() V50() ) Subset of ( ( ) ( ) set ) ) holds (id R : ( ( ) ( V48() V49() V50() ) Subset of ( ( ) ( ) set ) ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like one-to-one complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) | R : ( ( ) ( V48() V49() V50() ) Subset of ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like one-to-one complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is increasing ;

theorem :: RFUNCT_2:48

for X being ( ( ) ( ) set )
for h being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is increasing holds
(- h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is decreasing ;

theorem :: RFUNCT_2:49

for X being ( ( ) ( ) set )
for h being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is non-decreasing holds
(- h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is non-increasing ;

theorem :: RFUNCT_2:50

for p, g being ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) )
for h being ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st ( h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | [.p : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) ,g : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) .] : ( ( ) ( V48() V49() V50() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is increasing or h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | [.p : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) ,g : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) .] : ( ( ) ( V48() V49() V50() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is decreasing ) holds
h : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | [.p : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) ,g : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) .] : ( ( ) ( V48() V49() V50() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is one-to-one ;

theorem :: RFUNCT_2:51

for p, g being ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) )
for h being ( ( Function-like one-to-one ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like one-to-one complex-valued ext-real-valued real-valued ) PartFunc of ,) st h : ( ( Function-like one-to-one ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like one-to-one complex-valued ext-real-valued real-valued ) PartFunc of ,) | [.p : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) ,g : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) .] : ( ( ) ( V48() V49() V50() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like one-to-one complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is increasing holds
((h : ( ( Function-like one-to-one ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like one-to-one complex-valued ext-real-valued real-valued ) PartFunc of ,) | [.p : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) ,g : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) .] : ( ( ) ( V48() V49() V50() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like one-to-one complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) ") : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) | (h : ( ( Function-like one-to-one ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like one-to-one complex-valued ext-real-valued real-valued ) PartFunc of ,) .: [.p : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) ,g : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) .] : ( ( ) ( V48() V49() V50() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V48() V49() V50() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is increasing ;

theorem :: RFUNCT_2:52

for p, g being ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) )
for h being ( ( Function-like one-to-one ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like one-to-one complex-valued ext-real-valued real-valued ) PartFunc of ,) st h : ( ( Function-like one-to-one ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like one-to-one complex-valued ext-real-valued real-valued ) PartFunc of ,) | [.p : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) ,g : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) .] : ( ( ) ( V48() V49() V50() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like one-to-one complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is decreasing holds
((h : ( ( Function-like one-to-one ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like one-to-one complex-valued ext-real-valued real-valued ) PartFunc of ,) | [.p : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) ,g : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) .] : ( ( ) ( V48() V49() V50() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like one-to-one complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) ") : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) | (h : ( ( Function-like one-to-one ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like one-to-one complex-valued ext-real-valued real-valued ) PartFunc of ,) .: [.p : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) ,g : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ) .] : ( ( ) ( V48() V49() V50() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V48() V49() V50() ) Element of bool REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -defined REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) -valued Function-like one-to-one complex-valued ext-real-valued real-valued ) Element of bool [:REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) ,REAL : ( ( ) ( non empty V48() V49() V50() V54() V55() ) set ) :] : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( ) set ) ) is decreasing ;