:: VALUED_0 semantic presentation

begin

definition
let f be ( ( Relation-like ) ( Relation-like ) Relation) ;
attr f is complex-valued means :: VALUED_0:def 1
 rng f : ( ( integer ) ( complex real integer rational ext-real ) set ) : ( ( ) ( ) set ) c= COMPLEX : ( ( ) ( complex-membered V21() ) set ) ;
attr f is ext-real-valued means :: VALUED_0:def 2
 rng f : ( ( integer ) ( complex real integer rational ext-real ) set ) : ( ( ) ( ) set ) c= ExtREAL : ( ( ) ( ext-real-membered ) set ) ;
attr f is real-valued means :: VALUED_0:def 3
 rng f : ( ( integer ) ( complex real integer rational ext-real ) set ) : ( ( ) ( ) set ) c= REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) ;
canceled;
canceled;
attr f is natural-valued means :: VALUED_0:def 6
 rng f : ( ( integer ) ( complex real integer rational ext-real ) set ) : ( ( ) ( ) set ) c= NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

registration
cluster Relation-like natural-valued -> Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued for ( ( ) ( ) set ) ;
cluster Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued -> Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued for ( ( ) ( ) set ) ;
cluster Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued -> Relation-like real-valued for ( ( ) ( ) set ) ;
cluster Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued -> Relation-like real-valued for ( ( ) ( ) set ) ;
cluster Relation-like real-valued -> Relation-like ext-real-valued for ( ( ) ( ) set ) ;
cluster Relation-like real-valued -> Relation-like complex-valued for ( ( ) ( ) set ) ;
cluster Relation-like natural-valued -> Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued for ( ( ) ( ) set ) ;
cluster Relation-like natural-valued -> Relation-like real-valued for ( ( ) ( ) set ) ;
end;

registration
cluster empty Relation-like -> Relation-like natural-valued for ( ( ) ( ) set ) ;
end;

registration
cluster Relation-like Function-like natural-valued for ( ( ) ( ) set ) ;
end;

registration
let R be ( ( Relation-like complex-valued ) ( Relation-like complex-valued ) Relation) ;
cluster rng R : ( ( Relation-like complex-valued ) ( Relation-like complex-valued ) set ) : ( ( ) ( ) set ) -> complex-membered ;
end;

registration
let R be ( ( Relation-like ext-real-valued ) ( Relation-like ext-real-valued ) Relation) ;
cluster rng R : ( ( Relation-like ext-real-valued ) ( Relation-like ext-real-valued ) set ) : ( ( ) ( ) set ) -> ext-real-membered ;
end;

registration
let R be ( ( Relation-like real-valued ) ( Relation-like complex-valued ext-real-valued real-valued ) Relation) ;
cluster rng R : ( ( Relation-like real-valued ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( complex-membered ext-real-membered ) set ) -> real-membered ;
end;

registration
let R be ( ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued ) ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued ) Relation) ;
cluster rng R : ( ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued ) ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( complex-membered ext-real-membered real-membered ) set ) -> rational-membered ;
end;

registration
let R be ( ( Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued ) ( Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued ) Relation) ;
cluster rng R : ( ( Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued ) ( Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( complex-membered ext-real-membered real-membered ) set ) -> integer-membered ;
end;

registration
let R be ( ( Relation-like natural-valued ) ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) Relation) ;
cluster rng R : ( ( Relation-like natural-valued ) ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered ) set ) -> natural-membered ;
end;

theorem :: VALUED_0:1
for R being ( ( Relation-like ) ( Relation-like ) Relation)
for S being ( ( Relation-like complex-valued ) ( Relation-like complex-valued ) Relation) st R : ( ( Relation-like ) ( Relation-like ) Relation) c= S : ( ( Relation-like complex-valued ) ( Relation-like complex-valued ) Relation) holds
R : ( ( Relation-like ) ( Relation-like ) Relation) is complex-valued ;

theorem :: VALUED_0:2
for R being ( ( Relation-like ) ( Relation-like ) Relation)
for S being ( ( Relation-like ext-real-valued ) ( Relation-like ext-real-valued ) Relation) st R : ( ( Relation-like ) ( Relation-like ) Relation) c= S : ( ( Relation-like ext-real-valued ) ( Relation-like ext-real-valued ) Relation) holds
R : ( ( Relation-like ) ( Relation-like ) Relation) is ext-real-valued ;

theorem :: VALUED_0:3
for R being ( ( Relation-like ) ( Relation-like ) Relation)
for S being ( ( Relation-like real-valued ) ( Relation-like complex-valued ext-real-valued real-valued ) Relation) st R : ( ( Relation-like ) ( Relation-like ) Relation) c= S : ( ( Relation-like real-valued ) ( Relation-like complex-valued ext-real-valued real-valued ) Relation) holds
R : ( ( Relation-like ) ( Relation-like ) Relation) is real-valued ;

theorem :: VALUED_0:4
for R being ( ( Relation-like ) ( Relation-like ) Relation)
for S being ( ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued ) ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued ) Relation) st R : ( ( Relation-like ) ( Relation-like ) Relation) c= S : ( ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued ) ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued ) Relation) holds
R : ( ( Relation-like ) ( Relation-like ) Relation) is RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued ;

theorem :: VALUED_0:5
for R being ( ( Relation-like ) ( Relation-like ) Relation)
for S being ( ( Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued ) ( Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued ) Relation) st R : ( ( Relation-like ) ( Relation-like ) Relation) c= S : ( ( Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued ) ( Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued ) Relation) holds
R : ( ( Relation-like ) ( Relation-like ) Relation) is INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued ;

theorem :: VALUED_0:6
for R being ( ( Relation-like ) ( Relation-like ) Relation)
for S being ( ( Relation-like natural-valued ) ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) Relation) st R : ( ( Relation-like ) ( Relation-like ) Relation) c= S : ( ( Relation-like natural-valued ) ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) Relation) holds
R : ( ( Relation-like ) ( Relation-like ) Relation) is natural-valued ;

registration
let R be ( ( Relation-like complex-valued ) ( Relation-like complex-valued ) Relation) ;
cluster -> complex-valued for ( ( ) ( ) Element of bool R : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

registration
let R be ( ( Relation-like ext-real-valued ) ( Relation-like ext-real-valued ) Relation) ;
cluster -> ext-real-valued for ( ( ) ( ) Element of bool R : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

registration
let R be ( ( Relation-like real-valued ) ( Relation-like complex-valued ext-real-valued real-valued ) Relation) ;
cluster -> real-valued for ( ( ) ( ) Element of bool R : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

registration
let R be ( ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued ) ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued ) Relation) ;
cluster -> RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued for ( ( ) ( ) Element of bool R : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

registration
let R be ( ( Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued ) ( Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued ) Relation) ;
cluster -> INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued for ( ( ) ( ) Element of bool R : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

registration
let R be ( ( Relation-like natural-valued ) ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) Relation) ;
cluster -> natural-valued for ( ( ) ( ) Element of bool R : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

registration
let R, S be ( ( Relation-like complex-valued ) ( Relation-like complex-valued ) Relation) ;
cluster R : ( ( Relation-like complex-valued ) ( Relation-like complex-valued ) set ) \/ S : ( ( Relation-like complex-valued ) ( Relation-like complex-valued ) set ) : ( ( ) ( Relation-like ) set ) -> complex-valued ;
end;

registration
let R, S be ( ( Relation-like ext-real-valued ) ( Relation-like ext-real-valued ) Relation) ;
cluster R : ( ( Relation-like ext-real-valued ) ( Relation-like ext-real-valued ) set ) \/ S : ( ( Relation-like ext-real-valued ) ( Relation-like ext-real-valued ) set ) : ( ( ) ( Relation-like ) set ) -> ext-real-valued ;
end;

registration
let R, S be ( ( Relation-like real-valued ) ( Relation-like complex-valued ext-real-valued real-valued ) Relation) ;
cluster R : ( ( Relation-like real-valued ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) \/ S : ( ( Relation-like real-valued ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( Relation-like complex-valued ext-real-valued ) set ) -> real-valued ;
end;

registration
let R, S be ( ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued ) ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued ) Relation) ;
cluster R : ( ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued ) ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued ) set ) \/ S : ( ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued ) ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued ) set ) -> RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued ;
end;

registration
let R, S be ( ( Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued ) ( Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued ) Relation) ;
cluster R : ( ( Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued ) ( Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued ) set ) \/ S : ( ( Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued ) ( Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued ) set ) -> INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued ;
end;

registration
let R, S be ( ( Relation-like natural-valued ) ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) Relation) ;
cluster R : ( ( Relation-like natural-valued ) ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) \/ S : ( ( Relation-like natural-valued ) ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) : ( ( ) ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued ) set ) -> natural-valued ;
end;

