:: RFUNCT_1 semantic presentation

begin

definition
let f1, f2 be ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ;
func f1 / f2 -> ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) means :: RFUNCT_1:def 1
( dom it : ( ( Function-like ) ( Relation-like f1 : ( ( ) ( ext-real complex real ) Element of REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) -defined f2 : ( ( real ) ( ext-real complex real ) set ) -valued RAT : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(f1 : ( ( ) ( ext-real complex real ) Element of REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) ,f2 : ( ( real ) ( ext-real complex real ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) = (dom f1 : ( ( ) ( ext-real complex real ) Element of REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) ) : ( ( ) ( ) set ) /\ ((dom f2 : ( ( real ) ( ext-real complex real ) set ) ) : ( ( ) ( ) set ) \ (f2 : ( ( real ) ( ext-real complex real ) set ) " {0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered V51() V52() ) set ) -valued Function-like one-to-one constant functional empty ext-real non positive non negative natural complex real V33() V34() complex-valued ext-real-valued real-valued natural-valued complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() ) Element of NAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() ) Element of K19(REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) } : ( ( ) ( functional non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of K19((dom f2 : ( ( real ) ( ext-real complex real ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of K19((dom f2 : ( ( real ) ( ext-real complex real ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) & ( for c being ( ( ) ( ) set ) st c : ( ( ) ( ) set ) in dom it : ( ( Function-like ) ( Relation-like f1 : ( ( ) ( ext-real complex real ) Element of REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) -defined f2 : ( ( real ) ( ext-real complex real ) set ) -valued RAT : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(f1 : ( ( ) ( ext-real complex real ) Element of REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) ,f2 : ( ( real ) ( ext-real complex real ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) holds
it : ( ( Function-like ) ( Relation-like f1 : ( ( ) ( ext-real complex real ) Element of REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) -defined f2 : ( ( real ) ( ext-real complex real ) set ) -valued RAT : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(f1 : ( ( ) ( ext-real complex real ) Element of REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) ,f2 : ( ( real ) ( ext-real complex real ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( ) set ) ) . c : ( ( ) ( ) set ) : ( ( ) ( ext-real complex real V34() ) set ) = (f1 : ( ( ) ( ext-real complex real ) Element of REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) . c : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) * ((f2 : ( ( real ) ( ext-real complex real ) set ) . c : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ") : ( ( complex ) ( complex ) set ) : ( ( ) ( ) set ) ) );
end;

registration
let f1, f2 be ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ;
cluster f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) set ) / f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) set ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) -> Relation-like Function-like complex-valued ;
end;

registration
let f1, f2 be ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) ;
cluster f1 : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) / f2 : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) Function) -> Relation-like Function-like real-valued ;
end;

definition
let C be ( ( ) ( ) set ) ;
let D be ( ( complex-membered ) ( complex-membered ) set ) ;
let f1, f2 be ( ( Function-like ) ( Relation-like C : ( ( ) ( ) set ) -defined D : ( ( complex-membered ) ( complex-membered ) set ) -valued Function-like complex-valued ) PartFunc of ,) ;
:: original: /
redefine func f1 / f2 -> ( ( Function-like ) ( Relation-like C : ( ( ) ( ) set ) -defined COMPLEX : ( ( ) ( non empty complex-membered V51() V52() ) set ) -valued Function-like complex-valued ) PartFunc of ,) ;
end;

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

definition
let f be ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ;
func f ^ -> ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) means :: RFUNCT_1:def 2
( dom it : ( ( ) ( ) set ) : ( ( ) ( ) set ) = (dom f : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) \ (f : ( ( ) ( ) set ) " {0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered V51() V52() ) set ) -valued Function-like one-to-one constant functional empty ext-real non positive non negative natural complex real V33() V34() complex-valued ext-real-valued real-valued natural-valued complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() ) Element of NAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() ) Element of K19(REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) } : ( ( ) ( functional non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) Element of K19((dom f : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) & ( for c being ( ( ) ( ) set ) st c : ( ( ) ( ) set ) in dom it : ( ( ) ( ) set ) : ( ( ) ( ) set ) holds
it : ( ( ) ( ) set ) . c : ( ( ) ( ) set ) : ( ( ) ( ) set ) = (f : ( ( ) ( ) set ) . c : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) " : ( ( complex ) ( complex ) set ) ) );
end;

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

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

definition
let C be ( ( ) ( ) set ) ;
let D be ( ( complex-membered ) ( complex-membered ) set ) ;
let f be ( ( Function-like ) ( Relation-like C : ( ( ) ( ) set ) -defined D : ( ( complex-membered ) ( complex-membered ) set ) -valued Function-like complex-valued ) PartFunc of ,) ;
:: original: ^
redefine func f ^ -> ( ( Function-like ) ( Relation-like C : ( ( ) ( ) set ) -defined COMPLEX : ( ( ) ( non empty complex-membered V51() V52() ) set ) -valued Function-like complex-valued ) PartFunc of ,) ;
end;

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

theorem :: RFUNCT_1:1
for g being ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) holds
( dom (g : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ^) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) Function) : ( ( ) ( ) set ) c= dom g : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) : ( ( ) ( ) set ) & (dom g : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( ) ( ) set ) /\ ((dom g : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( ) ( ) set ) \ (g : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) " {0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered V51() V52() ) set ) -valued Function-like one-to-one constant functional empty ext-real non positive non negative natural complex real V33() V34() complex-valued ext-real-valued real-valued natural-valued complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() ) Element of NAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() ) Element of K19(REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) } : ( ( ) ( functional non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of K19((dom b1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of K19((dom b1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = (dom g : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( ) ( ) set ) \ (g : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) " {0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered V51() V52() ) set ) -valued Function-like one-to-one constant functional empty ext-real non positive non negative natural complex real V33() V34() complex-valued ext-real-valued real-valued natural-valued complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() ) Element of NAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() ) Element of K19(REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) } : ( ( ) ( functional non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) Element of K19((dom b1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: RFUNCT_1:2
for f1, f2 being ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) holds (dom (f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) (#) f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) ) : ( ( ) ( ) set ) \ ((f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) (#) f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) " {0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered V51() V52() ) set ) -valued Function-like one-to-one constant functional empty ext-real non positive non negative natural complex real V33() V34() complex-valued ext-real-valued real-valued natural-valued complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() ) Element of NAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() ) Element of K19(REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) } : ( ( ) ( functional non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) Element of K19((dom (b1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) (#) b2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = ((dom f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( ) ( ) set ) \ (f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) " {0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered V51() V52() ) set ) -valued Function-like one-to-one constant functional empty ext-real non positive non negative natural complex real V33() V34() complex-valued ext-real-valued real-valued natural-valued complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() ) Element of NAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() ) Element of K19(REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) } : ( ( ) ( functional non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of K19((dom b1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) /\ ((dom f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( ) ( ) set ) \ (f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) " {0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered V51() V52() ) set ) -valued Function-like one-to-one constant functional empty ext-real non positive non negative natural complex real V33() V34() complex-valued ext-real-valued real-valued natural-valued complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() ) Element of NAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() ) Element of K19(REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) } : ( ( ) ( functional non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of K19((dom b2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of K19((dom b2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: RFUNCT_1:3
for C being ( ( non empty ) ( non empty ) set )
for c being ( ( ) ( ) Element of C : ( ( non empty ) ( non empty ) set ) )
for f being ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) st c : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) in dom (f : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ^) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) Function) : ( ( ) ( ) set ) holds
f : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) . c : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( complex ) set ) <> 0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered V51() V52() ) set ) -valued Function-like one-to-one constant functional empty ext-real non positive non negative natural complex real V33() V34() complex-valued ext-real-valued real-valued natural-valued complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() ) Element of NAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() ) Element of K19(REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: RFUNCT_1:4
for f being ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) holds (f : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ^) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) Function) " {0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered V51() V52() ) set ) -valued Function-like one-to-one constant functional empty ext-real non positive non negative natural complex real V33() V34() complex-valued ext-real-valued real-valued natural-valued complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() ) Element of NAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() ) Element of K19(REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) } : ( ( ) ( functional non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) : ( ( ) ( ) set ) = {} : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered V51() V52() ) set ) -valued Function-like one-to-one constant functional empty complex-valued ext-real-valued real-valued natural-valued complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() ) set ) ;

