begin
definition
func COMPLEX -> ( ( ) ( )
set )
equals
((Funcs ({0 : ( ( ) ( Relation-like non-empty empty-yielding empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite ) set ) ,1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural finite ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite ) set ) ) } : ( ( ) ( non empty ) set ) ,REAL : ( ( ) ( non empty ) set ) )) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of {0 : ( ( ) ( Relation-like non-empty empty-yielding empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite ) set ) ,1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural finite ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite ) set ) ) } : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty ) set ) ) \ { x : ( ( ) ( Relation-like Function-like V14({0 : ( ( ) ( Relation-like non-empty empty-yielding empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite ) set ) ,1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural finite ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite ) set ) ) } : ( ( ) ( non empty ) set ) ) quasi_total ) Element of Funcs ({0 : ( ( ) ( Relation-like non-empty empty-yielding empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite ) set ) ,1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural finite ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite ) set ) ) } : ( ( ) ( non empty ) set ) ,REAL : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of {0 : ( ( ) ( Relation-like non-empty empty-yielding empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite ) set ) ,1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural finite ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite ) set ) ) } : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty ) set ) ) ) where x is ( ( ) ( Relation-like Function-like V14({0 : ( ( ) ( Relation-like non-empty empty-yielding empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite ) set ) ,1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural finite ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite ) set ) ) } : ( ( ) ( non empty ) set ) ) quasi_total ) Element of Funcs ({0 : ( ( ) ( Relation-like non-empty empty-yielding empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite ) set ) ,1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural finite ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite ) set ) ) } : ( ( ) ( non empty ) set ) ,REAL : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of {0 : ( ( ) ( Relation-like non-empty empty-yielding empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite ) set ) ,1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural finite ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite ) set ) ) } : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty ) set ) ) ) : x : ( ( ) ( Relation-like Function-like V14({0 : ( ( ) ( Relation-like non-empty empty-yielding empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite ) set ) ,1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural finite ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite ) set ) ) } : ( ( ) ( non empty ) set ) ) quasi_total ) Element of Funcs ({0 : ( ( ) ( Relation-like non-empty empty-yielding empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite ) set ) ,1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural finite ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite ) set ) ) } : ( ( ) ( non empty ) set ) ,REAL : ( ( ) ( non empty ) set ) ) : ( ( ) ( functional non empty ) FUNCTION_DOMAIN of {0 : ( ( ) ( Relation-like non-empty empty-yielding empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite ) set ) ,1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural finite ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite ) set ) ) } : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty ) set ) ) ) . 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural finite ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite ) set ) ) : ( ( ) ( ) set ) = 0 : ( ( ) ( Relation-like non-empty empty-yielding empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite ) set ) } ) : ( ( ) ( )
Element of
bool (Funcs ({0 : ( ( ) ( Relation-like non-empty empty-yielding empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite ) set ) ,1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural finite ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite ) set ) ) } : ( ( ) ( non empty ) set ) ,REAL : ( ( ) ( non empty ) set ) )) : ( ( ) (
functional non
empty )
FUNCTION_DOMAIN of
{0 : ( ( ) ( Relation-like non-empty empty-yielding empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite ) set ) ,1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural finite ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal non finite ) set ) ) } : ( ( ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set ) )
\/ REAL : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ;
NATredefine func NAT -> ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ;
end;
begin