registration
let R be ( ( Relation-like complex-valued ) ( Relation-like complex-valued ) Relation) ;
let S be ( ( Relation-like ) ( Relation-like ) Relation) ;
cluster R : ( ( Relation-like complex-valued ) ( Relation-like complex-valued ) set ) /\ S : ( ( Relation-like ) ( Relation-like ) set ) : ( ( ) ( Relation-like ) set ) -> complex-valued ;
cluster R : ( ( Relation-like complex-valued ) ( Relation-like complex-valued ) set ) \ S : ( ( Relation-like ) ( Relation-like ) set ) : ( ( ) ( Relation-like ) set ) -> complex-valued ;
end;

registration
let R be ( ( Relation-like ext-real-valued ) ( Relation-like ext-real-valued ) Relation) ;
let S be ( ( Relation-like ) ( Relation-like ) Relation) ;
cluster R : ( ( Relation-like ext-real-valued ) ( Relation-like ext-real-valued ) set ) /\ S : ( ( Relation-like ) ( Relation-like ) set ) : ( ( ) ( Relation-like ) set ) -> ext-real-valued ;
cluster R : ( ( Relation-like ext-real-valued ) ( Relation-like ext-real-valued ) set ) \ S : ( ( Relation-like ) ( Relation-like ) set ) : ( ( ) ( Relation-like ) set ) -> ext-real-valued ;
end;

registration
let R be ( ( Relation-like real-valued ) ( Relation-like complex-valued ext-real-valued real-valued ) Relation) ;
let S be ( ( Relation-like ) ( Relation-like ) Relation) ;
cluster R : ( ( Relation-like real-valued ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) /\ S : ( ( Relation-like ) ( Relation-like ) set ) : ( ( ) ( Relation-like complex-valued ext-real-valued ) set ) -> real-valued ;
cluster R : ( ( Relation-like real-valued ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) \ S : ( ( Relation-like ) ( Relation-like ) set ) : ( ( ) ( Relation-like complex-valued ext-real-valued ) set ) -> real-valued ;
end;

registration
let R be ( ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued ) ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued ) Relation) ;
let S be ( ( Relation-like ) ( Relation-like ) Relation) ;
cluster R : ( ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued ) ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued ) set ) /\ S : ( ( Relation-like ) ( Relation-like ) set ) : ( ( ) ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued ) set ) -> RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued ;
cluster R : ( ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued ) ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued ) set ) \ S : ( ( Relation-like ) ( Relation-like ) set ) : ( ( ) ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued ) set ) -> RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued ;
end;

registration
let R be ( ( Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued ) ( Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued ) Relation) ;
let S be ( ( Relation-like ) ( Relation-like ) Relation) ;
cluster R : ( ( Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued ) ( Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued ) set ) /\ S : ( ( Relation-like ) ( Relation-like ) set ) : ( ( ) ( Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued ) set ) -> INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued ;
cluster R : ( ( Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued ) ( Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued ) set ) \ S : ( ( Relation-like ) ( Relation-like ) set ) : ( ( ) ( Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued ) set ) -> INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued ;
end;

registration
let R be ( ( Relation-like natural-valued ) ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) Relation) ;
let S be ( ( Relation-like ) ( Relation-like ) Relation) ;
cluster R : ( ( Relation-like natural-valued ) ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) /\ S : ( ( Relation-like ) ( Relation-like ) set ) : ( ( ) ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued ) set ) -> natural-valued ;
cluster R : ( ( Relation-like natural-valued ) ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) \ S : ( ( Relation-like ) ( Relation-like ) set ) : ( ( ) ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued ) set ) -> natural-valued ;
end;

registration
let R, S be ( ( Relation-like complex-valued ) ( Relation-like complex-valued ) Relation) ;
cluster R : ( ( Relation-like complex-valued ) ( Relation-like complex-valued ) set ) \+\ S : ( ( Relation-like complex-valued ) ( Relation-like complex-valued ) set ) : ( ( ) ( Relation-like ) set ) -> complex-valued ;
end;

registration
let R, S be ( ( Relation-like ext-real-valued ) ( Relation-like ext-real-valued ) Relation) ;
cluster R : ( ( Relation-like ext-real-valued ) ( Relation-like ext-real-valued ) set ) \+\ S : ( ( Relation-like ext-real-valued ) ( Relation-like ext-real-valued ) set ) : ( ( ) ( Relation-like ) set ) -> ext-real-valued ;
end;

registration
let R, S be ( ( Relation-like real-valued ) ( Relation-like complex-valued ext-real-valued real-valued ) Relation) ;
cluster R : ( ( Relation-like real-valued ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) \+\ S : ( ( Relation-like real-valued ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( Relation-like complex-valued ext-real-valued ) set ) -> real-valued ;
end;

registration
let R, S be ( ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued ) ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued ) Relation) ;
cluster R : ( ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued ) ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued ) set ) \+\ S : ( ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued ) ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) -> RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued ;
end;

registration
let R, S be ( ( Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued ) ( Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued ) Relation) ;
cluster R : ( ( Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued ) ( Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued ) set ) \+\ S : ( ( Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued ) ( Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) -> INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued ;
end;

registration
let R, S be ( ( Relation-like natural-valued ) ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) Relation) ;
cluster R : ( ( Relation-like natural-valued ) ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) \+\ S : ( ( Relation-like natural-valued ) ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) : ( ( ) ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued ) set ) -> natural-valued ;
end;

registration
let R be ( ( Relation-like complex-valued ) ( Relation-like complex-valued ) Relation) ;
let X be ( ( ) ( ) set ) ;
cluster R : ( ( Relation-like complex-valued ) ( Relation-like complex-valued ) set ) .: X : ( ( ) ( ) set ) : ( ( ) ( ) set ) -> complex-membered ;
end;

registration
let R be ( ( Relation-like ext-real-valued ) ( Relation-like ext-real-valued ) Relation) ;
let X be ( ( ) ( ) set ) ;
cluster R : ( ( Relation-like ext-real-valued ) ( Relation-like ext-real-valued ) set ) .: X : ( ( ) ( ) set ) : ( ( ) ( ) set ) -> ext-real-membered ;
end;

registration
let R be ( ( Relation-like real-valued ) ( Relation-like complex-valued ext-real-valued real-valued ) Relation) ;
let X be ( ( ) ( ) set ) ;
cluster R : ( ( Relation-like real-valued ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) .: X : ( ( ) ( ) set ) : ( ( ) ( complex-membered ext-real-membered ) set ) -> real-membered ;
end;

registration
let R be ( ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued ) ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued ) Relation) ;
let X be ( ( ) ( ) set ) ;
cluster R : ( ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued ) ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued ) set ) .: X : ( ( ) ( ) set ) : ( ( ) ( complex-membered ext-real-membered real-membered ) set ) -> rational-membered ;
end;

registration
let R be ( ( Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued ) ( Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued ) Relation) ;
let X be ( ( ) ( ) set ) ;
cluster R : ( ( Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued ) ( Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued ) set ) .: X : ( ( ) ( ) set ) : ( ( ) ( complex-membered ext-real-membered real-membered ) set ) -> integer-membered ;
end;

registration
let R be ( ( Relation-like natural-valued ) ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) Relation) ;
let X be ( ( ) ( ) set ) ;
cluster R : ( ( Relation-like natural-valued ) ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) .: X : ( ( ) ( ) set ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered ) set ) -> natural-membered ;
end;

registration
let R be ( ( Relation-like complex-valued ) ( Relation-like complex-valued ) Relation) ;
let x be ( ( ) ( ) set ) ;
cluster Im (R : ( ( Relation-like complex-valued ) ( Relation-like complex-valued ) set ) ,x : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) -> complex-membered ;
end;

registration
let R be ( ( Relation-like ext-real-valued ) ( Relation-like ext-real-valued ) Relation) ;
let x be ( ( ) ( ) set ) ;
cluster Im (R : ( ( Relation-like ext-real-valued ) ( Relation-like ext-real-valued ) set ) ,x : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) -> ext-real-membered ;
end;

registration
let R be ( ( Relation-like real-valued ) ( Relation-like complex-valued ext-real-valued real-valued ) Relation) ;
let x be ( ( ) ( ) set ) ;
cluster Im (R : ( ( Relation-like real-valued ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ,x : ( ( ) ( ) set ) ) : ( ( ) ( complex-membered ext-real-membered ) set ) -> real-membered ;
end;

registration
let R be ( ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued ) ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued ) Relation) ;
let x be ( ( ) ( ) set ) ;
cluster Im (R : ( ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued ) ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued ) set ) ,x : ( ( ) ( ) set ) ) : ( ( ) ( complex-membered ext-real-membered real-membered ) set ) -> rational-membered ;
end;