theorem :: RFUNCT_1:5
for f being ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) holds
( (abs f : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) " {0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered V51() V52() ) set ) -valued Function-like one-to-one constant functional empty ext-real non positive non negative natural complex real V33() V34() complex-valued ext-real-valued real-valued natural-valued complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() ) Element of NAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() ) Element of K19(REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) } : ( ( ) ( functional non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) : ( ( ) ( ) set ) = f : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) " {0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered V51() V52() ) set ) -valued Function-like one-to-one constant functional empty ext-real non positive non negative natural complex real V33() V34() complex-valued ext-real-valued real-valued natural-valued complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() ) Element of NAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() ) Element of K19(REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) } : ( ( ) ( functional non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) : ( ( ) ( ) set ) & (- f : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) set ) " {0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered V51() V52() ) set ) -valued Function-like one-to-one constant functional empty ext-real non positive non negative natural complex real V33() V34() complex-valued ext-real-valued real-valued natural-valued complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() ) Element of NAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() ) Element of K19(REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) } : ( ( ) ( functional non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) : ( ( ) ( ) set ) = f : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) " {0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered V51() V52() ) set ) -valued Function-like one-to-one constant functional empty ext-real non positive non negative natural complex real V33() V34() complex-valued ext-real-valued real-valued natural-valued complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() ) Element of NAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() ) Element of K19(REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) } : ( ( ) ( functional non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) : ( ( ) ( ) set ) ) ;

theorem :: RFUNCT_1:6
for f being ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) holds dom ((f : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ^) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) Function) ^) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) Function) : ( ( ) ( ) set ) = dom (f : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) | (dom (f : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ^) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ) set ) : ( ( ) ( ) set ) ;

theorem :: RFUNCT_1:7
for f being ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function)
for r being ( ( complex ) ( complex ) number ) st r : ( ( complex ) ( complex ) number ) <> 0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered V51() V52() ) set ) -valued Function-like one-to-one constant functional empty ext-real non positive non negative natural complex real V33() V34() complex-valued ext-real-valued real-valued natural-valued complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() ) Element of NAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() ) Element of K19(REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) holds
(r : ( ( complex ) ( complex ) number ) (#) f : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) " {0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered V51() V52() ) set ) -valued Function-like one-to-one constant functional empty ext-real non positive non negative natural complex real V33() V34() complex-valued ext-real-valued real-valued natural-valued complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() ) Element of NAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() ) Element of K19(REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) } : ( ( ) ( functional non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) : ( ( ) ( ) set ) = f : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) " {0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered V51() V52() ) set ) -valued Function-like one-to-one constant functional empty ext-real non positive non negative natural complex real V33() V34() complex-valued ext-real-valued real-valued natural-valued complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() ) Element of NAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() ) Element of K19(REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) } : ( ( ) ( functional non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) : ( ( ) ( ) set ) ;

theorem :: RFUNCT_1:8
for f1, f2, f3 being ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) holds (f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) + f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) + f3 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) = f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) + (f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) + f3 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) ;

theorem :: RFUNCT_1:9
for f1, f2, f3 being ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) holds (f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) (#) f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) (#) f3 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) = f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) (#) (f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) (#) f3 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) ;

theorem :: RFUNCT_1:10
for f1, f2, f3 being ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) holds (f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) + f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) (#) f3 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) = (f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) (#) f3 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) + (f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) (#) f3 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) ;

theorem :: RFUNCT_1:11
for f3, f1, f2 being ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) holds f3 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) (#) (f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) + f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) = (f3 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) (#) f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) + (f3 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) (#) f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) ;

theorem :: RFUNCT_1:12
for f1, f2 being ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function)
for r being ( ( complex ) ( complex ) number ) holds r : ( ( complex ) ( complex ) number ) (#) (f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) (#) f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) = (r : ( ( complex ) ( complex ) number ) (#) f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) (#) f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) ;

theorem :: RFUNCT_1:13
for f1, f2 being ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function)
for r being ( ( complex ) ( complex ) number ) holds r : ( ( complex ) ( complex ) number ) (#) (f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) (#) f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) = f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) (#) (r : ( ( complex ) ( complex ) number ) (#) f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) ;

theorem :: RFUNCT_1:14
for f1, f2, f3 being ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) holds (f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) - f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) (#) f3 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) = (f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) (#) f3 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) - (f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) (#) f3 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) ;

theorem :: RFUNCT_1:15
for f3, f1, f2 being ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) holds (f3 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) (#) f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) - (f3 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) (#) f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) = f3 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) (#) (f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) - f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) ;

theorem :: RFUNCT_1:16
for f1, f2 being ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function)
for r being ( ( complex ) ( complex ) number ) holds r : ( ( complex ) ( complex ) number ) (#) (f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) + f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) = (r : ( ( complex ) ( complex ) number ) (#) f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) + (r : ( ( complex ) ( complex ) number ) (#) f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) ;

theorem :: RFUNCT_1:17
for f being ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function)
for r, p being ( ( complex ) ( complex ) number ) holds (r : ( ( complex ) ( complex ) number ) * p : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) set ) (#) f : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) = r : ( ( complex ) ( complex ) number ) (#) (p : ( ( complex ) ( complex ) number ) (#) f : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) ;

theorem :: RFUNCT_1:18
for f1, f2 being ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function)
for r being ( ( complex ) ( complex ) number ) holds r : ( ( complex ) ( complex ) number ) (#) (f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) - f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) = (r : ( ( complex ) ( complex ) number ) (#) f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) - (r : ( ( complex ) ( complex ) number ) (#) f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) ;

theorem :: RFUNCT_1:19
for f1, f2 being ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) holds f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) - f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) = (- 1 : ( ( ) ( non empty ext-real positive non negative natural complex real V33() V34() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of NAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() ) Element of K19(REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non empty ext-real non positive negative complex real ) Element of REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) (#) (f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) - f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) ;

theorem :: RFUNCT_1:20
for f1, f2, f3 being ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) holds f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) - (f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) + f3 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) = (f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) - f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) - f3 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) ;

theorem :: RFUNCT_1:21
for f being ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) holds 1 : ( ( ) ( non empty ext-real positive non negative natural complex real V33() V34() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of NAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() ) Element of K19(REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) (#) f : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) = f : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ;

theorem :: RFUNCT_1:22
for f1, f2, f3 being ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) holds f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) - (f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) - f3 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) = (f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) - f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) + f3 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) ;

