begin
begin
theorem
for
N being ( (
with_zero ) ( non
empty with_zero )
set )
for
S being ( ( non
empty with_non-empty_values IC-Ins-separated ) ( non
empty with_non-empty_values IC-Ins-separated )
AMI-Struct over
N : ( (
with_zero ) ( non
empty with_zero )
set ) )
for
f1,
f2 being ( (
Function-like quasi_total ) (
Relation-like NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) )
-defined NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) )
-valued non
empty Function-like total quasi_total )
Function of
NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) ) ,
NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) ) ) st
f1 : ( (
Function-like quasi_total ) (
Relation-like NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) )
-defined NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) )
-valued non
empty Function-like total quasi_total )
Function of
NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) ) ,
NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) ) ) is
bijective & ( for
m,
n being ( ( ) (
ordinal natural V16()
V17()
finite cardinal V41()
ext-real non
negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55()
V56()
V57()
countable V68() )
Element of
NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) ) ) holds
(
m : ( ( ) (
ordinal natural V16()
V17()
finite cardinal V41()
ext-real non
negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55()
V56()
V57()
countable V68() )
Element of
NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) ) )
<= n : ( ( ) (
ordinal natural V16()
V17()
finite cardinal V41()
ext-real non
negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55()
V56()
V57()
countable V68() )
Element of
NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) ) ) iff
f1 : ( (
Function-like quasi_total ) (
Relation-like NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) )
-defined NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) )
-valued non
empty Function-like total quasi_total )
Function of
NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) ) ,
NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) ) )
. m : ( ( ) (
ordinal natural V16()
V17()
finite cardinal V41()
ext-real non
negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55()
V56()
V57()
countable V68() )
Element of
NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) ) ) : ( ( ) (
ordinal natural V16()
V17()
finite cardinal V41()
ext-real non
negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55()
V56()
V57()
countable V68() )
Element of
NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) ) )
<= f1 : ( (
Function-like quasi_total ) (
Relation-like NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) )
-defined NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) )
-valued non
empty Function-like total quasi_total )
Function of
NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) ) ,
NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) ) )
. n : ( ( ) (
ordinal natural V16()
V17()
finite cardinal V41()
ext-real non
negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55()
V56()
V57()
countable V68() )
Element of
NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) ) ) : ( ( ) (
ordinal natural V16()
V17()
finite cardinal V41()
ext-real non
negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55()
V56()
V57()
countable V68() )
Element of
NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) ) ) ,
S : ( ( non
empty with_non-empty_values IC-Ins-separated ) ( non
empty with_non-empty_values IC-Ins-separated )
AMI-Struct over
b1 : ( (
with_zero ) ( non
empty with_zero )
set ) ) ) ) &
f2 : ( (
Function-like quasi_total ) (
Relation-like NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) )
-defined NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) )
-valued non
empty Function-like total quasi_total )
Function of
NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) ) ,
NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) ) ) is
bijective & ( for
m,
n being ( ( ) (
ordinal natural V16()
V17()
finite cardinal V41()
ext-real non
negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55()
V56()
V57()
countable V68() )
Element of
NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) ) ) holds
(
m : ( ( ) (
ordinal natural V16()
V17()
finite cardinal V41()
ext-real non
negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55()
V56()
V57()
countable V68() )
Element of
NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) ) )
<= n : ( ( ) (
ordinal natural V16()
V17()
finite cardinal V41()
ext-real non
negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55()
V56()
V57()
countable V68() )
Element of
NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) ) ) iff
f2 : ( (
Function-like quasi_total ) (
Relation-like NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) )
-defined NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) )
-valued non
empty Function-like total quasi_total )
Function of
NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) ) ,
NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) ) )
. m : ( ( ) (
ordinal natural V16()
V17()
finite cardinal V41()
ext-real non
negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55()
V56()
V57()
countable V68() )
Element of
NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) ) ) : ( ( ) (
ordinal natural V16()
V17()
finite cardinal V41()
ext-real non
negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55()
V56()
V57()
countable V68() )
Element of
NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) ) )
<= f2 : ( (
Function-like quasi_total ) (
Relation-like NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) )
-defined NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) )
-valued non
empty Function-like total quasi_total )
Function of
NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) ) ,
NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) ) )
. n : ( ( ) (
ordinal natural V16()
V17()
finite cardinal V41()
ext-real non
negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55()
V56()
V57()
countable V68() )
Element of
NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) ) ) : ( ( ) (
ordinal natural V16()
V17()
finite cardinal V41()
ext-real non
negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55()
V56()
V57()
countable V68() )
Element of
NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) ) ) ,
S : ( ( non
empty with_non-empty_values IC-Ins-separated ) ( non
empty with_non-empty_values IC-Ins-separated )
AMI-Struct over
b1 : ( (
with_zero ) ( non
empty with_zero )
set ) ) ) ) holds
f1 : ( (
Function-like quasi_total ) (
Relation-like NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) )
-defined NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) )
-valued non
empty Function-like total quasi_total )
Function of
NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) ) ,
NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) ) )
= f2 : ( (
Function-like quasi_total ) (
Relation-like NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) )
-defined NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) )
-valued non
empty Function-like total quasi_total )
Function of
NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) ) ,
NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) ) ) ;
theorem
for
N being ( (
with_zero ) ( non
empty with_zero )
set )
for
S being ( ( non
empty with_non-empty_values IC-Ins-separated ) ( non
empty with_non-empty_values IC-Ins-separated )
AMI-Struct over
N : ( (
with_zero ) ( non
empty with_zero )
set ) )
for
f being ( (
Function-like quasi_total ) (
Relation-like NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) )
-defined NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) )
-valued non
empty Function-like total quasi_total )
Function of
NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) ) ,
NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) ) ) st
f : ( (
Function-like quasi_total ) (
Relation-like NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) )
-defined NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) )
-valued non
empty Function-like total quasi_total )
Function of
NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) ) ,
NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) ) ) is
bijective holds
( ( for
m,
n being ( ( ) (
ordinal natural V16()
V17()
finite cardinal V41()
ext-real non
negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55()
V56()
V57()
countable V68() )
Element of
NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) ) ) holds
(
m : ( ( ) (
ordinal natural V16()
V17()
finite cardinal V41()
ext-real non
negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55()
V56()
V57()
countable V68() )
Element of
NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) ) )
<= n : ( ( ) (
ordinal natural V16()
V17()
finite cardinal V41()
ext-real non
negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55()
V56()
V57()
countable V68() )
Element of
NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) ) ) iff
f : ( (
Function-like quasi_total ) (
Relation-like NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) )
-defined NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) )
-valued non
empty Function-like total quasi_total )
Function of
NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) ) ,
NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) ) )
. m : ( ( ) (
ordinal natural V16()
V17()
finite cardinal V41()
ext-real non
negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55()
V56()
V57()
countable V68() )
Element of
NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) ) ) : ( ( ) (
ordinal natural V16()
V17()
finite cardinal V41()
ext-real non
negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55()
V56()
V57()
countable V68() )
Element of
NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) ) )
<= f : ( (
Function-like quasi_total ) (
Relation-like NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) )
-defined NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) )
-valued non
empty Function-like total quasi_total )
Function of
NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) ) ,
NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) ) )
. n : ( ( ) (
ordinal natural V16()
V17()
finite cardinal V41()
ext-real non
negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55()
V56()
V57()
countable V68() )
Element of
NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) ) ) : ( ( ) (
ordinal natural V16()
V17()
finite cardinal V41()
ext-real non
negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55()
V56()
V57()
countable V68() )
Element of
NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) ) ) ,
S : ( ( non
empty with_non-empty_values IC-Ins-separated ) ( non
empty with_non-empty_values IC-Ins-separated )
AMI-Struct over
b1 : ( (
with_zero ) ( non
empty with_zero )
set ) ) ) ) iff for
k being ( ( ) (
ordinal natural V16()
V17()
finite cardinal V41()
ext-real non
negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55()
V56()
V57()
countable V68() )
Element of
NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) ) ) holds
(
f : ( (
Function-like quasi_total ) (
Relation-like NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) )
-defined NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) )
-valued non
empty Function-like total quasi_total )
Function of
NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) ) ,
NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) ) )
. (k : ( ( ) ( ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() ) Element of NAT : ( ( ) ( ordinal non empty non trivial non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52() V53() V55() countable denumerable with_zero ) Element of bool REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V55() V56() V58() with_zero ) set ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( ordinal natural non empty V16() V17() finite cardinal V41() ext-real positive non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53() V54() V55() V56() V57() countable V68() ) Element of NAT : ( ( ) ( ordinal non empty non trivial non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52() V53() V55() countable denumerable with_zero ) Element of bool REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V55() V56() V58() with_zero ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) (
ordinal natural non
empty V16()
V17()
finite cardinal V41()
ext-real positive non
negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V53()
V54()
V55()
V56()
V57()
countable V68() )
Element of
NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) ) ) : ( ( ) (
ordinal natural V16()
V17()
finite cardinal V41()
ext-real non
negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55()
V56()
V57()
countable V68() )
Element of
NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) ) )
in SUCC (
(f : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( ordinal non empty non trivial non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52() V53() V55() countable denumerable with_zero ) Element of bool REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V55() V56() V58() with_zero ) set ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( ordinal non empty non trivial non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52() V53() V55() countable denumerable with_zero ) Element of bool REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V55() V56() V58() with_zero ) set ) : ( ( ) ( ) set ) ) -valued non empty Function-like total quasi_total ) Function of NAT : ( ( ) ( ordinal non empty non trivial non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52() V53() V55() countable denumerable with_zero ) Element of bool REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V55() V56() V58() with_zero ) set ) : ( ( ) ( ) set ) ) , NAT : ( ( ) ( ordinal non empty non trivial non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52() V53() V55() countable denumerable with_zero ) Element of bool REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V55() V56() V58() with_zero ) set ) : ( ( ) ( ) set ) ) ) . k : ( ( ) ( ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() ) Element of NAT : ( ( ) ( ordinal non empty non trivial non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52() V53() V55() countable denumerable with_zero ) Element of bool REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V55() V56() V58() with_zero ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) (
ordinal natural V16()
V17()
finite cardinal V41()
ext-real non
negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55()
V56()
V57()
countable V68() )
Element of
NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) ) ) ,
S : ( ( non
empty with_non-empty_values IC-Ins-separated ) ( non
empty with_non-empty_values IC-Ins-separated )
AMI-Struct over
b1 : ( (
with_zero ) ( non
empty with_zero )
set ) ) ) : ( ( ) (
complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55()
countable )
Element of
bool NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) ) : ( ( ) ( non
trivial non
finite )
set ) ) & ( for
j being ( ( ) (
ordinal natural V16()
V17()
finite cardinal V41()
ext-real non
negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55()
V56()
V57()
countable V68() )
Element of
NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) ) ) st
f : ( (
Function-like quasi_total ) (
Relation-like NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) )
-defined NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) )
-valued non
empty Function-like total quasi_total )
Function of
NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) ) ,
NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) ) )
. j : ( ( ) (
ordinal natural V16()
V17()
finite cardinal V41()
ext-real non
negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55()
V56()
V57()
countable V68() )
Element of
NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) ) ) : ( ( ) (
ordinal natural V16()
V17()
finite cardinal V41()
ext-real non
negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55()
V56()
V57()
countable V68() )
Element of
NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) ) )
in SUCC (
(f : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( ordinal non empty non trivial non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52() V53() V55() countable denumerable with_zero ) Element of bool REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V55() V56() V58() with_zero ) set ) : ( ( ) ( ) set ) ) -defined NAT : ( ( ) ( ordinal non empty non trivial non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52() V53() V55() countable denumerable with_zero ) Element of bool REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V55() V56() V58() with_zero ) set ) : ( ( ) ( ) set ) ) -valued non empty Function-like total quasi_total ) Function of NAT : ( ( ) ( ordinal non empty non trivial non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52() V53() V55() countable denumerable with_zero ) Element of bool REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V55() V56() V58() with_zero ) set ) : ( ( ) ( ) set ) ) , NAT : ( ( ) ( ordinal non empty non trivial non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52() V53() V55() countable denumerable with_zero ) Element of bool REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V55() V56() V58() with_zero ) set ) : ( ( ) ( ) set ) ) ) . k : ( ( ) ( ordinal natural V16() V17() finite cardinal V41() ext-real non negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55() V56() V57() countable V68() ) Element of NAT : ( ( ) ( ordinal non empty non trivial non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52() V53() V55() countable denumerable with_zero ) Element of bool REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V52() V55() V56() V58() with_zero ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( ) (
ordinal natural V16()
V17()
finite cardinal V41()
ext-real non
negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55()
V56()
V57()
countable V68() )
Element of
NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) ) ) ,
S : ( ( non
empty with_non-empty_values IC-Ins-separated ) ( non
empty with_non-empty_values IC-Ins-separated )
AMI-Struct over
b1 : ( (
with_zero ) ( non
empty with_zero )
set ) ) ) : ( ( ) (
complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55()
countable )
Element of
bool NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) ) : ( ( ) ( non
trivial non
finite )
set ) ) holds
k : ( ( ) (
ordinal natural V16()
V17()
finite cardinal V41()
ext-real non
negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55()
V56()
V57()
countable V68() )
Element of
NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) ) )
<= j : ( ( ) (
ordinal natural V16()
V17()
finite cardinal V41()
ext-real non
negative complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V55()
V56()
V57()
countable V68() )
Element of
NAT : ( ( ) (
ordinal non
empty non
trivial non
finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V52()
V53()
V55()
countable denumerable with_zero )
Element of
bool REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V52()
V55()
V56()
V58()
with_zero )
set ) : ( ( ) ( )
set ) ) ) ) ) ) ;
begin
begin