registration
let R be ( ( Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued ) ( Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued ) Relation) ;
let x be ( ( ) ( ) set ) ;
cluster Im (R : ( ( Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued ) ( Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued ) set ) ,x : ( ( ) ( ) set ) ) : ( ( ) ( complex-membered ext-real-membered real-membered ) set ) -> integer-membered ;
end;

registration
let R be ( ( Relation-like natural-valued ) ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) Relation) ;
let x be ( ( ) ( ) set ) ;
cluster Im (R : ( ( Relation-like natural-valued ) ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) ,x : ( ( ) ( ) set ) ) : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered ) set ) -> natural-membered ;
end;

registration
let R be ( ( Relation-like complex-valued ) ( Relation-like complex-valued ) Relation) ;
let X be ( ( ) ( ) set ) ;
cluster R : ( ( Relation-like complex-valued ) ( Relation-like complex-valued ) set ) | X : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like ) set ) -> Relation-like complex-valued ;
end;

registration
let R be ( ( Relation-like ext-real-valued ) ( Relation-like ext-real-valued ) Relation) ;
let X be ( ( ) ( ) set ) ;
cluster R : ( ( Relation-like ext-real-valued ) ( Relation-like ext-real-valued ) set ) | X : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like ) set ) -> Relation-like ext-real-valued ;
end;

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

registration
let R be ( ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued ) ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued ) Relation) ;
let X be ( ( ) ( ) set ) ;
cluster R : ( ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued ) ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued ) set ) | X : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued ) set ) -> Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued ;
end;

registration
let R be ( ( Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued ) ( Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued ) Relation) ;
let X be ( ( ) ( ) set ) ;
cluster R : ( ( Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued ) ( Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued ) set ) | X : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued ) set ) -> Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued ;
end;

registration
let R be ( ( Relation-like natural-valued ) ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) Relation) ;
let X be ( ( ) ( ) set ) ;
cluster R : ( ( Relation-like natural-valued ) ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) | X : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued ) set ) -> Relation-like natural-valued ;
end;

registration
let X be ( ( complex-membered ) ( complex-membered ) set ) ;
cluster id X : ( ( complex-membered ) ( complex-membered ) set ) : ( ( Relation-like ) ( Relation-like X : ( ( complex-membered ) ( complex-membered ) set ) -defined X : ( ( complex-membered ) ( complex-membered ) set ) -valued Function-like one-to-one total ) set ) -> Relation-like complex-valued ;
end;

registration
let X be ( ( ext-real-membered ) ( ext-real-membered ) set ) ;
cluster id X : ( ( ext-real-membered ) ( ext-real-membered ) set ) : ( ( Relation-like ) ( Relation-like X : ( ( ext-real-membered ) ( ext-real-membered ) set ) -defined X : ( ( ext-real-membered ) ( ext-real-membered ) set ) -valued Function-like one-to-one total ) set ) -> Relation-like ext-real-valued ;
end;

registration
let X be ( ( real-membered ) ( complex-membered ext-real-membered real-membered ) set ) ;
cluster id X : ( ( real-membered ) ( complex-membered ext-real-membered real-membered ) set ) : ( ( Relation-like ) ( Relation-like X : ( ( real-membered ) ( complex-membered ext-real-membered real-membered ) set ) -defined X : ( ( real-membered ) ( complex-membered ext-real-membered real-membered ) set ) -valued Function-like one-to-one total complex-valued ext-real-valued ) set ) -> Relation-like real-valued ;
end;

registration
let X be ( ( rational-membered ) ( complex-membered ext-real-membered real-membered rational-membered ) set ) ;
cluster id X : ( ( rational-membered ) ( complex-membered ext-real-membered real-membered rational-membered ) set ) : ( ( Relation-like ) ( Relation-like X : ( ( rational-membered ) ( complex-membered ext-real-membered real-membered rational-membered ) set ) -defined X : ( ( rational-membered ) ( complex-membered ext-real-membered real-membered rational-membered ) set ) -valued Function-like one-to-one total complex-valued ext-real-valued real-valued ) set ) -> Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued ;
end;

registration
let X be ( ( integer-membered ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ;
cluster id X : ( ( integer-membered ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) : ( ( Relation-like ) ( Relation-like X : ( ( integer-membered ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) -defined X : ( ( integer-membered ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) -valued RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued Function-like one-to-one total complex-valued ext-real-valued real-valued ) set ) -> Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued ;
end;

registration
let X be ( ( natural-membered ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ;
cluster id X : ( ( natural-membered ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) : ( ( Relation-like ) ( Relation-like X : ( ( natural-membered ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) -defined X : ( ( natural-membered ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) -valued RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued Function-like one-to-one total complex-valued ext-real-valued real-valued ) set ) -> Relation-like natural-valued ;
end;

registration
let R be ( ( Relation-like ) ( Relation-like ) Relation) ;
let S be ( ( Relation-like complex-valued ) ( Relation-like complex-valued ) Relation) ;
cluster R : ( ( Relation-like ) ( Relation-like ) set ) * S : ( ( Relation-like complex-valued ) ( Relation-like complex-valued ) set ) : ( ( Relation-like ) ( Relation-like ) set ) -> Relation-like complex-valued ;
end;

registration
let R be ( ( Relation-like ) ( Relation-like ) Relation) ;
let S be ( ( Relation-like ext-real-valued ) ( Relation-like ext-real-valued ) Relation) ;
cluster R : ( ( Relation-like ) ( Relation-like ) set ) * S : ( ( Relation-like ext-real-valued ) ( Relation-like ext-real-valued ) set ) : ( ( Relation-like ) ( Relation-like ) set ) -> Relation-like ext-real-valued ;
end;

registration
let R be ( ( Relation-like ) ( Relation-like ) Relation) ;
let S be ( ( Relation-like real-valued ) ( Relation-like complex-valued ext-real-valued real-valued ) Relation) ;
cluster R : ( ( Relation-like ) ( Relation-like ) set ) * S : ( ( Relation-like real-valued ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) : ( ( Relation-like ) ( Relation-like complex-valued ext-real-valued ) set ) -> Relation-like real-valued ;
end;

registration
let R be ( ( Relation-like ) ( Relation-like ) Relation) ;
let S be ( ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued ) ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued ) Relation) ;
cluster R : ( ( Relation-like ) ( Relation-like ) set ) * S : ( ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued ) ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued ) set ) : ( ( Relation-like ) ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued ) set ) -> Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued ;
end;

registration
let R be ( ( Relation-like ) ( Relation-like ) Relation) ;
let S be ( ( Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued ) ( Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued ) Relation) ;
cluster R : ( ( Relation-like ) ( Relation-like ) set ) * S : ( ( Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued ) ( Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued ) set ) : ( ( Relation-like ) ( Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued ) set ) -> Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued ;
end;

registration
let R be ( ( Relation-like ) ( Relation-like ) Relation) ;
let S be ( ( Relation-like natural-valued ) ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) Relation) ;
cluster R : ( ( Relation-like ) ( Relation-like ) set ) * S : ( ( Relation-like natural-valued ) ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) : ( ( Relation-like ) ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued ) set ) -> Relation-like natural-valued ;
end;

definition
let f be ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ;
redefine attr f is complex-valued means :: VALUED_0:def 7
 for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in dom f : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) holds
f : ( ( non empty ) ( non empty ) set ) . x : ( ( ) ( ) set ) : ( ( ) ( ) set ) is complex ;
redefine attr f is ext-real-valued means :: VALUED_0:def 8
 for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in dom f : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) holds
f : ( ( non empty ) ( non empty ) set ) . x : ( ( ) ( ) set ) : ( ( ) ( ) set ) is ext-real ;
redefine attr f is real-valued means :: VALUED_0:def 9
 for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in dom f : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) holds
f : ( ( non empty ) ( non empty ) set ) . x : ( ( ) ( ) set ) : ( ( ) ( ) set ) is real ;
canceled;
canceled;
redefine attr f is natural-valued means :: VALUED_0:def 12
 for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in dom f : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) holds
f : ( ( non empty ) ( non empty ) set ) . x : ( ( ) ( ) set ) : ( ( ) ( ) set ) is natural ;
end;

theorem :: VALUED_0:7
for f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) holds
( f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) is complex-valued iff for x being ( ( ) ( ) set ) holds f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . x : ( ( ) ( ) set ) : ( ( ) ( ) set ) is complex ) ;

theorem :: VALUED_0:8
for f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) holds
( f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) is ext-real-valued iff for x being ( ( ) ( ) set ) holds f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . x : ( ( ) ( ) set ) : ( ( ) ( ) set ) is ext-real ) ;

theorem :: VALUED_0:9
for f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) holds
( f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) is real-valued iff for x being ( ( ) ( ) set ) holds f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . x : ( ( ) ( ) set ) : ( ( ) ( ) set ) is real ) ;