theorem :: RFUNCT_1:23
for f1, f2, f3 being ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) holds f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) + (f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) - f3 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) = (f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) + f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) - f3 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) ;

theorem :: RFUNCT_1:24
for f1, f2 being ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) holds abs (f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) (#) f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) = (abs f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) (#) (abs f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) ;

theorem :: RFUNCT_1:25
for f being ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function)
for r being ( ( complex ) ( complex ) number ) holds abs (r : ( ( complex ) ( complex ) number ) (#) f : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) = (abs r : ( ( complex ) ( complex ) number ) ) : ( ( ) ( ext-real complex real ) Element of REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) (#) (abs f : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) ;

theorem :: RFUNCT_1:26
for f being ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) holds (f : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ^) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) Function) ^ : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) Function) = f : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) | (dom (f : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ^) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ) set ) ;

theorem :: RFUNCT_1:27
for f1, f2 being ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) holds (f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) (#) f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) ^ : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) Function) = (f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ^) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) Function) (#) (f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ^) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) Function) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) ;

theorem :: RFUNCT_1:28
for f being ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function)
for r being ( ( complex ) ( complex ) number ) st r : ( ( complex ) ( complex ) number ) <> 0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered V51() V52() ) set ) -valued Function-like one-to-one constant functional empty ext-real non positive non negative natural complex real V33() V34() complex-valued ext-real-valued real-valued natural-valued complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() ) Element of NAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() ) Element of K19(REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) holds
(r : ( ( complex ) ( complex ) number ) (#) f : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) ^ : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) Function) = (r : ( ( complex ) ( complex ) number ) ") : ( ( complex ) ( complex ) set ) (#) (f : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ^) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) Function) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) ;

theorem :: RFUNCT_1:29
for f being ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) holds (- f : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) set ) ^ : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) Function) = (- 1 : ( ( ) ( non empty ext-real positive non negative natural complex real V33() V34() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of NAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() ) Element of K19(REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non empty ext-real non positive negative complex real ) Element of REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) (#) (f : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ^) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) Function) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) ;

theorem :: RFUNCT_1:30
for f being ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) holds (abs f : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) ^ : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) = abs (f : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ^) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) Function) : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) ;

theorem :: RFUNCT_1:31
for f, g being ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) holds f : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) / g : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) Function) = f : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) (#) (g : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ^) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) Function) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) ;

theorem :: RFUNCT_1:32
for g, f being ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function)
for r being ( ( complex ) ( complex ) number ) holds r : ( ( complex ) ( complex ) number ) (#) (g : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) / f : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) Function) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) = (r : ( ( complex ) ( complex ) number ) (#) g : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) / f : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) Function) ;

theorem :: RFUNCT_1:33
for f, g being ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) holds (f : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) / g : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) Function) (#) g : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) = f : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) | (dom (g : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ^) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ) set ) ;

theorem :: RFUNCT_1:34
for f, g, f1, g1 being ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) holds (f : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) / g : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) Function) (#) (f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) / g1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) Function) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) = (f : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) (#) f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) / (g : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) (#) g1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) Function) ;

theorem :: RFUNCT_1:35
for f1, f2 being ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) holds (f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) / f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) Function) ^ : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) Function) = (f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) | (dom (f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ^) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ) set ) / f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) Function) ;

theorem :: RFUNCT_1:36
for g, f1, f2 being ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) holds g : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) (#) (f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) / f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) Function) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) = (g : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) (#) f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) / f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) Function) ;

theorem :: RFUNCT_1:37
for g, f1, f2 being ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) holds g : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) / (f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) / f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) Function) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) Function) = (g : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) (#) (f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) | (dom (f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ^) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) / f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) Function) ;

theorem :: RFUNCT_1:38
for f, g being ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) holds
( - (f : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) / g : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) Function) : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) set ) = (- f : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) set ) / g : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) Function) & f : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) / (- g : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) set ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) Function) = - (f : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) / g : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) Function) : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) set ) ) ;

theorem :: RFUNCT_1:39
for f1, f, f2 being ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) holds
( (f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) / f : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) Function) + (f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) / f : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) Function) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) = (f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) + f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) / f : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) Function) & (f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) / f : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) Function) - (f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) / f : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) Function) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) = (f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) - f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) / f : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) Function) ) ;

theorem :: RFUNCT_1:40
for f1, f, g1, g being ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) holds (f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) / f : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) Function) + (g1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) / g : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) Function) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) = ((f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) (#) g : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) + (g1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) (#) f : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) / (f : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) (#) g : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) Function) ;

theorem :: RFUNCT_1:41
for f, g, f1, g1 being ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) holds (f : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) / g : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) Function) / (f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) / g1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) Function) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) Function) = (f : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) (#) (g1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) | (dom (g1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ^) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) / (g : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) (#) f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) Function) ;

theorem :: RFUNCT_1:42
for f1, f, g1, g being ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) holds (f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) / f : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) Function) - (g1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) / g : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) Function) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) = ((f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) (#) g : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) - (g1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) (#) f : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) / (f : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) (#) g : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) Function) ;

theorem :: RFUNCT_1:43
for f1, f2 being ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) holds abs (f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) / f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) Function) : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) = (abs f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) / (abs f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) ;

theorem :: RFUNCT_1:44
for X being ( ( ) ( ) set )
for f1, f2 being ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) holds
( (f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) + f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) | X : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ) set ) = (f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) | X : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ) set ) + (f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) | X : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ) set ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) & (f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) + f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) | X : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ) set ) = (f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) | X : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ) set ) + f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) & (f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) + f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) | X : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ) set ) = f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) + (f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) | X : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ) set ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) ) ;

theorem :: RFUNCT_1:45
for X being ( ( ) ( ) set )
for f1, f2 being ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) holds
( (f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) (#) f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) | X : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ) set ) = (f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) | X : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ) set ) (#) (f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) | X : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ) set ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) & (f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) (#) f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) | X : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ) set ) = (f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) | X : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ) set ) (#) f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) & (f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) (#) f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) | X : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ) set ) = f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) (#) (f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) | X : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ) set ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) ) ;

theorem :: RFUNCT_1:46
for X being ( ( ) ( ) set )
for f being ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) holds
( (- f : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) set ) | X : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ) set ) = - (f : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) | X : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ) set ) : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) set ) & (f : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ^) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) Function) | X : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ) set ) = (f : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) | X : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ) set ) ^ : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) Function) & (abs f : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) | X : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) = abs (f : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) | X : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ) set ) : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) ) ;

theorem :: RFUNCT_1:47
for X being ( ( ) ( ) set )
for f1, f2 being ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) holds
( (f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) - f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) | X : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ) set ) = (f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) | X : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ) set ) - (f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) | X : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ) set ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) & (f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) - f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) | X : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ) set ) = (f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) | X : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ) set ) - f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) & (f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) - f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) | X : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ) set ) = f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) - (f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) | X : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ) set ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) ) ;

theorem :: RFUNCT_1:48
for X being ( ( ) ( ) set )
for f1, f2 being ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) holds
( (f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) / f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) Function) | X : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ) set ) = (f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) | X : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ) set ) / (f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) | X : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ) set ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) Function) & (f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) / f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) Function) | X : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ) set ) = (f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) | X : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ) set ) / f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) Function) & (f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) / f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) Function) | X : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ) set ) = f1 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) / (f2 : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) | X : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ) set ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) Function) ) ;

theorem :: RFUNCT_1:49
for X being ( ( ) ( ) set )
for f being ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function)
for r being ( ( complex ) ( complex ) number ) holds (r : ( ( complex ) ( complex ) number ) (#) f : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) | X : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ) set ) = r : ( ( complex ) ( complex ) number ) (#) (f : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) Function) | X : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ) set ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ) set ) ;

theorem :: RFUNCT_1:50
for C being ( ( non empty ) ( non empty ) set )
for f1, f2 being ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) holds
( ( f1 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) is total & f2 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) is total implies f1 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) + f2 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is total ) & ( f1 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) + f2 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is total implies ( f1 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) is total & f2 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) is total ) ) & ( f1 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) is total & f2 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) is total implies f1 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) - f2 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is total ) & ( f1 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) - f2 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is total implies ( f1 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) is total & f2 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) is total ) ) & ( f1 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) is total & f2 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) is total implies f1 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) (#) f2 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is total ) & ( f1 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) (#) f2 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is total implies ( f1 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) is total & f2 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) is total ) ) ) ;

theorem :: RFUNCT_1:51
for C being ( ( non empty ) ( non empty ) set )
for r being ( ( real ) ( ext-real complex real ) number )
for f being ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) holds
( f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) is total iff r : ( ( real ) ( ext-real complex real ) number ) (#) f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is total ) ;

theorem :: RFUNCT_1:52
for C being ( ( non empty ) ( non empty ) set )
for f being ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) holds
( f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) is total iff - f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is total ) ;

theorem :: RFUNCT_1:53
for C being ( ( non empty ) ( non empty ) set )
for f being ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) holds
( f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) is total iff abs f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is total ) ;

theorem :: RFUNCT_1:54
for C being ( ( non empty ) ( non empty ) set )
for f being ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) holds
( f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ^ : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) is total iff ( f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) " {0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered V51() V52() ) set ) -valued Function-like one-to-one constant functional empty ext-real non positive non negative natural complex real V33() V34() complex-valued ext-real-valued real-valued natural-valued complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() ) Element of NAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() ) Element of K19(REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) } : ( ( ) ( functional non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) : ( ( ) ( ) Element of K19(b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) = {} : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered V51() V52() ) set ) -valued Function-like one-to-one constant functional empty complex-valued ext-real-valued real-valued natural-valued complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() ) set ) & f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) is total ) ) ;

theorem :: RFUNCT_1:55
for C being ( ( non empty ) ( non empty ) set )
for f1, f2 being ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) holds
( ( f1 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) is total & f2 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) " {0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered V51() V52() ) set ) -valued Function-like one-to-one constant functional empty ext-real non positive non negative natural complex real V33() V34() complex-valued ext-real-valued real-valued natural-valued complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() ) Element of NAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() ) Element of K19(REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) } : ( ( ) ( functional non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) : ( ( ) ( ) Element of K19(b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) = {} : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered V51() V52() ) set ) -valued Function-like one-to-one constant functional empty complex-valued ext-real-valued real-valued natural-valued complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() ) set ) & f2 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) is total ) iff f1 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) / f2 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) is total ) ;

theorem :: RFUNCT_1:56
for C being ( ( non empty ) ( non empty ) set )
for c being ( ( ) ( ) Element of C : ( ( non empty ) ( non empty ) set ) )
for f1, f2 being ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st f1 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) is total & f2 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) is total holds
( (f1 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) + f2 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) . c : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ext-real complex real ) set ) = (f1 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . c : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ext-real complex real ) set ) + (f2 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . c : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ext-real complex real ) set ) : ( ( ) ( complex ) set ) & (f1 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) - f2 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) . c : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ext-real complex real ) set ) = (f1 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . c : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ext-real complex real ) set ) - (f2 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . c : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ext-real complex real ) set ) : ( ( ) ( complex ) set ) & (f1 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) (#) f2 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) . c : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ext-real complex real ) set ) = (f1 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . c : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ext-real complex real ) set ) * (f2 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . c : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ext-real complex real ) set ) : ( ( ) ( complex ) set ) ) ;

theorem :: RFUNCT_1:57
for C being ( ( non empty ) ( non empty ) set )
for c being ( ( ) ( ) Element of C : ( ( non empty ) ( non empty ) set ) )
for r being ( ( real ) ( ext-real complex real ) number )
for f being ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) is total holds
(r : ( ( real ) ( ext-real complex real ) number ) (#) f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) . c : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ext-real complex real ) set ) = r : ( ( real ) ( ext-real complex real ) number ) * (f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . c : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ext-real complex real ) set ) : ( ( ) ( ext-real complex real ) set ) ;

theorem :: RFUNCT_1:58
for C being ( ( non empty ) ( non empty ) set )
for c being ( ( ) ( ) Element of C : ( ( non empty ) ( non empty ) set ) )
for f being ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) is total holds
( (- f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) . c : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ext-real complex real ) set ) = - (f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . c : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ext-real complex real ) set ) : ( ( complex ) ( complex ) set ) & (abs f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) . c : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ext-real complex real ) set ) = abs (f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . c : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ext-real complex real ) set ) : ( ( ) ( ext-real complex real ) Element of REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) ) ;

theorem :: RFUNCT_1:59
for C being ( ( non empty ) ( non empty ) set )
for c being ( ( ) ( ) Element of C : ( ( non empty ) ( non empty ) set ) )
for f being ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ^ : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) is total holds
(f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ^) : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . c : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ext-real complex real ) set ) = (f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . c : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ext-real complex real ) set ) " : ( ( complex ) ( complex ) set ) ;

theorem :: RFUNCT_1:60
for C being ( ( non empty ) ( non empty ) set )
for c being ( ( ) ( ) Element of C : ( ( non empty ) ( non empty ) set ) )
for f1, f2 being ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st f1 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) is total & f2 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ^ : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) is total holds
(f1 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) / f2 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . c : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ext-real complex real ) set ) = (f1 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . c : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ext-real complex real ) set ) * ((f2 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . c : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ext-real complex real ) set ) ") : ( ( complex ) ( ext-real complex real ) set ) : ( ( ) ( complex ) set ) ;