theorem :: VALUED_0:10
for f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) holds
( f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) is RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued iff for x being ( ( ) ( ) set ) holds f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . x : ( ( ) ( ) set ) : ( ( ) ( ) set ) is rational ) ;

theorem :: VALUED_0:11
for f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) holds
( f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) is INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued iff for x being ( ( ) ( ) set ) holds f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . x : ( ( ) ( ) set ) : ( ( ) ( ) set ) is integer ) ;

theorem :: VALUED_0:12
for f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) holds
( f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) is natural-valued iff for x being ( ( ) ( ) set ) holds f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . x : ( ( ) ( ) set ) : ( ( ) ( ) set ) is natural ) ;

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

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

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

registration
let f be ( ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued Function-like ) ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Function) ;
let x be ( ( ) ( ) set ) ;
cluster f : ( ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued Function-like ) ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) set ) . x : ( ( ) ( ) set ) : ( ( ) ( complex real ext-real ) set ) -> rational ;
end;

registration
let f be ( ( Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued Function-like ) ( Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Function) ;
let x be ( ( ) ( ) set ) ;
cluster f : ( ( Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued Function-like ) ( Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) set ) . x : ( ( ) ( ) set ) : ( ( ) ( complex real ext-real ) set ) -> integer ;
end;

registration
let f be ( ( Relation-like Function-like natural-valued ) ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued Function-like complex-valued ext-real-valued real-valued natural-valued ) Function) ;
let x be ( ( ) ( ) set ) ;
cluster f : ( ( Relation-like Function-like natural-valued ) ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued Function-like complex-valued ext-real-valued real-valued natural-valued ) set ) . x : ( ( ) ( ) set ) : ( ( ) ( complex real rational ext-real ) set ) -> natural ;
end;

registration
let X be ( ( ) ( ) set ) ;
let x be ( ( complex ) ( complex ) number ) ;
cluster X : ( ( ) ( ) set ) --> x : ( ( complex ) ( complex ) set ) : ( ( ) ( Relation-like X : ( ( ) ( ) set ) -defined Function-like constant total ) set ) -> complex-valued ;
end;

registration
let X be ( ( ) ( ) set ) ;
let x be ( ( ext-real ) ( ext-real ) number ) ;
cluster X : ( ( ) ( ) set ) --> x : ( ( ext-real ) ( ext-real ) set ) : ( ( ) ( Relation-like X : ( ( ) ( ) set ) -defined Function-like constant total ) set ) -> ext-real-valued ;
end;

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

registration
let X be ( ( ) ( ) set ) ;
let x be ( ( rational ) ( complex real rational ext-real ) number ) ;
cluster X : ( ( ) ( ) set ) --> x : ( ( rational ) ( complex real rational ext-real ) set ) : ( ( ) ( Relation-like X : ( ( ) ( ) set ) -defined Function-like constant total complex-valued ext-real-valued real-valued ) set ) -> RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued ;
end;

registration
let X be ( ( ) ( ) set ) ;
let x be ( ( integer ) ( complex real integer rational ext-real ) number ) ;
cluster X : ( ( ) ( ) set ) --> x : ( ( integer ) ( complex real integer rational ext-real ) set ) : ( ( ) ( Relation-like X : ( ( ) ( ) set ) -defined RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued Function-like constant total complex-valued ext-real-valued real-valued ) set ) -> INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued ;
end;

registration
let X be ( ( ) ( ) set ) ;
let x be ( ( natural ) ( complex epsilon-transitive epsilon-connected ordinal natural real integer rational ext-real ) Nat) ;
cluster X : ( ( ) ( ) set ) --> x : ( ( natural ) ( complex epsilon-transitive epsilon-connected ordinal natural real integer rational ext-real ) set ) : ( ( ) ( Relation-like X : ( ( ) ( ) set ) -defined RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued Function-like constant total complex-valued ext-real-valued real-valued ) set ) -> natural-valued ;
end;

registration
let f, g 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 ) +* g : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ) set ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) -> Relation-like Function-like complex-valued ;
end;

registration
let f, g be ( ( Relation-like Function-like ext-real-valued ) ( Relation-like Function-like ext-real-valued ) Function) ;
cluster f : ( ( Relation-like Function-like ext-real-valued ) ( Relation-like Function-like ext-real-valued ) set ) +* g : ( ( Relation-like Function-like ext-real-valued ) ( Relation-like Function-like ext-real-valued ) set ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) -> Relation-like Function-like ext-real-valued ;
end;

registration
let f, g 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 ) +* g : ( ( 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 ) set ) -> Relation-like Function-like real-valued ;
end;

registration
let f, g be ( ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued Function-like ) ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Function) ;
cluster f : ( ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued Function-like ) ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) set ) +* g : ( ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued Function-like ) ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued 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 ) -> Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued Function-like ;
end;

registration
let f, g be ( ( Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued Function-like ) ( Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) Function) ;
cluster f : ( ( Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued Function-like ) ( Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) set ) +* g : ( ( Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued Function-like ) ( Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued 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 ) -> Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued Function-like ;
end;

registration
let f, g be ( ( Relation-like Function-like natural-valued ) ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued Function-like complex-valued ext-real-valued real-valued natural-valued ) Function) ;
cluster f : ( ( Relation-like Function-like natural-valued ) ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued Function-like complex-valued ext-real-valued real-valued natural-valued ) set ) +* g : ( ( Relation-like Function-like natural-valued ) ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued Function-like complex-valued ext-real-valued real-valued natural-valued ) set ) : ( ( Relation-like Function-like ) ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) set ) -> Relation-like Function-like natural-valued ;
end;

registration
let x be ( ( ) ( ) set ) ;
let y be ( ( complex ) ( complex ) number ) ;
cluster x : ( ( ) ( ) set ) .--> y : ( ( complex ) ( complex ) set ) : ( ( ) ( Relation-like {x : ( ( ) ( ) set ) } : ( ( ) ( non empty trivial ) set ) -defined Function-like one-to-one ) set ) -> complex-valued ;
end;

registration
let x be ( ( ) ( ) set ) ;
let y be ( ( ext-real ) ( ext-real ) number ) ;
cluster x : ( ( ) ( ) set ) .--> y : ( ( ext-real ) ( ext-real ) set ) : ( ( ) ( Relation-like {x : ( ( ) ( ) set ) } : ( ( ) ( non empty trivial ) set ) -defined Function-like one-to-one ) set ) -> ext-real-valued ;
end;

registration
let x be ( ( ) ( ) set ) ;
let y be ( ( real ) ( complex real ext-real ) number ) ;
cluster x : ( ( ) ( ) set ) .--> y : ( ( real ) ( complex real ext-real ) set ) : ( ( ) ( Relation-like {x : ( ( ) ( ) set ) } : ( ( ) ( non empty trivial ) set ) -defined Function-like one-to-one complex-valued ext-real-valued ) set ) -> real-valued ;
end;

registration
let x be ( ( ) ( ) set ) ;
let y be ( ( rational ) ( complex real rational ext-real ) number ) ;
cluster x : ( ( ) ( ) set ) .--> y : ( ( rational ) ( complex real rational ext-real ) set ) : ( ( ) ( Relation-like {x : ( ( ) ( ) set ) } : ( ( ) ( non empty trivial ) set ) -defined Function-like one-to-one complex-valued ext-real-valued real-valued ) set ) -> RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued ;
end;

registration
let x be ( ( ) ( ) set ) ;
let y be ( ( integer ) ( complex real integer rational ext-real ) number ) ;
cluster x : ( ( ) ( ) set ) .--> y : ( ( integer ) ( complex real integer rational ext-real ) set ) : ( ( ) ( Relation-like {x : ( ( ) ( ) set ) } : ( ( ) ( non empty trivial ) set ) -defined RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued Function-like one-to-one complex-valued ext-real-valued real-valued ) set ) -> INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued ;
end;

registration
let x be ( ( ) ( ) set ) ;
let y be ( ( natural ) ( complex epsilon-transitive epsilon-connected ordinal natural real integer rational ext-real ) Nat) ;
cluster x : ( ( ) ( ) set ) .--> y : ( ( natural ) ( complex epsilon-transitive epsilon-connected ordinal natural real integer rational ext-real ) set ) : ( ( ) ( Relation-like {x : ( ( ) ( ) set ) } : ( ( ) ( non empty trivial ) set ) -defined RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued Function-like one-to-one complex-valued ext-real-valued real-valued ) set ) -> natural-valued ;
end;