definition
let X, C be ( ( ) ( ) set ) ;
:: original: chi
redefine func chi (X,C) -> ( ( Function-like ) ( Relation-like C : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ;
end;

registration
let X, C be ( ( ) ( ) set ) ;
cluster chi (X : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) -> Function-like total for ( ( Function-like ) ( Relation-like C : ( ( ) ( ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ;
end;

theorem :: RFUNCT_1:61
for X being ( ( ) ( ) set )
for C being ( ( non empty ) ( non empty ) set )
for f being ( ( Function-like ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) holds
( f : ( ( Function-like ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) = chi (X : ( ( ) ( ) set ) ,C : ( ( non empty ) ( non empty ) set ) ) : ( ( Function-like ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like total complex-valued ext-real-valued real-valued ) PartFunc of ,) iff ( dom f : ( ( Function-like ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( ) ( ) Element of K19(b2 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) = C : ( ( non empty ) ( non empty ) set ) & ( for c being ( ( ) ( ) Element of C : ( ( non empty ) ( non empty ) set ) ) holds
( ( c : ( ( ) ( ) Element of b2 : ( ( non empty ) ( non empty ) set ) ) in X : ( ( ) ( ) set ) implies f : ( ( Function-like ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . c : ( ( ) ( ) Element of b2 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ext-real complex real ) set ) = 1 : ( ( ) ( non empty ext-real positive non negative natural complex real V33() V34() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of NAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() ) Element of K19(REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ) & ( not c : ( ( ) ( ) Element of b2 : ( ( non empty ) ( non empty ) set ) ) in X : ( ( ) ( ) set ) implies f : ( ( Function-like ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . c : ( ( ) ( ) Element of b2 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ext-real complex real ) set ) = 0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered V51() V52() ) set ) -valued Function-like one-to-one constant functional empty ext-real non positive non negative natural complex real V33() V34() complex-valued ext-real-valued real-valued natural-valued complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() ) Element of NAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() ) Element of K19(REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) ) ) ) ;

theorem :: RFUNCT_1:62
for X being ( ( ) ( ) set )
for C being ( ( non empty ) ( non empty ) set ) holds chi (X : ( ( ) ( ) set ) ,C : ( ( non empty ) ( non empty ) set ) ) : ( ( Function-like ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like total complex-valued ext-real-valued real-valued ) PartFunc of ,) is total ;

theorem :: RFUNCT_1:63
for X being ( ( ) ( ) set )
for C being ( ( non empty ) ( non empty ) set )
for c being ( ( ) ( ) Element of C : ( ( non empty ) ( non empty ) set ) ) holds
( c : ( ( ) ( ) Element of b2 : ( ( non empty ) ( non empty ) set ) ) in X : ( ( ) ( ) set ) iff (chi (X : ( ( ) ( ) set ) ,C : ( ( non empty ) ( non empty ) set ) )) : ( ( Function-like ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like total complex-valued ext-real-valued real-valued ) PartFunc of ,) . c : ( ( ) ( ) Element of b2 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ext-real complex real ) set ) = 1 : ( ( ) ( non empty ext-real positive non negative natural complex real V33() V34() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of NAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() ) Element of K19(REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ) ;

theorem :: RFUNCT_1:64
for X being ( ( ) ( ) set )
for C being ( ( non empty ) ( non empty ) set )
for c being ( ( ) ( ) Element of C : ( ( non empty ) ( non empty ) set ) ) holds
( not c : ( ( ) ( ) Element of b2 : ( ( non empty ) ( non empty ) set ) ) in X : ( ( ) ( ) set ) iff (chi (X : ( ( ) ( ) set ) ,C : ( ( non empty ) ( non empty ) set ) )) : ( ( Function-like ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like total complex-valued ext-real-valued real-valued ) PartFunc of ,) . c : ( ( ) ( ) Element of b2 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ext-real complex real ) set ) = 0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered V51() V52() ) set ) -valued Function-like one-to-one constant functional empty ext-real non positive non negative natural complex real V33() V34() complex-valued ext-real-valued real-valued natural-valued complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() ) Element of NAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() ) Element of K19(REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ) ;

theorem :: RFUNCT_1:65
for X being ( ( ) ( ) set )
for C being ( ( non empty ) ( non empty ) set )
for c being ( ( ) ( ) Element of C : ( ( non empty ) ( non empty ) set ) ) holds
( c : ( ( ) ( ) Element of b2 : ( ( non empty ) ( non empty ) set ) ) in C : ( ( non empty ) ( non empty ) set ) \ X : ( ( ) ( ) set ) : ( ( ) ( ) Element of K19(b2 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) iff (chi (X : ( ( ) ( ) set ) ,C : ( ( non empty ) ( non empty ) set ) )) : ( ( Function-like ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like total complex-valued ext-real-valued real-valued ) PartFunc of ,) . c : ( ( ) ( ) Element of b2 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ext-real complex real ) set ) = 0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered V51() V52() ) set ) -valued Function-like one-to-one constant functional empty ext-real non positive non negative natural complex real V33() V34() complex-valued ext-real-valued real-valued natural-valued complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() ) Element of NAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() ) Element of K19(REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ) ;

theorem :: RFUNCT_1:66
for C being ( ( non empty ) ( non empty ) set )
for c being ( ( ) ( ) Element of C : ( ( non empty ) ( non empty ) set ) ) holds (chi (C : ( ( non empty ) ( non empty ) set ) ,C : ( ( non empty ) ( non empty ) set ) )) : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like total complex-valued ext-real-valued real-valued ) PartFunc of ,) . c : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ext-real complex real ) set ) = 1 : ( ( ) ( non empty ext-real positive non negative natural complex real V33() V34() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of NAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() ) Element of K19(REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: RFUNCT_1:67
for X being ( ( ) ( ) set )
for C being ( ( non empty ) ( non empty ) set )
for c being ( ( ) ( ) Element of C : ( ( non empty ) ( non empty ) set ) ) holds
( (chi (X : ( ( ) ( ) set ) ,C : ( ( non empty ) ( non empty ) set ) )) : ( ( Function-like ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like total complex-valued ext-real-valued real-valued ) PartFunc of ,) . c : ( ( ) ( ) Element of b2 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ext-real complex real ) set ) <> 1 : ( ( ) ( non empty ext-real positive non negative natural complex real V33() V34() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) Element of NAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() ) Element of K19(REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) iff (chi (X : ( ( ) ( ) set ) ,C : ( ( non empty ) ( non empty ) set ) )) : ( ( Function-like ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like total complex-valued ext-real-valued real-valued ) PartFunc of ,) . c : ( ( ) ( ) Element of b2 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ext-real complex real ) set ) = 0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered V51() V52() ) set ) -valued Function-like one-to-one constant functional empty ext-real non positive non negative natural complex real V33() V34() complex-valued ext-real-valued real-valued natural-valued complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() ) Element of NAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() ) Element of K19(REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) ) ;

theorem :: RFUNCT_1:68
for X, Y being ( ( ) ( ) set )
for C being ( ( non empty ) ( non empty ) set ) st X : ( ( ) ( ) set ) misses Y : ( ( ) ( ) set ) holds
(chi (X : ( ( ) ( ) set ) ,C : ( ( non empty ) ( non empty ) set ) )) : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like total complex-valued ext-real-valued real-valued ) PartFunc of ,) + (chi (Y : ( ( ) ( ) set ) ,C : ( ( non empty ) ( non empty ) set ) )) : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like total complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like total complex-valued ext-real-valued real-valued ) Element of K19(K20(b3 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) = chi ((X : ( ( ) ( ) set ) \/ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,C : ( ( non empty ) ( non empty ) set ) ) : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like total complex-valued ext-real-valued real-valued ) PartFunc of ,) ;

theorem :: RFUNCT_1:69
for X, Y being ( ( ) ( ) set )
for C being ( ( non empty ) ( non empty ) set ) holds (chi (X : ( ( ) ( ) set ) ,C : ( ( non empty ) ( non empty ) set ) )) : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like total complex-valued ext-real-valued real-valued ) PartFunc of ,) (#) (chi (Y : ( ( ) ( ) set ) ,C : ( ( non empty ) ( non empty ) set ) )) : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like total complex-valued ext-real-valued real-valued ) PartFunc of ,) : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like total complex-valued ext-real-valued real-valued ) Element of K19(K20(b3 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) = chi ((X : ( ( ) ( ) set ) /\ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,C : ( ( non empty ) ( non empty ) set ) ) : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like total complex-valued ext-real-valued real-valued ) PartFunc of ,) ;

theorem :: RFUNCT_1:70
for Y being ( ( ) ( ) set )
for f being ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) holds
( f : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) | Y : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) is bounded_above iff ex r being ( ( real ) ( ext-real complex real ) number ) st
for c being ( ( ) ( ) set ) st c : ( ( ) ( ) set ) in Y : ( ( ) ( ) set ) /\ (dom f : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) holds
f : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) . c : ( ( ) ( ) set ) : ( ( ) ( ext-real complex real ) set ) <= r : ( ( real ) ( ext-real complex real ) number ) ) ;

theorem :: RFUNCT_1:71
for Y being ( ( ) ( ) set )
for f being ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) holds
( f : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) | Y : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) is bounded_below iff ex r being ( ( real ) ( ext-real complex real ) number ) st
for c being ( ( ) ( ) set ) st c : ( ( ) ( ) set ) in Y : ( ( ) ( ) set ) /\ (dom f : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) holds
r : ( ( real ) ( ext-real complex real ) number ) <= f : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) . c : ( ( ) ( ) set ) : ( ( ) ( ext-real complex real ) set ) ) ;

theorem :: RFUNCT_1:72
for f being ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) holds
( f : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) is bounded iff ex r being ( ( real ) ( ext-real complex real ) number ) st
for c being ( ( ) ( ) set ) st c : ( ( ) ( ) set ) in dom f : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) : ( ( ) ( ) set ) holds
abs (f : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) . c : ( ( ) ( ) set ) ) : ( ( ) ( ext-real complex real ) set ) : ( ( ) ( ext-real complex real ) Element of REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) <= r : ( ( real ) ( ext-real complex real ) number ) ) ;

theorem :: RFUNCT_1:73
for Y being ( ( ) ( ) set )
for f being ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) holds
( f : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) | Y : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) is bounded iff ex r being ( ( real ) ( ext-real complex real ) number ) st
for c being ( ( ) ( ) set ) st c : ( ( ) ( ) set ) in Y : ( ( ) ( ) set ) /\ (dom f : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) holds
abs (f : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) . c : ( ( ) ( ) set ) ) : ( ( ) ( ext-real complex real ) set ) : ( ( ) ( ext-real complex real ) Element of REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) <= r : ( ( real ) ( ext-real complex real ) number ) ) ;

theorem :: RFUNCT_1:74
for Y, X being ( ( ) ( ) set )
for f being ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) holds
( ( Y : ( ( ) ( ) set ) c= X : ( ( ) ( ) set ) & f : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) | X : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) is bounded_above implies f : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) | Y : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) is bounded_above ) & ( Y : ( ( ) ( ) set ) c= X : ( ( ) ( ) set ) & f : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) | X : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) is bounded_below implies f : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) | Y : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) is bounded_below ) & ( Y : ( ( ) ( ) set ) c= X : ( ( ) ( ) set ) & f : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) | X : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) is bounded implies f : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) | Y : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) is bounded ) ) ;

theorem :: RFUNCT_1:75
for X, Y being ( ( ) ( ) set )
for f being ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) st f : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) | X : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) is bounded_above & f : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) | Y : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) is bounded_below holds
f : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) | (X : ( ( ) ( ) set ) /\ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) is bounded ;

registration
cluster Relation-like Function-like constant real-valued -> Relation-like Function-like real-valued bounded for ( ( ) ( ) set ) ;
end;

theorem :: RFUNCT_1:76
for X being ( ( ) ( ) set )
for f being ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) st X : ( ( ) ( ) set ) misses dom f : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) : ( ( ) ( ) set ) holds
f : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) | X : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) is bounded ;

theorem :: RFUNCT_1:77
for Y being ( ( ) ( ) set )
for f being ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) holds (0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered V51() V52() ) set ) -valued Function-like one-to-one constant functional empty ext-real non positive non negative natural complex real V33() V34() complex-valued ext-real-valued real-valued natural-valued complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() bounded_above bounded_below bounded ) Element of NAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() ) Element of K19(REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) (#) f : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) | Y : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) is bounded ;

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

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

registration
let f be ( ( Relation-like Function-like real-valued bounded_above ) ( Relation-like Function-like complex-valued ext-real-valued real-valued bounded_above ) Function) ;
let r be ( ( non negative real ) ( ext-real non negative complex real ) number ) ;
cluster r : ( ( non negative real ) ( ext-real non negative complex real ) set ) (#) f : ( ( Relation-like Function-like real-valued bounded_above ) ( Relation-like Function-like complex-valued ext-real-valued real-valued bounded_above ) set ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) -> Relation-like Function-like real-valued bounded_above for ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) ;
end;

registration
let f be ( ( Relation-like Function-like real-valued bounded_below ) ( Relation-like Function-like complex-valued ext-real-valued real-valued bounded_below ) Function) ;
let r be ( ( non negative real ) ( ext-real non negative complex real ) number ) ;
cluster r : ( ( non negative real ) ( ext-real non negative complex real ) set ) (#) f : ( ( Relation-like Function-like real-valued bounded_below ) ( Relation-like Function-like complex-valued ext-real-valued real-valued bounded_below ) set ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) -> Relation-like Function-like real-valued bounded_below for ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) ;
end;

registration
let f be ( ( Relation-like Function-like real-valued bounded_above ) ( Relation-like Function-like complex-valued ext-real-valued real-valued bounded_above ) Function) ;
let r be ( ( non positive real ) ( ext-real non positive complex real ) number ) ;
cluster r : ( ( non positive real ) ( ext-real non positive complex real ) set ) (#) f : ( ( Relation-like Function-like real-valued bounded_above ) ( Relation-like Function-like complex-valued ext-real-valued real-valued bounded_above ) set ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) -> Relation-like Function-like real-valued bounded_below for ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) ;
end;

registration
let f be ( ( Relation-like Function-like real-valued bounded_below ) ( Relation-like Function-like complex-valued ext-real-valued real-valued bounded_below ) Function) ;
let r be ( ( non positive real ) ( ext-real non positive complex real ) number ) ;
cluster r : ( ( non positive real ) ( ext-real non positive complex real ) set ) (#) f : ( ( Relation-like Function-like real-valued bounded_below ) ( Relation-like Function-like complex-valued ext-real-valued real-valued bounded_below ) set ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) -> Relation-like Function-like real-valued bounded_above for ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) ;
end;

theorem :: RFUNCT_1:78
for Y being ( ( ) ( ) set )
for r being ( ( real ) ( ext-real complex real ) number )
for f being ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) holds
( ( f : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) | Y : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) is bounded_above & 0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered V51() V52() ) set ) -valued Function-like one-to-one constant functional empty ext-real non positive non negative natural complex real V33() V34() complex-valued ext-real-valued real-valued natural-valued complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() bounded_above bounded_below bounded ) Element of NAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() ) Element of K19(REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) <= r : ( ( real ) ( ext-real complex real ) number ) implies (r : ( ( real ) ( ext-real complex real ) number ) (#) f : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) | Y : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) is bounded_above ) & ( f : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) | Y : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) is bounded_above & r : ( ( real ) ( ext-real complex real ) number ) <= 0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered V51() V52() ) set ) -valued Function-like one-to-one constant functional empty ext-real non positive non negative natural complex real V33() V34() complex-valued ext-real-valued real-valued natural-valued complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() bounded_above bounded_below bounded ) Element of NAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() ) Element of K19(REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) implies (r : ( ( real ) ( ext-real complex real ) number ) (#) f : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) | Y : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) is bounded_below ) ) ;

theorem :: RFUNCT_1:79
for Y being ( ( ) ( ) set )
for r being ( ( real ) ( ext-real complex real ) number )
for f being ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) holds
( ( f : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) | Y : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) is bounded_below & 0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered V51() V52() ) set ) -valued Function-like one-to-one constant functional empty ext-real non positive non negative natural complex real V33() V34() complex-valued ext-real-valued real-valued natural-valued complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() bounded_above bounded_below bounded ) Element of NAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() ) Element of K19(REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) <= r : ( ( real ) ( ext-real complex real ) number ) implies (r : ( ( real ) ( ext-real complex real ) number ) (#) f : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) | Y : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) is bounded_below ) & ( f : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) | Y : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) is bounded_below & r : ( ( real ) ( ext-real complex real ) number ) <= 0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty complex-membered ext-real-membered real-membered rational-membered V51() V52() ) set ) -valued Function-like one-to-one constant functional empty ext-real non positive non negative natural complex real V33() V34() complex-valued ext-real-valued real-valued natural-valued complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() bounded_above bounded_below bounded ) Element of NAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V51() ) Element of K19(REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( ) set ) ) ) implies (r : ( ( real ) ( ext-real complex real ) number ) (#) f : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) | Y : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) is bounded_above ) ) ;

theorem :: RFUNCT_1:80
for Y being ( ( ) ( ) set )
for r being ( ( real ) ( ext-real complex real ) number )
for f being ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) st f : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) | Y : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) is bounded holds
(r : ( ( real ) ( ext-real complex real ) number ) (#) f : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) | Y : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) is bounded ;

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

theorem :: RFUNCT_1:81
for X being ( ( ) ( ) set )
for f being ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) holds (abs f : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) ) : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued bounded_below ) set ) | X : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued bounded_below ) set ) is bounded_below ;