registration
let X be ( ( ) ( ) set ) ;
let Y be ( ( complex-membered ) ( complex-membered ) set ) ;
cluster -> complex-valued for ( ( ) ( ) Element of bool [:X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

registration
let X be ( ( ) ( ) set ) ;
let Y be ( ( ext-real-membered ) ( ext-real-membered ) set ) ;
cluster -> ext-real-valued for ( ( ) ( ) Element of bool [:X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

registration
let X be ( ( ) ( ) set ) ;
let Y be ( ( real-membered ) ( complex-membered ext-real-membered real-membered ) set ) ;
cluster -> real-valued for ( ( ) ( ) Element of bool [:X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

registration
let X be ( ( ) ( ) set ) ;
let Y be ( ( rational-membered ) ( complex-membered ext-real-membered real-membered rational-membered ) set ) ;
cluster -> RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued for ( ( ) ( ) Element of bool [:X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

registration
let X be ( ( ) ( ) set ) ;
let Y be ( ( integer-membered ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ;
cluster -> INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued for ( ( ) ( ) Element of bool [:X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

registration
let X be ( ( ) ( ) set ) ;
let Y be ( ( natural-membered ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ;
cluster -> natural-valued for ( ( ) ( ) Element of bool [:X : ( ( non empty ) ( non empty ) set ) ,Y : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

registration
let X be ( ( ) ( ) set ) ;
let Y be ( ( complex-membered ) ( complex-membered ) set ) ;
cluster [:X : ( ( ) ( ) set ) ,Y : ( ( complex-membered ) ( complex-membered ) set ) :] : ( ( ) ( Relation-like ) set ) -> complex-valued ;
end;

registration
let X be ( ( ) ( ) set ) ;
let Y be ( ( ext-real-membered ) ( ext-real-membered ) set ) ;
cluster [:X : ( ( ) ( ) set ) ,Y : ( ( ext-real-membered ) ( ext-real-membered ) set ) :] : ( ( ) ( Relation-like ) set ) -> ext-real-valued ;
end;

registration
let X be ( ( ) ( ) set ) ;
let Y be ( ( real-membered ) ( complex-membered ext-real-membered real-membered ) set ) ;
cluster [:X : ( ( ) ( ) set ) ,Y : ( ( real-membered ) ( complex-membered ext-real-membered real-membered ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued ) set ) -> real-valued ;
end;

registration
let X be ( ( ) ( ) set ) ;
let Y be ( ( rational-membered ) ( complex-membered ext-real-membered real-membered rational-membered ) set ) ;
cluster [:X : ( ( ) ( ) set ) ,Y : ( ( rational-membered ) ( complex-membered ext-real-membered real-membered rational-membered ) set ) :] : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) -> RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued ;
end;

registration
let X be ( ( ) ( ) set ) ;
let Y be ( ( integer-membered ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) ;
cluster [:X : ( ( ) ( ) set ) ,Y : ( ( integer-membered ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered ) set ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued ) set ) -> INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued ;
end;

registration
let X be ( ( ) ( ) set ) ;
let Y be ( ( natural-membered ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) ;
cluster [:X : ( ( ) ( ) set ) ,Y : ( ( natural-membered ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ) set ) :] : ( ( ) ( Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued ) set ) -> natural-valued ;
end;

notation
let f be ( ( Relation-like ext-real-valued ) ( Relation-like ext-real-valued ) Relation) ;
synonym non-zero f for non-empty ;
end;

registration
cluster non empty Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued Function-like constant natural-valued for ( ( ) ( ) set ) ;
end;

theorem :: VALUED_0:13
for f being ( ( non empty Relation-like Function-like constant complex-valued ) ( non empty Relation-like Function-like constant complex-valued ) Function) ex r being ( ( complex ) ( complex ) number ) st
for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in dom f : ( ( non empty Relation-like Function-like constant complex-valued ) ( non empty Relation-like Function-like constant complex-valued ) Function) : ( ( ) ( non empty ) set ) holds
f : ( ( non empty Relation-like Function-like constant complex-valued ) ( non empty Relation-like Function-like constant complex-valued ) Function) . x : ( ( ) ( ) set ) : ( ( ) ( complex ) set ) = r : ( ( complex ) ( complex ) number ) ;

theorem :: VALUED_0:14
for f being ( ( non empty Relation-like Function-like constant ext-real-valued ) ( non empty Relation-like Function-like constant ext-real-valued ) Function) ex r being ( ( ext-real ) ( ext-real ) number ) st
for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in dom f : ( ( non empty Relation-like Function-like constant ext-real-valued ) ( non empty Relation-like Function-like constant ext-real-valued ) Function) : ( ( ) ( non empty ) set ) holds
f : ( ( non empty Relation-like Function-like constant ext-real-valued ) ( non empty Relation-like Function-like constant ext-real-valued ) Function) . x : ( ( ) ( ) set ) : ( ( ) ( ext-real ) set ) = r : ( ( ext-real ) ( ext-real ) number ) ;

theorem :: VALUED_0:15
for f being ( ( non empty Relation-like Function-like constant real-valued ) ( non empty Relation-like Function-like constant complex-valued ext-real-valued real-valued ) Function) ex r being ( ( real ) ( complex real ext-real ) number ) st
for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in dom f : ( ( non empty Relation-like Function-like constant real-valued ) ( non empty Relation-like Function-like constant complex-valued ext-real-valued real-valued ) Function) : ( ( ) ( non empty ) set ) holds
f : ( ( non empty Relation-like Function-like constant real-valued ) ( non empty Relation-like Function-like constant complex-valued ext-real-valued real-valued ) Function) . x : ( ( ) ( ) set ) : ( ( ) ( complex real ext-real ) set ) = r : ( ( real ) ( complex real ext-real ) number ) ;

theorem :: VALUED_0:16
for f being ( ( non empty Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued Function-like constant ) ( non empty Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued Function-like constant complex-valued ext-real-valued real-valued ) Function) ex r being ( ( rational ) ( complex real rational ext-real ) number ) st
for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in dom f : ( ( non empty Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued Function-like constant ) ( non empty Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued Function-like constant complex-valued ext-real-valued real-valued ) Function) : ( ( ) ( non empty ) set ) holds
f : ( ( non empty Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued Function-like constant ) ( non empty Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued Function-like constant complex-valued ext-real-valued real-valued ) Function) . x : ( ( ) ( ) set ) : ( ( ) ( complex real rational ext-real ) set ) = r : ( ( rational ) ( complex real rational ext-real ) number ) ;

theorem :: VALUED_0:17
for f being ( ( non empty Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued Function-like constant ) ( non empty Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued Function-like constant complex-valued ext-real-valued real-valued ) Function) ex r being ( ( integer ) ( complex real integer rational ext-real ) number ) st
for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in dom f : ( ( non empty Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued Function-like constant ) ( non empty Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued Function-like constant complex-valued ext-real-valued real-valued ) Function) : ( ( ) ( non empty ) set ) holds
f : ( ( non empty Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued Function-like constant ) ( non empty Relation-like INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued Function-like constant complex-valued ext-real-valued real-valued ) Function) . x : ( ( ) ( ) set ) : ( ( ) ( complex real integer rational ext-real ) set ) = r : ( ( integer ) ( complex real integer rational ext-real ) number ) ;

theorem :: VALUED_0:18
for f being ( ( non empty Relation-like Function-like constant natural-valued ) ( non empty Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued Function-like constant complex-valued ext-real-valued real-valued natural-valued ) Function) ex r being ( ( natural ) ( complex epsilon-transitive epsilon-connected ordinal natural real integer rational ext-real ) Nat) st
for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in dom f : ( ( non empty Relation-like Function-like constant natural-valued ) ( non empty Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued Function-like constant complex-valued ext-real-valued real-valued natural-valued ) Function) : ( ( ) ( non empty ) set ) holds
f : ( ( non empty Relation-like Function-like constant natural-valued ) ( non empty Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued Function-like constant complex-valued ext-real-valued real-valued natural-valued ) Function) . x : ( ( ) ( ) set ) : ( ( ) ( complex epsilon-transitive epsilon-connected ordinal natural real integer rational ext-real ) set ) = r : ( ( natural ) ( complex epsilon-transitive epsilon-connected ordinal natural real integer rational ext-real ) Nat) ;

begin

definition
let f be ( ( Relation-like Function-like ext-real-valued ) ( Relation-like Function-like ext-real-valued ) Function) ;
attr f is increasing means :: VALUED_0:def 13
 for e1, e2 being ( ( ext-real ) ( ext-real ) number ) st e1 : ( ( ext-real ) ( ext-real ) number ) in dom f : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) & e2 : ( ( ext-real ) ( ext-real ) number ) in dom f : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) & e1 : ( ( ext-real ) ( ext-real ) number ) < e2 : ( ( ext-real ) ( ext-real ) number ) holds
f : ( ( non empty ) ( non empty ) set ) . e1 : ( ( ext-real ) ( ext-real ) number ) : ( ( ) ( ) set ) < f : ( ( non empty ) ( non empty ) set ) . e2 : ( ( ext-real ) ( ext-real ) number ) : ( ( ) ( ) set ) ;
attr f is decreasing means :: VALUED_0:def 14
 for e1, e2 being ( ( ext-real ) ( ext-real ) number ) st e1 : ( ( ext-real ) ( ext-real ) number ) in dom f : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) & e2 : ( ( ext-real ) ( ext-real ) number ) in dom f : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) & e1 : ( ( ext-real ) ( ext-real ) number ) < e2 : ( ( ext-real ) ( ext-real ) number ) holds
f : ( ( non empty ) ( non empty ) set ) . e1 : ( ( ext-real ) ( ext-real ) number ) : ( ( ) ( ) set ) > f : ( ( non empty ) ( non empty ) set ) . e2 : ( ( ext-real ) ( ext-real ) number ) : ( ( ) ( ) set ) ;
attr f is non-decreasing means :: VALUED_0:def 15
 for e1, e2 being ( ( ext-real ) ( ext-real ) number ) st e1 : ( ( ext-real ) ( ext-real ) number ) in dom f : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) & e2 : ( ( ext-real ) ( ext-real ) number ) in dom f : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) & e1 : ( ( ext-real ) ( ext-real ) number ) <= e2 : ( ( ext-real ) ( ext-real ) number ) holds
f : ( ( non empty ) ( non empty ) set ) . e1 : ( ( ext-real ) ( ext-real ) number ) : ( ( ) ( ) set ) <= f : ( ( non empty ) ( non empty ) set ) . e2 : ( ( ext-real ) ( ext-real ) number ) : ( ( ) ( ) set ) ;
attr f is non-increasing means :: VALUED_0:def 16
 for e1, e2 being ( ( ext-real ) ( ext-real ) number ) st e1 : ( ( ext-real ) ( ext-real ) number ) in dom f : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) & e2 : ( ( ext-real ) ( ext-real ) number ) in dom f : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) & e1 : ( ( ext-real ) ( ext-real ) number ) <= e2 : ( ( ext-real ) ( ext-real ) number ) holds
f : ( ( non empty ) ( non empty ) set ) . e1 : ( ( ext-real ) ( ext-real ) number ) : ( ( ) ( ) set ) >= f : ( ( non empty ) ( non empty ) set ) . e2 : ( ( ext-real ) ( ext-real ) number ) : ( ( ) ( ) set ) ;
end;

registration
cluster trivial Relation-like Function-like ext-real-valued -> Relation-like Function-like ext-real-valued increasing decreasing for ( ( ) ( ) set ) ;
end;

registration
cluster Relation-like Function-like ext-real-valued increasing -> Relation-like Function-like ext-real-valued non-decreasing for ( ( ) ( ) set ) ;
cluster Relation-like Function-like ext-real-valued decreasing -> Relation-like Function-like ext-real-valued non-increasing for ( ( ) ( ) set ) ;
end;

registration
let f, g be ( ( Relation-like Function-like ext-real-valued increasing ) ( Relation-like Function-like ext-real-valued increasing non-decreasing ) Function) ;
cluster f : ( ( Relation-like Function-like ext-real-valued increasing ) ( Relation-like Function-like ext-real-valued increasing non-decreasing ) set ) * g : ( ( Relation-like Function-like ext-real-valued increasing ) ( Relation-like Function-like ext-real-valued increasing non-decreasing ) set ) : ( ( Relation-like ) ( Relation-like Function-like ext-real-valued ) set ) -> Relation-like increasing ;
end;

registration
let f, g be ( ( Relation-like Function-like ext-real-valued non-decreasing ) ( Relation-like Function-like ext-real-valued non-decreasing ) Function) ;
cluster f : ( ( Relation-like Function-like ext-real-valued non-decreasing ) ( Relation-like Function-like ext-real-valued non-decreasing ) set ) * g : ( ( Relation-like Function-like ext-real-valued non-decreasing ) ( Relation-like Function-like ext-real-valued non-decreasing ) set ) : ( ( Relation-like ) ( Relation-like Function-like ext-real-valued ) set ) -> Relation-like non-decreasing ;
end;

registration
let f, g be ( ( Relation-like Function-like ext-real-valued decreasing ) ( Relation-like Function-like ext-real-valued decreasing non-increasing ) Function) ;
cluster f : ( ( Relation-like Function-like ext-real-valued decreasing ) ( Relation-like Function-like ext-real-valued decreasing non-increasing ) set ) * g : ( ( Relation-like Function-like ext-real-valued decreasing ) ( Relation-like Function-like ext-real-valued decreasing non-increasing ) set ) : ( ( Relation-like ) ( Relation-like Function-like ext-real-valued ) set ) -> Relation-like increasing ;
end;

registration
let f, g be ( ( Relation-like Function-like ext-real-valued non-increasing ) ( Relation-like Function-like ext-real-valued non-increasing ) Function) ;
cluster f : ( ( Relation-like Function-like ext-real-valued non-increasing ) ( Relation-like Function-like ext-real-valued non-increasing ) set ) * g : ( ( Relation-like Function-like ext-real-valued non-increasing ) ( Relation-like Function-like ext-real-valued non-increasing ) set ) : ( ( Relation-like ) ( Relation-like Function-like ext-real-valued ) set ) -> Relation-like non-decreasing ;
end;

registration
let f be ( ( Relation-like Function-like ext-real-valued decreasing ) ( Relation-like Function-like ext-real-valued decreasing non-increasing ) Function) ;
let g be ( ( Relation-like Function-like ext-real-valued increasing ) ( Relation-like Function-like ext-real-valued increasing non-decreasing ) Function) ;
cluster f : ( ( Relation-like Function-like ext-real-valued decreasing ) ( Relation-like Function-like ext-real-valued decreasing non-increasing ) set ) * g : ( ( Relation-like Function-like ext-real-valued increasing ) ( Relation-like Function-like ext-real-valued increasing non-decreasing ) set ) : ( ( Relation-like ) ( Relation-like Function-like ext-real-valued ) set ) -> Relation-like decreasing ;
cluster g : ( ( Relation-like Function-like ext-real-valued increasing ) ( Relation-like Function-like ext-real-valued increasing non-decreasing ) set ) * f : ( ( Relation-like Function-like ext-real-valued decreasing ) ( Relation-like Function-like ext-real-valued decreasing non-increasing ) set ) : ( ( Relation-like ) ( Relation-like Function-like ext-real-valued ) set ) -> Relation-like decreasing ;
end;

registration
let f be ( ( Relation-like Function-like ext-real-valued non-increasing ) ( Relation-like Function-like ext-real-valued non-increasing ) Function) ;
let g be ( ( Relation-like Function-like ext-real-valued non-decreasing ) ( Relation-like Function-like ext-real-valued non-decreasing ) Function) ;
cluster f : ( ( Relation-like Function-like ext-real-valued non-increasing ) ( Relation-like Function-like ext-real-valued non-increasing ) set ) * g : ( ( Relation-like Function-like ext-real-valued non-decreasing ) ( Relation-like Function-like ext-real-valued non-decreasing ) set ) : ( ( Relation-like ) ( Relation-like Function-like ext-real-valued ) set ) -> Relation-like non-increasing ;
cluster g : ( ( Relation-like Function-like ext-real-valued non-decreasing ) ( Relation-like Function-like ext-real-valued non-decreasing ) set ) * f : ( ( Relation-like Function-like ext-real-valued non-increasing ) ( Relation-like Function-like ext-real-valued non-increasing ) set ) : ( ( Relation-like ) ( Relation-like Function-like ext-real-valued ) set ) -> Relation-like non-increasing ;
end;

registration
let X be ( ( ext-real-membered ) ( ext-real-membered ) set ) ;
cluster id X : ( ( ext-real-membered ) ( ext-real-membered ) set ) : ( ( Relation-like ) ( Relation-like X : ( ( ext-real-membered ) ( ext-real-membered ) set ) -defined X : ( ( ext-real-membered ) ( ext-real-membered ) set ) -valued Function-like one-to-one total ext-real-valued ) set ) -> Function-like quasi_total increasing for ( ( Function-like quasi_total ) ( Relation-like X : ( ( ext-real-membered ) ( ext-real-membered ) set ) -defined X : ( ( ext-real-membered ) ( ext-real-membered ) set ) -valued Function-like total quasi_total ext-real-valued ) Function of X : ( ( ext-real-membered ) ( ext-real-membered ) set ) ,X : ( ( ext-real-membered ) ( ext-real-membered ) set ) ) ;
end;

registration
cluster non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like total quasi_total complex-valued ext-real-valued real-valued natural-valued increasing for ( ( ) ( ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) ,NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty Relation-like RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued INT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered integer-membered V21() ) set ) -valued complex-valued ext-real-valued real-valued natural-valued ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

definition
let s be ( ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined Function-like total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined Function-like total ) ManySortedSet of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) ) ;
mode subsequence of s -> ( ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined Function-like total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined Function-like total ) ManySortedSet of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) ) means :: VALUED_0:def 17
 ex N being ( ( Function-like quasi_total increasing ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like total quasi_total complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing ) sequence of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) ) st it : ( ( ) ( ) set ) = s : ( ( non empty ) ( non empty ) set ) * N : ( ( Function-like quasi_total increasing ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like total quasi_total complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing ) sequence of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( Relation-like ) ( Relation-like ) set ) ;
end;

registration
let X be ( ( non empty ) ( non empty ) set ) ;
let s be ( ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined X : ( ( non empty ) ( non empty ) set ) -valued Function-like total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined X : ( ( non empty ) ( non empty ) set ) -valued Function-like total ) ManySortedSet of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) ) ;
cluster -> X : ( ( non empty ) ( non empty ) set ) -valued for ( ( ) ( ) subsequence of s : ( ( ) ( ) set ) ) ;
end;

definition
let X be ( ( non empty ) ( non empty ) set ) ;
let s be ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined X : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of X : ( ( non empty ) ( non empty ) set ) ) ;
:: original: subsequence
redefine mode subsequence of s -> ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined X : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of X : ( ( non empty ) ( non empty ) set ) ) ;
end;