registration
let f be ( ( Relation-like Function-like real-valued bounded ) ( Relation-like Function-like complex-valued ext-real-valued real-valued bounded_above bounded_below bounded ) Function) ;
cluster |.f : ( ( Relation-like Function-like real-valued bounded ) ( Relation-like Function-like complex-valued ext-real-valued real-valued bounded_above bounded_below bounded ) set ) .| : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued bounded_below ) set ) -> Relation-like Function-like real-valued bounded for ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) ;
end;

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

theorem :: RFUNCT_1:82
for Y being ( ( ) ( ) set )
for f being ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) st f : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) | Y : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) is bounded holds
( (abs f : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) ) : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued bounded_below ) set ) | Y : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued bounded_below ) set ) is bounded & (- f : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) ) : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) | Y : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) is bounded ) ;

registration
let f1, f2 be ( ( Relation-like Function-like real-valued bounded_above ) ( Relation-like Function-like complex-valued ext-real-valued real-valued bounded_above ) Function) ;
cluster f1 : ( ( Relation-like Function-like real-valued bounded_above ) ( Relation-like Function-like complex-valued ext-real-valued real-valued bounded_above ) set ) + f2 : ( ( Relation-like Function-like real-valued bounded_above ) ( Relation-like Function-like complex-valued ext-real-valued real-valued bounded_above ) set ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) -> Relation-like Function-like real-valued bounded_above for ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) ;
end;

registration
let f1, f2 be ( ( Relation-like Function-like real-valued bounded_below ) ( Relation-like Function-like complex-valued ext-real-valued real-valued bounded_below ) Function) ;
cluster f1 : ( ( Relation-like Function-like real-valued bounded_below ) ( Relation-like Function-like complex-valued ext-real-valued real-valued bounded_below ) set ) + f2 : ( ( Relation-like Function-like real-valued bounded_below ) ( Relation-like Function-like complex-valued ext-real-valued real-valued bounded_below ) set ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) -> Relation-like Function-like real-valued bounded_below for ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) ;
end;

theorem :: RFUNCT_1:83
for X, Y being ( ( ) ( ) set )
for f1, f2 being ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) holds
( ( f1 : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) | X : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) is bounded_above & f2 : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) | Y : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) is bounded_above implies (f1 : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) + f2 : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) | (X : ( ( ) ( ) set ) /\ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) is bounded_above ) & ( f1 : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) | X : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) is bounded_below & f2 : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) | Y : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) is bounded_below implies (f1 : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) + f2 : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) | (X : ( ( ) ( ) set ) /\ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) is bounded_below ) & ( f1 : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) | X : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) is bounded & f2 : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) | Y : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) is bounded implies (f1 : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) + f2 : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) | (X : ( ( ) ( ) set ) /\ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) is bounded ) ) ;

registration
let f1, f2 be ( ( Relation-like Function-like real-valued bounded ) ( Relation-like Function-like complex-valued ext-real-valued real-valued bounded_above bounded_below bounded ) Function) ;
cluster f1 : ( ( Relation-like Function-like real-valued bounded ) ( Relation-like Function-like complex-valued ext-real-valued real-valued bounded_above bounded_below bounded ) set ) (#) f2 : ( ( Relation-like Function-like real-valued bounded ) ( Relation-like Function-like complex-valued ext-real-valued real-valued bounded_above bounded_below bounded ) set ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) -> Relation-like Function-like real-valued bounded for ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) ;
end;

theorem :: RFUNCT_1:84
for X, Y being ( ( ) ( ) set )
for f1, f2 being ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) st f1 : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) | X : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) is bounded & f2 : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) | Y : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) is bounded holds
( (f1 : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) (#) f2 : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) | (X : ( ( ) ( ) set ) /\ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) is bounded & (f1 : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) - f2 : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) | (X : ( ( ) ( ) set ) /\ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) is bounded ) ;

theorem :: RFUNCT_1:85
for X, Y being ( ( ) ( ) set )
for f being ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) st f : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) | X : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) is bounded_above & f : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) | Y : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) is bounded_above holds
f : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) | (X : ( ( ) ( ) set ) \/ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) is bounded_above ;

theorem :: RFUNCT_1:86
for X, Y being ( ( ) ( ) set )
for f being ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) st f : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) | X : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) is bounded_below & f : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) | Y : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) is bounded_below holds
f : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) | (X : ( ( ) ( ) set ) \/ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) is bounded_below ;

theorem :: RFUNCT_1:87
for X, Y being ( ( ) ( ) set )
for f being ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) st f : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) | X : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) is bounded & f : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) | Y : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) is bounded holds
f : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) | (X : ( ( ) ( ) set ) \/ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) is bounded ;