definition
let X be ( ( non empty ) ( non empty ) set ) ;
let s be ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined X : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of X : ( ( non empty ) ( non empty ) set ) ) ;
let k be ( ( natural ) ( complex epsilon-transitive epsilon-connected ordinal natural real integer rational ext-real ) Nat) ;
:: original: ^\
redefine func s ^\ k -> ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined X : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) subsequence of s : ( ( ) ( ) set ) ) ;
end;

theorem :: VALUED_0:19
for XX being ( ( non empty ) ( non empty ) set )
for ss being ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of XX : ( ( non empty ) ( non empty ) set ) ) holds ss : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of b1 : ( ( non empty ) ( non empty ) set ) ) is ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) subsequence of ss : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of b1 : ( ( non empty ) ( non empty ) set ) ) ) ;

theorem :: VALUED_0:20
for XX being ( ( non empty ) ( non empty ) set )
for ss1, ss2, ss3 being ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of XX : ( ( non empty ) ( non empty ) set ) ) st ss1 : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of b1 : ( ( non empty ) ( non empty ) set ) ) is ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) subsequence of ss2 : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of b1 : ( ( non empty ) ( non empty ) set ) ) ) & ss2 : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of b1 : ( ( non empty ) ( non empty ) set ) ) is ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) subsequence of ss3 : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of b1 : ( ( non empty ) ( non empty ) set ) ) ) holds
ss1 : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of b1 : ( ( non empty ) ( non empty ) set ) ) is ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) subsequence of ss3 : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of b1 : ( ( non empty ) ( non empty ) set ) ) ) ;