registration
let C be ( ( non empty ) ( non empty ) set ) ;
let f1, f2 be ( ( Function-like constant ) ( Relation-like C : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like constant complex-valued ext-real-valued real-valued bounded_above bounded_below bounded ) PartFunc of ,) ;
cluster f1 : ( ( Function-like constant ) ( Relation-like C : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like constant complex-valued ext-real-valued real-valued bounded_above bounded_below bounded ) Element of K19(K20(C : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) + f2 : ( ( Function-like constant ) ( Relation-like C : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like constant complex-valued ext-real-valued real-valued bounded_above bounded_below bounded ) Element of K19(K20(C : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like C : ( ( non empty ) ( non empty ) set ) -defined Function-like complex-valued ext-real-valued real-valued bounded_above bounded_below bounded ) set ) -> Relation-like Function-like constant ;
cluster f1 : ( ( Function-like constant ) ( Relation-like C : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like constant complex-valued ext-real-valued real-valued bounded_above bounded_below bounded ) Element of K19(K20(C : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) - f2 : ( ( Function-like constant ) ( Relation-like C : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like constant complex-valued ext-real-valued real-valued bounded_above bounded_below bounded ) Element of K19(K20(C : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like C : ( ( non empty ) ( non empty ) set ) -defined Function-like complex-valued ext-real-valued real-valued ) set ) -> Relation-like Function-like constant ;
cluster f1 : ( ( Function-like constant ) ( Relation-like C : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like constant complex-valued ext-real-valued real-valued bounded_above bounded_below bounded ) Element of K19(K20(C : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) (#) f2 : ( ( Function-like constant ) ( Relation-like C : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like constant complex-valued ext-real-valued real-valued bounded_above bounded_below bounded ) Element of K19(K20(C : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like C : ( ( non empty ) ( non empty ) set ) -defined Function-like complex-valued ext-real-valued real-valued bounded_above bounded_below bounded ) set ) -> Relation-like Function-like constant ;
end;

theorem :: RFUNCT_1:88
for X, Y being ( ( ) ( ) set )
for C being ( ( non empty ) ( non empty ) set )
for f1, f2 being ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st f1 : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(b3 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is constant & f2 : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | Y : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(b3 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is constant holds
( (f1 : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) + f2 : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(b3 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) | (X : ( ( ) ( ) set ) /\ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( ) ( ) set ) /\ b2 : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(b3 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is constant & (f1 : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) - f2 : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(b3 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) | (X : ( ( ) ( ) set ) /\ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( ) ( ) set ) /\ b2 : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(b3 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is constant & (f1 : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) (#) f2 : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(b3 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) | (X : ( ( ) ( ) set ) /\ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( ) ( ) set ) /\ b2 : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(b3 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is constant ) ;

registration
let C be ( ( non empty ) ( non empty ) set ) ;
let f be ( ( Function-like constant ) ( Relation-like C : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like constant complex-valued ext-real-valued real-valued bounded_above bounded_below bounded ) PartFunc of ,) ;
cluster - f : ( ( Function-like constant ) ( Relation-like C : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like constant complex-valued ext-real-valued real-valued bounded_above bounded_below bounded ) Element of K19(K20(C : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like complex-valued ) ( Relation-like C : ( ( non empty ) ( non empty ) set ) -defined Function-like complex-valued ext-real-valued real-valued bounded_below ) set ) -> Relation-like Function-like constant complex-valued ;
cluster |.f : ( ( Function-like constant ) ( Relation-like C : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like constant complex-valued ext-real-valued real-valued bounded_above bounded_below bounded ) Element of K19(K20(C : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) .| : ( ( Relation-like Function-like real-valued ) ( Relation-like C : ( ( non empty ) ( non empty ) set ) -defined Function-like complex-valued ext-real-valued real-valued bounded_above bounded_below bounded ) set ) -> Relation-like Function-like constant real-valued ;
let p be ( ( real ) ( ext-real complex real ) number ) ;
cluster p : ( ( real ) ( ext-real complex real ) set ) (#) f : ( ( Function-like constant ) ( Relation-like C : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like constant complex-valued ext-real-valued real-valued bounded_above bounded_below bounded ) Element of K19(K20(C : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like C : ( ( non empty ) ( non empty ) set ) -defined Function-like complex-valued ext-real-valued real-valued ) set ) -> Relation-like Function-like constant ;
end;

theorem :: RFUNCT_1:89
for Y being ( ( ) ( ) set )
for C being ( ( non empty ) ( non empty ) set )
for p being ( ( real ) ( ext-real complex real ) number )
for f being ( ( Function-like ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st f : ( ( Function-like ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | Y : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(b2 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is constant holds
(p : ( ( real ) ( ext-real complex real ) number ) (#) f : ( ( Function-like ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(b2 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) | Y : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(b2 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is constant ;

theorem :: RFUNCT_1:90
for Y being ( ( ) ( ) set )
for C being ( ( non empty ) ( non empty ) set )
for f being ( ( Function-like ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st f : ( ( Function-like ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | Y : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(b2 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is constant holds
(- f : ( ( Function-like ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(b2 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) | Y : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(b2 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is constant ;

theorem :: RFUNCT_1:91
for Y being ( ( ) ( ) set )
for C being ( ( non empty ) ( non empty ) set )
for f being ( ( Function-like ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st f : ( ( Function-like ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | Y : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(b2 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is constant holds
(abs f : ( ( Function-like ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued bounded_below ) Element of K19(K20(b2 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) | Y : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued bounded_below ) Element of K19(K20(b2 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is constant ;

theorem :: RFUNCT_1:92
for Y being ( ( ) ( ) set )
for C being ( ( non empty ) ( non empty ) set )
for f being ( ( Function-like ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) st f : ( ( Function-like ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | Y : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(b2 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is constant holds
( ( for r being ( ( real ) ( ext-real complex real ) number ) holds (r : ( ( real ) ( ext-real complex real ) number ) (#) f : ( ( Function-like ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(b2 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) | Y : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(b2 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is bounded ) & (- f : ( ( Function-like ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(b2 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) | Y : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(b2 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is bounded & (abs f : ( ( Function-like ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued bounded_below ) Element of K19(K20(b2 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) | Y : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued bounded_below ) Element of K19(K20(b2 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is bounded ) ;

theorem :: RFUNCT_1:93
for X, Y being ( ( ) ( ) set )
for C being ( ( non empty ) ( non empty ) set )
for f1, f2 being ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) holds
( ( f1 : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(b3 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is bounded_above & f2 : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | Y : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(b3 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is constant implies (f1 : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) + f2 : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(b3 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) | (X : ( ( ) ( ) set ) /\ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( ) ( ) set ) /\ b2 : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(b3 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is bounded_above ) & ( f1 : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(b3 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is bounded_below & f2 : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | Y : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(b3 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is constant implies (f1 : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) + f2 : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(b3 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) | (X : ( ( ) ( ) set ) /\ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( ) ( ) set ) /\ b2 : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(b3 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is bounded_below ) & ( f1 : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(b3 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is bounded & f2 : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | Y : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(b3 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is constant implies (f1 : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) + f2 : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(b3 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) | (X : ( ( ) ( ) set ) /\ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( ) ( ) set ) /\ b2 : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(b3 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is bounded ) ) ;

theorem :: RFUNCT_1:94
for X, Y being ( ( ) ( ) set )
for C being ( ( non empty ) ( non empty ) set )
for f1, f2 being ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) holds
( ( f1 : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(b3 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is bounded_above & f2 : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | Y : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(b3 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is constant implies (f1 : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) - f2 : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(b3 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) | (X : ( ( ) ( ) set ) /\ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( ) ( ) set ) /\ b2 : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(b3 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is bounded_above ) & ( f1 : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(b3 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is bounded_below & f2 : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | Y : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(b3 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is constant implies (f1 : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) - f2 : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(b3 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) | (X : ( ( ) ( ) set ) /\ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( ) ( ) set ) /\ b2 : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(b3 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is bounded_below ) & ( f1 : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | X : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(b3 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is bounded & f2 : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) | Y : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b2 : ( ( ) ( ) set ) -defined b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(b3 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is constant implies ( (f1 : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) - f2 : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(b3 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) | (X : ( ( ) ( ) set ) /\ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( ) ( ) set ) /\ b2 : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(b3 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is bounded & (f2 : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) - f1 : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(b3 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) | (X : ( ( ) ( ) set ) /\ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( ) ( ) set ) /\ b2 : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(b3 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is bounded & (f1 : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) (#) f2 : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(b3 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) | (X : ( ( ) ( ) set ) /\ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined b1 : ( ( ) ( ) set ) /\ b2 : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Element of K19(K20(b3 : ( ( non empty ) ( non empty ) set ) ,REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is bounded ) ) ) ;