registration
let X be ( ( ) ( ) set ) ;
cluster Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined X : ( ( ) ( ) set ) -valued Function-like constant quasi_total for ( ( ) ( ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) ,X : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

theorem :: VALUED_0:21
for XX being ( ( non empty ) ( non empty ) set )
for ss being ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of XX : ( ( non empty ) ( non empty ) set ) )
for ss1 being ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) subsequence of ss : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of b1 : ( ( non empty ) ( non empty ) set ) ) ) holds rng ss1 : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) subsequence of b2 : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) Element of bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) c= rng ss : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

registration
let X be ( ( non empty ) ( non empty ) set ) ;
let s be ( ( Function-like constant quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined X : ( ( non empty ) ( non empty ) set ) -valued Function-like constant total quasi_total ) sequence of X : ( ( non empty ) ( non empty ) set ) ) ;
cluster -> constant for ( ( ) ( ) subsequence of s : ( ( ) ( ) set ) ) ;
end;

definition
let X be ( ( non empty ) ( non empty ) set ) ;
let N be ( ( Function-like quasi_total increasing ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like total quasi_total complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing ) sequence of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) ) ;
let s be ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined X : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of X : ( ( non empty ) ( non empty ) set ) ) ;
:: original: *
redefine func s * N -> ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined X : ( ( ) ( ) set ) -valued Function-like total quasi_total ) subsequence of s : ( ( natural ) ( complex epsilon-transitive epsilon-connected ordinal natural real integer rational ext-real ) set ) ) ;
end;

theorem :: VALUED_0:22
for X, Y being ( ( non empty ) ( non empty ) set )
for s, s1 being ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of X : ( ( non empty ) ( non empty ) set ) )
for h being ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) st rng s : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) c= dom h : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) : ( ( ) ( ) Element of bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) & s1 : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of b1 : ( ( non empty ) ( non empty ) set ) ) is ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) subsequence of s : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of b1 : ( ( non empty ) ( non empty ) set ) ) ) holds
h : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) /* s1 : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) ,b2 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) is ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) subsequence of h : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) /* s : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) ,b2 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ) ;

registration
let X be ( ( with_non-empty_element ) ( non empty with_non-empty_element ) set ) ;
cluster non empty Relation-like non-empty NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined X : ( ( with_non-empty_element ) ( non empty with_non-empty_element ) set ) -valued Function-like total quasi_total for ( ( ) ( ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) ,X : ( ( with_non-empty_element ) ( non empty with_non-empty_element ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

registration
let X be ( ( with_non-empty_element ) ( non empty with_non-empty_element ) set ) ;
let s be ( ( non-empty Function-like quasi_total ) ( non empty Relation-like non-empty non empty-yielding NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined X : ( ( with_non-empty_element ) ( non empty with_non-empty_element ) set ) -valued Function-like total quasi_total ) sequence of X : ( ( with_non-empty_element ) ( non empty with_non-empty_element ) set ) ) ;
cluster -> non-empty for ( ( ) ( ) subsequence of s : ( ( ) ( ) set ) ) ;
end;

definition
let X be ( ( non empty ) ( non empty ) set ) ;
let s be ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined X : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of X : ( ( non empty ) ( non empty ) set ) ) ;
:: original: constant
redefine attr s is constant means :: VALUED_0:def 18
 ex x being ( ( ) ( ) Element of X : ( ( with_non-empty_element ) ( non empty with_non-empty_element ) set ) ) st
for n being ( ( natural ) ( complex epsilon-transitive epsilon-connected ordinal natural real integer rational ext-real ) Nat) holds s : ( ( ) ( ) set ) . n : ( ( natural ) ( complex epsilon-transitive epsilon-connected ordinal natural real integer rational ext-real ) Nat) : ( ( ) ( ) Element of X : ( ( with_non-empty_element ) ( non empty with_non-empty_element ) set ) ) = x : ( ( ) ( ) Element of X : ( ( non empty ) ( non empty ) set ) ) ;
end;

theorem :: VALUED_0:23
for i, j being ( ( natural ) ( complex epsilon-transitive epsilon-connected ordinal natural real integer rational ext-real ) Nat)
for X being ( ( ) ( ) set )
for s being ( ( Function-like constant quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b3 : ( ( ) ( ) set ) -valued Function-like constant quasi_total ) sequence of X : ( ( ) ( ) set ) ) holds s : ( ( Function-like constant quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b3 : ( ( ) ( ) set ) -valued Function-like constant quasi_total ) sequence of b3 : ( ( ) ( ) set ) ) . i : ( ( natural ) ( complex epsilon-transitive epsilon-connected ordinal natural real integer rational ext-real ) Nat) : ( ( ) ( ) Element of b3 : ( ( ) ( ) set ) ) = s : ( ( Function-like constant quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b3 : ( ( ) ( ) set ) -valued Function-like constant quasi_total ) sequence of b3 : ( ( ) ( ) set ) ) . j : ( ( natural ) ( complex epsilon-transitive epsilon-connected ordinal natural real integer rational ext-real ) Nat) : ( ( ) ( ) Element of b3 : ( ( ) ( ) set ) ) ;

theorem :: VALUED_0:24
for X being ( ( non empty ) ( non empty ) set )
for s being ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of X : ( ( non empty ) ( non empty ) set ) ) st ( for i, j being ( ( natural ) ( complex epsilon-transitive epsilon-connected ordinal natural real integer rational ext-real ) Nat) holds s : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of b1 : ( ( non empty ) ( non empty ) set ) ) . i : ( ( natural ) ( complex epsilon-transitive epsilon-connected ordinal natural real integer rational ext-real ) Nat) : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) = s : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of b1 : ( ( non empty ) ( non empty ) set ) ) . j : ( ( natural ) ( complex epsilon-transitive epsilon-connected ordinal natural real integer rational ext-real ) Nat) : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) holds
s : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of b1 : ( ( non empty ) ( non empty ) set ) ) is V29() ;

theorem :: VALUED_0:25
for X being ( ( non empty ) ( non empty ) set )
for s being ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of X : ( ( non empty ) ( non empty ) set ) ) st ( for i being ( ( natural ) ( complex epsilon-transitive epsilon-connected ordinal natural real integer rational ext-real ) Nat) holds s : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of b1 : ( ( non empty ) ( non empty ) set ) ) . i : ( ( natural ) ( complex epsilon-transitive epsilon-connected ordinal natural real integer rational ext-real ) Nat) : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) = s : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of b1 : ( ( non empty ) ( non empty ) set ) ) . (i : ( ( natural ) ( complex epsilon-transitive epsilon-connected ordinal natural real integer rational ext-real ) Nat) + 1 : ( ( ) ( complex non empty epsilon-transitive epsilon-connected ordinal natural real integer rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ext-real positive ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( complex epsilon-transitive epsilon-connected ordinal natural real integer rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered ext-real ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) holds
s : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of b1 : ( ( non empty ) ( non empty ) set ) ) is V29() ;

theorem :: VALUED_0:26
for X being ( ( non empty ) ( non empty ) set )
for s, s1 being ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of X : ( ( non empty ) ( non empty ) set ) ) st s : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of b1 : ( ( non empty ) ( non empty ) set ) ) is V29() & s1 : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of b1 : ( ( non empty ) ( non empty ) set ) ) is ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) subsequence of s : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of b1 : ( ( non empty ) ( non empty ) set ) ) ) holds
s : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of b1 : ( ( non empty ) ( non empty ) set ) ) = s1 : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of b1 : ( ( non empty ) ( non empty ) set ) ) ;

theorem :: VALUED_0:27
for X, Y being ( ( non empty ) ( non empty ) set )
for s being ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of X : ( ( non empty ) ( non empty ) set ) )
for h being ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like ) PartFunc of ,)
for n being ( ( natural ) ( complex epsilon-transitive epsilon-connected ordinal natural real integer rational ext-real ) Nat) st rng s : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) c= dom h : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) : ( ( ) ( ) Element of bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) holds
(h : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) /* s : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) ,b2 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ^\ n : ( ( natural ) ( complex epsilon-transitive epsilon-connected ordinal natural real integer rational ext-real ) Nat) : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) subsequence of b4 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) /* b3 : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) ,b2 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ) = h : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) /* (s : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of b1 : ( ( non empty ) ( non empty ) set ) ) ^\ n : ( ( natural ) ( complex epsilon-transitive epsilon-connected ordinal natural real integer rational ext-real ) Nat) ) : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) subsequence of b3 : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) ,b2 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: VALUED_0:28
for X being ( ( non empty ) ( non empty ) set )
for s being ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of X : ( ( non empty ) ( non empty ) set ) )
for n being ( ( natural ) ( complex epsilon-transitive epsilon-connected ordinal natural real integer rational ext-real ) Nat) holds s : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of b1 : ( ( non empty ) ( non empty ) set ) ) . n : ( ( natural ) ( complex epsilon-transitive epsilon-connected ordinal natural real integer rational ext-real ) Nat) : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) in rng s : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: VALUED_0:29
for X, Y being ( ( non empty ) ( non empty ) set )
for s being ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of X : ( ( non empty ) ( non empty ) set ) )
for h being ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like ) PartFunc of ,)
for n being ( ( natural ) ( complex epsilon-transitive epsilon-connected ordinal natural real integer rational ext-real ) Nat) st h : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) is total holds
h : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) /* (s : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of b1 : ( ( non empty ) ( non empty ) set ) ) ^\ n : ( ( natural ) ( complex epsilon-transitive epsilon-connected ordinal natural real integer rational ext-real ) Nat) ) : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) subsequence of b3 : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) ,b2 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) = (h : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) /* s : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) ,b2 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ^\ n : ( ( natural ) ( complex epsilon-transitive epsilon-connected ordinal natural real integer rational ext-real ) Nat) : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) subsequence of b4 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) /* b3 : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) ,b2 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: VALUED_0:30
for X, Y being ( ( non empty ) ( non empty ) set )
for s being ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of X : ( ( non empty ) ( non empty ) set ) )
for h being ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) st rng s : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) c= dom h : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) : ( ( ) ( ) Element of bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) holds
h : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) .: (rng s : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) Element of bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool b2 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = rng (h : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) /* s : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) ,b2 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool b2 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: VALUED_0:31
for X, Y being ( ( non empty ) ( non empty ) set )
for Z being ( ( ) ( ) set )
for s being ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of X : ( ( non empty ) ( non empty ) set ) )
for h1 being ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like ) PartFunc of ,)
for h2 being ( ( Function-like ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined b3 : ( ( ) ( ) set ) -valued Function-like ) PartFunc of ,) st rng s : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) c= dom (h2 : ( ( Function-like ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined b3 : ( ( ) ( ) set ) -valued Function-like ) PartFunc of ,) * h1 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b3 : ( ( ) ( ) set ) -valued Function-like ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool b1 : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) holds
h2 : ( ( Function-like ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined b3 : ( ( ) ( ) set ) -valued Function-like ) PartFunc of ,) /* (h1 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) /* s : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) ,b2 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b3 : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) ,b3 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) = (h2 : ( ( Function-like ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined b3 : ( ( ) ( ) set ) -valued Function-like ) PartFunc of ,) * h1 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b2 : ( ( non empty ) ( non empty ) set ) -valued Function-like ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b3 : ( ( ) ( ) set ) -valued Function-like ) Element of bool [:b1 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) /* s : ( ( Function-like quasi_total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like total quasi_total ) sequence of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined b3 : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) ,b3 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ;

definition
let f be ( ( Relation-like Function-like ext-real-valued ) ( Relation-like Function-like ext-real-valued ) Function) ;
attr f is zeroed means :: VALUED_0:def 19
f : ( ( with_non-empty_element ) ( non empty with_non-empty_element ) set ) . {} : ( ( ) ( complex empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real integer rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() Relation-like non-zero empty-yielding RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued Function-like one-to-one constant functional Function-yielding V40() ext-real complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing ) set ) : ( ( ) ( ) set ) = 0 : ( ( ) ( complex empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real integer rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() Relation-like non-zero empty-yielding RAT : ( ( ) ( complex-membered ext-real-membered real-membered rational-membered V21() ) set ) -valued Function-like one-to-one constant functional Function-yielding V40() ext-real complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) ) ;
end;

registration
cluster Relation-like COMPLEX : ( ( ) ( complex-membered V21() ) set ) -valued -> Relation-like complex-valued for ( ( ) ( ) set ) ;
cluster Relation-like ExtREAL : ( ( ) ( ext-real-membered ) set ) -valued -> Relation-like ext-real-valued for ( ( ) ( ) set ) ;
cluster Relation-like REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) -valued -> Relation-like real-valued for ( ( ) ( ) set ) ;
cluster Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -valued -> Relation-like natural-valued for ( ( ) ( ) set ) ;
end;

definition
let s be ( ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined Function-like total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined Function-like total ) ManySortedSet of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) ) ;
redefine attr s is constant means :: VALUED_0:def 20
 ex x being ( ( ) ( ) set ) st
for n being ( ( natural ) ( complex epsilon-transitive epsilon-connected ordinal natural real integer rational ext-real ) Nat) holds s : ( ( with_non-empty_element ) ( non empty with_non-empty_element ) set ) . n : ( ( natural ) ( complex epsilon-transitive epsilon-connected ordinal natural real integer rational ext-real ) Nat) : ( ( ) ( ) set ) = x : ( ( ) ( ) set ) ;
end;

theorem :: VALUED_0:32
for x being ( ( non empty ) ( non empty ) set )
for M being ( ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined Function-like total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined Function-like total ) ManySortedSet of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) )
for s being ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined Function-like total ) subsequence of M : ( ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined Function-like total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined Function-like total ) ManySortedSet of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) ) ) holds rng s : ( ( ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined Function-like total ) subsequence of b2 : ( ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined Function-like total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined Function-like total ) ManySortedSet of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty ) set ) c= rng M : ( ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined Function-like total ) ( non empty Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) -defined Function-like total ) ManySortedSet of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V21() ) Element of bool REAL : ( ( ) ( complex-membered ext-real-membered real-membered V21() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) ;

registration
let X be ( ( ) ( ) set ) ;
cluster Relation-like X : ( ( ) ( ) set ) -defined Function-like total natural-valued for ( ( ) ( ) set ) ;
end;