REAL is non empty non trivial non finite V72() V73() V74() V78() V295() V296() V298() set
NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V72() V73() V74() V75() V76() V77() V78() V293() V295() Element of bool REAL
bool REAL is non empty non trivial non finite cup-closed diff-closed preBoolean set
omega is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V72() V73() V74() V75() V76() V77() V78() V293() V295() set
bool omega is non empty non trivial non finite cup-closed diff-closed preBoolean set
bool NAT is non empty non trivial non finite cup-closed diff-closed preBoolean set
COMPLEX is non empty non trivial non finite V72() V78() set
RAT is non empty non trivial non finite V72() V73() V74() V75() V78() set
INT is non empty non trivial non finite V72() V73() V74() V75() V76() V78() set
[:REAL,REAL:] is non empty non trivial Relation-like non finite complex-valued ext-real-valued real-valued set
bool [:REAL,REAL:] is non empty non trivial non finite cup-closed diff-closed preBoolean set
{} is empty Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional Function-yielding epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding V34() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V42() V43() ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V72() V73() V74() V75() V76() V77() V78() FinSequence-yielding finite-support V295() V296() V297() V298() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real positive non negative V49() V72() V73() V74() V75() V76() V77() V293() V294() V295() V296() V297() Element of NAT
{{},1} is non empty finite V34() V72() V73() V74() V75() V76() V77() V293() V294() V295() V296() V297() set
K392() is set
bool K392() is non empty cup-closed diff-closed preBoolean set
K393() is Element of bool K392()
K458() is set
{{}} is non empty trivial functional finite V34() 1 -element V72() V73() V74() V75() V76() V77() V293() V294() V295() V296() V297() set
{{}} * is non empty functional FinSequence-membered FinSequenceSet of {{}}
[:({{}} *),{{}}:] is non empty Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
bool [:({{}} *),{{}}:] is non empty cup-closed diff-closed preBoolean set
PFuncs (({{}} *),{{}}) is set
2 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real positive non negative V49() V72() V73() V74() V75() V76() V77() V293() V294() V295() V296() V297() Element of NAT
[:NAT,NAT:] is non empty non trivial Relation-like RAT -valued INT -valued non finite complex-valued ext-real-valued real-valued natural-valued set
bool [:NAT,NAT:] is non empty non trivial non finite cup-closed diff-closed preBoolean set
[:COMPLEX,COMPLEX:] is non empty non trivial Relation-like non finite complex-valued set
bool [:COMPLEX,COMPLEX:] is non empty non trivial non finite cup-closed diff-closed preBoolean set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial Relation-like non finite complex-valued set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial non finite cup-closed diff-closed preBoolean set
[:[:REAL,REAL:],REAL:] is non empty non trivial Relation-like non finite complex-valued ext-real-valued real-valued set
bool [:[:REAL,REAL:],REAL:] is non empty non trivial non finite cup-closed diff-closed preBoolean set
[:RAT,RAT:] is non empty non trivial Relation-like RAT -valued non finite complex-valued ext-real-valued real-valued set
bool [:RAT,RAT:] is non empty non trivial non finite cup-closed diff-closed preBoolean set
[:[:RAT,RAT:],RAT:] is non empty non trivial Relation-like RAT -valued non finite complex-valued ext-real-valued real-valued set
bool [:[:RAT,RAT:],RAT:] is non empty non trivial non finite cup-closed diff-closed preBoolean set
[:INT,INT:] is non empty non trivial Relation-like RAT -valued INT -valued non finite complex-valued ext-real-valued real-valued set
bool [:INT,INT:] is non empty non trivial non finite cup-closed diff-closed preBoolean set
[:[:INT,INT:],INT:] is non empty non trivial Relation-like RAT -valued INT -valued non finite complex-valued ext-real-valued real-valued set
bool [:[:INT,INT:],INT:] is non empty non trivial non finite cup-closed diff-closed preBoolean set
[:[:NAT,NAT:],NAT:] is non empty non trivial Relation-like RAT -valued INT -valued non finite complex-valued ext-real-valued real-valued natural-valued set
bool [:[:NAT,NAT:],NAT:] is non empty non trivial non finite cup-closed diff-closed preBoolean set
[:COMPLEX,REAL:] is non empty non trivial Relation-like non finite complex-valued ext-real-valued real-valued set
bool [:COMPLEX,REAL:] is non empty non trivial non finite cup-closed diff-closed preBoolean set
K516() is Relation-like NAT -defined Function-like total set
3 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real positive non negative V49() V72() V73() V74() V75() V76() V77() V293() V294() V295() V296() V297() Element of NAT
dom {} is empty Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional Function-yielding epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding V34() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V42() V43() ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V72() V73() V74() V75() V76() V77() V78() FinSequence-yielding finite-support V295() V296() V297() V298() set
rng {} is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional Function-yielding epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding V34() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V42() V43() ext-real non positive non negative V50() complex-valued ext-real-valued real-valued natural-valued V66() decreasing non-decreasing non-increasing V72() V73() V74() V75() V76() V77() V78() FinSequence-yielding finite-support V295() V296() V297() V298() set
NATOrd is Relation-like NAT -defined NAT -valued complex-valued ext-real-valued real-valued natural-valued Element of bool [:NAT,NAT:]
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of NAT : b1 <= b2 } is set
OrderedNAT is non empty transitive antisymmetric connected well_founded quasi_ordered Dickson RelStr
RelStr(# NAT,NATOrd #) is non empty strict RelStr
<*> REAL is empty proper Relation-like non-empty empty-yielding NAT -defined REAL -valued Function-like one-to-one constant functional Function-yielding epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding V34() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V42() V43() ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V72() V73() V74() V75() V76() V77() V78() FinSequence-yielding finite-support V295() V296() V297() V298() FinSequence of REAL
[:NAT,REAL:] is non empty non trivial Relation-like non finite complex-valued ext-real-valued real-valued set
Sum (<*> REAL) is V42() V43() ext-real Element of REAL
0 is empty Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional Function-yielding epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding V34() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V42() V43() V44() ext-real non positive non negative V49() complex-valued ext-real-valued real-valued natural-valued V72() V73() V74() V75() V76() V77() V78() FinSequence-yielding finite-support V295() V296() V297() V298() Element of NAT
card {} is empty Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional Function-yielding epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite finite-yielding V34() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V42() V43() ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V72() V73() V74() V75() V76() V77() V78() FinSequence-yielding finite-support V295() V296() V297() V298() set
CR is set
R is set
IR is set
{CR} is non empty trivial finite 1 -element set
R \ {CR} is Element of bool R
bool R is non empty cup-closed diff-closed preBoolean set
IR \ {CR} is Element of bool IR
bool IR is non empty cup-closed diff-closed preBoolean set
R \/ {CR} is non empty set
(IR \ {CR}) \/ {CR} is non empty set
IR \/ {CR} is non empty set
IR is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of NAT
R is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of NAT
Seg R is finite R -element V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of bool NAT
IR - 1 is V42() V43() ext-real Element of REAL
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of NAT : ( 1 <= b1 & b1 <= R ) } is set
CR is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of NAT
R - 1 is V42() V43() ext-real Element of REAL
A is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of NAT
- 1 is V42() V43() ext-real non positive Element of REAL
IR + (- 1) is V42() V43() ext-real Element of REAL
R + (- 1) is V42() V43() ext-real Element of REAL
zz is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of NAT
zz + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real positive non negative V49() V72() V73() V74() V75() V76() V77() V293() V294() V295() V296() V297() Element of NAT
CR is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of NAT
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real positive non negative V49() V72() V73() V74() V75() V76() V77() V293() V294() V295() V296() V297() Element of NAT
(IR - 1) + 1 is V42() V43() ext-real Element of REAL
(R - 1) + 1 is V42() V43() ext-real Element of REAL
R is Relation-like Function-like finite-support set
IR is set
R | IR is Relation-like Function-like set
support (R | IR) is set
support R is finite set
CR is set
(R | IR) . CR is set
dom (R | IR) is set
R . CR is set
R is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued Cardinal-yielding finite-support FinSequence of NAT
Sum R is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of NAT
len R is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of NAT
(len R) |-> 0 is Relation-like NAT -defined NAT -valued Function-like Function-yielding finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued Cardinal-yielding FinSequence-yielding finite-support Element of (len R) -tuples_on NAT
(len R) -tuples_on NAT is FinSequenceSet of NAT
NAT * is non empty functional FinSequence-membered FinSequenceSet of NAT
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of NAT * : len b1 = len R } is set
Seg (len R) is finite len R -element V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of bool NAT
(Seg (len R)) --> 0 is Relation-like Seg (len R) -defined RAT -valued INT -valued {0} -valued Function-like total V18( Seg (len R),{0}) finite complex-valued ext-real-valued real-valued natural-valued finite-support Element of bool [:(Seg (len R)),{0}:]
{0} is non empty trivial functional finite V34() 1 -element V72() V73() V74() V75() V76() V77() V293() V294() V295() V296() V297() set
[:(Seg (len R)),{0}:] is Relation-like RAT -valued INT -valued finite complex-valued ext-real-valued real-valued natural-valued set
bool [:(Seg (len R)),{0}:] is non empty finite V34() cup-closed diff-closed preBoolean set
dom R is finite V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of bool NAT
dom ((len R) |-> 0) is finite V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of bool NAT
IR is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() ext-real non negative set
R . IR is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of NAT
CR is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() ext-real non negative set
R . CR is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of NAT
((len R) |-> 0) . IR is epsilon-transitive epsilon-connected ordinal natural finite cardinal FinSequence-like V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of NAT
R is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() ext-real non negative set
CR is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() ext-real non negative set
IR is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() ext-real non negative set
CR -' IR is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of NAT
FIR is Relation-like R -defined Function-like total finite-support set
FCR is set
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of NAT : not CR -' IR <= b1 } is set
zz is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of NAT
A is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of NAT
IR + A is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of NAT
FIR . (IR + A) is set
zz is set
zz is set
FCR is set
FCR is Relation-like Function-like set
dom FCR is set
A is Relation-like CR -' IR -defined Function-like total finite-support set
zz is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of NAT
A . zz is set
IR + zz is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of NAT
FIR . (IR + zz) is set
zz is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of NAT
IR + zz is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of NAT
FIR . (IR + zz) is set
FCR is Relation-like CR -' IR -defined Function-like total finite-support set
A is Relation-like CR -' IR -defined Function-like total finite-support set
dom FCR is finite V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of bool (CR -' IR)
bool (CR -' IR) is non empty finite V34() cup-closed diff-closed preBoolean set
dom A is finite V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of bool (CR -' IR)
zz is set
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of NAT : not CR -' IR <= b1 } is set
Z is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of NAT
FCR . zz is set
zz is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of NAT
IR + zz is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of NAT
FIR . (IR + zz) is set
A . zz is set
R is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() ext-real non negative set
IR is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() ext-real non negative set
CR is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() ext-real non negative set
FIR is Relation-like R -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set
(R,IR,CR,FIR) is Relation-like CR -' IR -defined Function-like total finite-support set
CR -' IR is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of NAT
FCR is set
rng (R,IR,CR,FIR) is set
dom (R,IR,CR,FIR) is finite V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of bool (CR -' IR)
bool (CR -' IR) is non empty finite V34() cup-closed diff-closed preBoolean set
A is set
(R,IR,CR,FIR) . A is set
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of NAT : not CR -' IR <= b1 } is set
zz is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of NAT
zz is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of NAT
IR + zz is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of NAT
FIR . (IR + zz) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of NAT
R is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of NAT
IR is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of NAT
CR is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of NAT
FIR is Relation-like R -defined Function-like total finite-support set
(R,IR,CR,FIR) is Relation-like CR -' IR -defined Function-like total finite-support set
CR -' IR is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of NAT
R is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() ext-real non negative set
IR is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() ext-real non negative set
IR + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real positive non negative V49() V72() V73() V74() V75() V76() V77() V293() V294() V295() V296() V297() Element of NAT
CR is Relation-like R -defined Function-like total finite-support set
FIR is Relation-like R -defined Function-like total finite-support set
(R,0,(IR + 1),CR) is Relation-like (IR + 1) -' 0 -defined Function-like total finite-support set
(IR + 1) -' 0 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of NAT
(R,0,(IR + 1),FIR) is Relation-like (IR + 1) -' 0 -defined Function-like total finite-support set
(R,(IR + 1),R,CR) is Relation-like R -' (IR + 1) -defined Function-like total finite-support set
R -' (IR + 1) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of NAT
(R,(IR + 1),R,FIR) is Relation-like R -' (IR + 1) -defined Function-like total finite-support set
Z is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of NAT
(IR + 1) + 0 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real positive non negative V49() V72() V73() V74() V75() V76() V77() V293() V294() V295() V296() V297() Element of NAT
((IR + 1) + 0) -' 0 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of NAT
(R,0,(IR + 1),FIR) . Z is set
0 + Z is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of NAT
FIR . (0 + Z) is set
CR . Z is set
FIR . Z is set
Z is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of NAT
Z -' (IR + 1) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of NAT
(IR + 1) - (IR + 1) is V42() V43() ext-real Element of REAL
Z - (IR + 1) is V42() V43() ext-real Element of REAL
R - (IR + 1) is V42() V43() ext-real Element of REAL
(R,(IR + 1),R,FIR) . (Z -' (IR + 1)) is set
(IR + 1) + (Z -' (IR + 1)) is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real positive non negative V49() V72() V73() V74() V75() V76() V77() V293() V294() V295() V296() V297() Element of NAT
FIR . ((IR + 1) + (Z -' (IR + 1))) is set
CR . Z is set
FIR . Z is set
Z is set
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of NAT : not R <= b1 } is set
SS is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of NAT
aStart is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of NAT
CR . Z is set
FIR . Z is set
aStart is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of NAT
CR . Z is set
FIR . Z is set
SS is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of NAT
aStart is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of NAT
R is non empty set
bool R is non empty cup-closed diff-closed preBoolean set
IR is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real positive non negative V49() V72() V73() V74() V75() V76() V77() V293() V294() V295() V296() V297() Element of NAT
{ b1 where b1 is Element of bool R : ( b1 is finite & not b1 is empty & card b1 c= IR ) } is set
R is non empty set
IR is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real positive non negative V49() V72() V73() V74() V75() V76() V77() V293() V294() V295() V296() V297() Element of NAT
(R,IR) is set
bool R is non empty cup-closed diff-closed preBoolean set
{ b1 where b1 is Element of bool R : ( b1 is finite & not b1 is empty & card b1 c= IR ) } is set
the Element of R is Element of R
IR + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real positive non negative V49() V72() V73() V74() V75() V76() V77() V293() V294() V295() V296() V297() Element of NAT
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real positive non negative V49() V72() V73() V74() V75() V76() V77() V293() V294() V295() V296() V297() Element of NAT
{ the Element of R} is non empty trivial finite 1 -element Element of bool R
card { the Element of R} is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real positive non negative V49() V72() V73() V74() V75() V76() V77() V293() V294() V295() V296() V297() Element of omega
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of NAT : not 1 <= b1 } is set
{ the Element of R} is non empty trivial finite 1 -element Element of bool R
card { the Element of R} is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real positive non negative V49() V72() V73() V74() V75() V76() V77() V293() V294() V295() V296() V297() Element of omega
FIR is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of NAT
{ the Element of R} is non empty trivial finite 1 -element Element of bool R
card { the Element of R} is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real positive non negative V49() V72() V73() V74() V75() V76() V77() V293() V294() V295() V296() V297() Element of omega
{ the Element of R} is non empty trivial finite 1 -element Element of bool R
card { the Element of R} is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real positive non negative V49() V72() V73() V74() V75() V76() V77() V293() V294() V295() V296() V297() Element of omega
R is non empty transitive antisymmetric RelStr
the carrier of R is non empty set
bool the carrier of R is non empty cup-closed diff-closed preBoolean set
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is non empty Relation-like set
bool [: the carrier of R, the carrier of R:] is non empty cup-closed diff-closed preBoolean set
IR is finite Element of bool the carrier of R
FCR is set
A is set
{FCR} is non empty trivial finite 1 -element set
A \/ {FCR} is non empty set
zz is Element of the carrier of R
zz is Element of the carrier of R
{zz} is non empty trivial finite 1 -element Element of bool the carrier of R
A \/ {zz} is non empty set
Z is set
[zz,Z] is V1() set
{zz,Z} is non empty finite set
{zz} is non empty trivial finite 1 -element set
{{zz,Z},{zz}} is non empty finite V34() set
zz is Element of the carrier of R
zz is Element of the carrier of R
[zz,FCR] is V1() set
{zz,FCR} is non empty finite set
{zz} is non empty trivial finite 1 -element set
{{zz,FCR},{zz}} is non empty finite V34() set
zz is Element of the carrier of R
Z is Element of the carrier of R
aStart is set
[FCR,aStart] is V1() set
{FCR,aStart} is non empty finite set
{{FCR,aStart},{FCR}} is non empty finite V34() set
[zz,aStart] is V1() set
{zz,aStart} is non empty finite set
{{zz,aStart},{zz}} is non empty finite V34() set
[FCR,zz] is V1() set
{FCR,zz} is non empty finite set
{{FCR,zz},{FCR}} is non empty finite V34() set
Z is Element of the carrier of R
aStart is set
[Z,aStart] is V1() set
{Z,aStart} is non empty finite set
{Z} is non empty trivial finite 1 -element set
{{Z,aStart},{Z}} is non empty finite V34() set
aStart is set
[Z,aStart] is V1() set
{Z,aStart} is non empty finite set
{Z} is non empty trivial finite 1 -element set
{{Z,aStart},{Z}} is non empty finite V34() set
[zz,FCR] is V1() set
{zz,FCR} is non empty finite set
{zz} is non empty trivial finite 1 -element set
{{zz,FCR},{zz}} is non empty finite V34() set
[FCR,zz] is V1() set
{FCR,zz} is non empty finite set
{{FCR,zz},{FCR}} is non empty finite V34() set
Z is Element of the carrier of R
aStart is set
[Z,aStart] is V1() set
{Z,aStart} is non empty finite set
{Z} is non empty trivial finite 1 -element set
{{Z,aStart},{Z}} is non empty finite V34() set
aStart is set
[Z,aStart] is V1() set
{Z,aStart} is non empty finite set
{Z} is non empty trivial finite 1 -element set
{{Z,aStart},{Z}} is non empty finite V34() set
[zz,FCR] is V1() set
{zz,FCR} is non empty finite set
{zz} is non empty trivial finite 1 -element set
{{zz,FCR},{zz}} is non empty finite V34() set
[FCR,zz] is V1() set
{FCR,zz} is non empty finite set
{{FCR,zz},{FCR}} is non empty finite V34() set
Z is Element of the carrier of R
FCR is set
A is set
zz is Element of the carrier of R
{FCR} is non empty trivial finite 1 -element set
A \/ {FCR} is non empty set
R is non empty transitive antisymmetric RelStr
the carrier of R is non empty set
bool the carrier of R is non empty cup-closed diff-closed preBoolean set
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is non empty Relation-like set
bool [: the carrier of R, the carrier of R:] is non empty cup-closed diff-closed preBoolean set
IR is finite Element of bool the carrier of R
FCR is set
A is set
{FCR} is non empty trivial finite 1 -element set
A \/ {FCR} is non empty set
zz is Element of the carrier of R
zz is Element of the carrier of R
{zz} is non empty trivial finite 1 -element Element of bool the carrier of R
A \/ {zz} is non empty set
Z is set
[Z,zz] is V1() set
{Z,zz} is non empty finite set
{Z} is non empty trivial finite 1 -element set
{{Z,zz},{Z}} is non empty finite V34() set
zz is Element of the carrier of R
zz is Element of the carrier of R
[FCR,zz] is V1() set
{FCR,zz} is non empty finite set
{{FCR,zz},{FCR}} is non empty finite V34() set
zz is Element of the carrier of R
Z is Element of the carrier of R
aStart is set
[aStart,FCR] is V1() set
{aStart,FCR} is non empty finite set
{aStart} is non empty trivial finite 1 -element set
{{aStart,FCR},{aStart}} is non empty finite V34() set
aStart is set
[aStart,FCR] is V1() set
{aStart,FCR} is non empty finite set
{aStart} is non empty trivial finite 1 -element set
{{aStart,FCR},{aStart}} is non empty finite V34() set
[aStart,zz] is V1() set
{aStart,zz} is non empty finite set
{{aStart,zz},{aStart}} is non empty finite V34() set
[zz,FCR] is V1() set
{zz,FCR} is non empty finite set
{zz} is non empty trivial finite 1 -element set
{{zz,FCR},{zz}} is non empty finite V34() set
Z is Element of the carrier of R
aStart is set
[aStart,Z] is V1() set
{aStart,Z} is non empty finite set
{aStart} is non empty trivial finite 1 -element set
{{aStart,Z},{aStart}} is non empty finite V34() set
aStart is set
[aStart,Z] is V1() set
{aStart,Z} is non empty finite set
{aStart} is non empty trivial finite 1 -element set
{{aStart,Z},{aStart}} is non empty finite V34() set
[zz,FCR] is V1() set
{zz,FCR} is non empty finite set
{zz} is non empty trivial finite 1 -element set
{{zz,FCR},{zz}} is non empty finite V34() set
[FCR,zz] is V1() set
{FCR,zz} is non empty finite set
{{FCR,zz},{FCR}} is non empty finite V34() set
Z is Element of the carrier of R
aStart is set
[aStart,Z] is V1() set
{aStart,Z} is non empty finite set
{aStart} is non empty trivial finite 1 -element set
{{aStart,Z},{aStart}} is non empty finite V34() set
aStart is set
[aStart,Z] is V1() set
{aStart,Z} is non empty finite set
{aStart} is non empty trivial finite 1 -element set
{{aStart,Z},{aStart}} is non empty finite V34() set
[FCR,zz] is V1() set
{FCR,zz} is non empty finite set
{{FCR,zz},{FCR}} is non empty finite V34() set
[zz,FCR] is V1() set
{zz,FCR} is non empty finite set
{zz} is non empty trivial finite 1 -element set
{{zz,FCR},{zz}} is non empty finite V34() set
Z is Element of the carrier of R
FCR is set
A is set
zz is Element of the carrier of R
{FCR} is non empty trivial finite 1 -element set
A \/ {FCR} is non empty set
R is non empty transitive antisymmetric RelStr
the carrier of R is non empty set
[:NAT, the carrier of R:] is non empty non trivial Relation-like non finite set
bool [:NAT, the carrier of R:] is non empty non trivial non finite cup-closed diff-closed preBoolean set
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is non empty Relation-like set
bool [: the carrier of R, the carrier of R:] is non empty cup-closed diff-closed preBoolean set
IR is non empty Relation-like NAT -defined the carrier of R -valued Function-like total V18( NAT , the carrier of R) Element of bool [:NAT, the carrier of R:]
IR . 0 is Element of the carrier of R
FCR is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() ext-real non negative set
IR . FCR is Element of the carrier of R
[(IR . 0),(IR . FCR)] is V1() Element of [: the carrier of R, the carrier of R:]
{(IR . 0),(IR . FCR)} is non empty finite set
{(IR . 0)} is non empty trivial finite 1 -element set
{{(IR . 0),(IR . FCR)},{(IR . 0)}} is non empty finite V34() set
FCR is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() ext-real non negative set
IR . FCR is Element of the carrier of R
FCR + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real positive non negative V49() V72() V73() V74() V75() V76() V77() V293() V294() V295() V296() V297() Element of NAT
A is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() ext-real non negative set
IR . A is Element of the carrier of R
IR . (FCR + 1) is Element of the carrier of R
[(IR . (FCR + 1)),(IR . A)] is V1() Element of [: the carrier of R, the carrier of R:]
{(IR . (FCR + 1)),(IR . A)} is non empty finite set
{(IR . (FCR + 1))} is non empty trivial finite 1 -element set
{{(IR . (FCR + 1)),(IR . A)},{(IR . (FCR + 1))}} is non empty finite V34() set
IR . A is Element of the carrier of R
IR . (FCR + 1) is Element of the carrier of R
[(IR . (FCR + 1)),(IR . A)] is V1() Element of [: the carrier of R, the carrier of R:]
{(IR . (FCR + 1)),(IR . A)} is non empty finite set
{(IR . (FCR + 1))} is non empty trivial finite 1 -element set
{{(IR . (FCR + 1)),(IR . A)},{(IR . (FCR + 1))}} is non empty finite V34() set
IR . A is Element of the carrier of R
[(IR . FCR),(IR . A)] is V1() Element of [: the carrier of R, the carrier of R:]
{(IR . FCR),(IR . A)} is non empty finite set
{(IR . FCR)} is non empty trivial finite 1 -element set
{{(IR . FCR),(IR . A)},{(IR . FCR)}} is non empty finite V34() set
IR . (FCR + 1) is Element of the carrier of R
[(IR . (FCR + 1)),(IR . FCR)] is V1() Element of [: the carrier of R, the carrier of R:]
{(IR . (FCR + 1)),(IR . FCR)} is non empty finite set
{(IR . (FCR + 1))} is non empty trivial finite 1 -element set
{{(IR . (FCR + 1)),(IR . FCR)},{(IR . (FCR + 1))}} is non empty finite V34() set
[(IR . (FCR + 1)),(IR . A)] is V1() Element of [: the carrier of R, the carrier of R:]
{(IR . (FCR + 1)),(IR . A)} is non empty finite set
{{(IR . (FCR + 1)),(IR . A)},{(IR . (FCR + 1))}} is non empty finite V34() set
IR . A is Element of the carrier of R
IR . (FCR + 1) is Element of the carrier of R
[(IR . (FCR + 1)),(IR . A)] is V1() Element of [: the carrier of R, the carrier of R:]
{(IR . (FCR + 1)),(IR . A)} is non empty finite set
{(IR . (FCR + 1))} is non empty trivial finite 1 -element set
{{(IR . (FCR + 1)),(IR . A)},{(IR . (FCR + 1))}} is non empty finite V34() set
IR . A is Element of the carrier of R
IR . (FCR + 1) is Element of the carrier of R
[(IR . (FCR + 1)),(IR . A)] is V1() Element of [: the carrier of R, the carrier of R:]
{(IR . (FCR + 1)),(IR . A)} is non empty finite set
{(IR . (FCR + 1))} is non empty trivial finite 1 -element set
{{(IR . (FCR + 1)),(IR . A)},{(IR . (FCR + 1))}} is non empty finite V34() set
FCR is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() ext-real non negative set
IR . FCR is Element of the carrier of R
FCR + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real positive non negative V49() V72() V73() V74() V75() V76() V77() V293() V294() V295() V296() V297() Element of NAT
A is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() ext-real non negative set
IR . A is Element of the carrier of R
IR . (FCR + 1) is Element of the carrier of R
[(IR . (FCR + 1)),(IR . A)] is V1() Element of [: the carrier of R, the carrier of R:]
{(IR . (FCR + 1)),(IR . A)} is non empty finite set
{(IR . (FCR + 1))} is non empty trivial finite 1 -element set
{{(IR . (FCR + 1)),(IR . A)},{(IR . (FCR + 1))}} is non empty finite V34() set
R is non empty RelStr
the carrier of R is non empty set
[:NAT, the carrier of R:] is non empty non trivial Relation-like non finite set
bool [:NAT, the carrier of R:] is non empty non trivial non finite cup-closed diff-closed preBoolean set
R is non empty transitive RelStr
the carrier of R is non empty set
[:NAT, the carrier of R:] is non empty non trivial Relation-like non finite set
bool [:NAT, the carrier of R:] is non empty non trivial non finite cup-closed diff-closed preBoolean set
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is non empty Relation-like set
bool [: the carrier of R, the carrier of R:] is non empty cup-closed diff-closed preBoolean set
IR is non empty Relation-like NAT -defined the carrier of R -valued Function-like total V18( NAT , the carrier of R) Element of bool [:NAT, the carrier of R:]
IR . 0 is Element of the carrier of R
FCR is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() ext-real non negative set
IR . FCR is Element of the carrier of R
[(IR . 0),(IR . FCR)] is V1() Element of [: the carrier of R, the carrier of R:]
{(IR . 0),(IR . FCR)} is non empty finite set
{(IR . 0)} is non empty trivial finite 1 -element set
{{(IR . 0),(IR . FCR)},{(IR . 0)}} is non empty finite V34() set
FCR is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() ext-real non negative set
IR . FCR is Element of the carrier of R
FCR + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real positive non negative V49() V72() V73() V74() V75() V76() V77() V293() V294() V295() V296() V297() Element of NAT
A is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() ext-real non negative set
IR . (FCR + 1) is Element of the carrier of R
IR . A is Element of the carrier of R
[(IR . (FCR + 1)),(IR . A)] is V1() Element of [: the carrier of R, the carrier of R:]
{(IR . (FCR + 1)),(IR . A)} is non empty finite set
{(IR . (FCR + 1))} is non empty trivial finite 1 -element set
{{(IR . (FCR + 1)),(IR . A)},{(IR . (FCR + 1))}} is non empty finite V34() set
IR . (FCR + 1) is Element of the carrier of R
IR . A is Element of the carrier of R
[(IR . (FCR + 1)),(IR . A)] is V1() Element of [: the carrier of R, the carrier of R:]
{(IR . (FCR + 1)),(IR . A)} is non empty finite set
{(IR . (FCR + 1))} is non empty trivial finite 1 -element set
{{(IR . (FCR + 1)),(IR . A)},{(IR . (FCR + 1))}} is non empty finite V34() set
IR . A is Element of the carrier of R
[(IR . FCR),(IR . A)] is V1() Element of [: the carrier of R, the carrier of R:]
{(IR . FCR),(IR . A)} is non empty finite set
{(IR . FCR)} is non empty trivial finite 1 -element set
{{(IR . FCR),(IR . A)},{(IR . FCR)}} is non empty finite V34() set
IR . (FCR + 1) is Element of the carrier of R
[(IR . (FCR + 1)),(IR . FCR)] is V1() Element of [: the carrier of R, the carrier of R:]
{(IR . (FCR + 1)),(IR . FCR)} is non empty finite set
{(IR . (FCR + 1))} is non empty trivial finite 1 -element set
{{(IR . (FCR + 1)),(IR . FCR)},{(IR . (FCR + 1))}} is non empty finite V34() set
[(IR . (FCR + 1)),(IR . A)] is V1() Element of [: the carrier of R, the carrier of R:]
{(IR . (FCR + 1)),(IR . A)} is non empty finite set
{{(IR . (FCR + 1)),(IR . A)},{(IR . (FCR + 1))}} is non empty finite V34() set
IR . (FCR + 1) is Element of the carrier of R
IR . A is Element of the carrier of R
[(IR . (FCR + 1)),(IR . A)] is V1() Element of [: the carrier of R, the carrier of R:]
{(IR . (FCR + 1)),(IR . A)} is non empty finite set
{(IR . (FCR + 1))} is non empty trivial finite 1 -element set
{{(IR . (FCR + 1)),(IR . A)},{(IR . (FCR + 1))}} is non empty finite V34() set
IR . (FCR + 1) is Element of the carrier of R
IR . A is Element of the carrier of R
[(IR . (FCR + 1)),(IR . A)] is V1() Element of [: the carrier of R, the carrier of R:]
{(IR . (FCR + 1)),(IR . A)} is non empty finite set
{(IR . (FCR + 1))} is non empty trivial finite 1 -element set
{{(IR . (FCR + 1)),(IR . A)},{(IR . (FCR + 1))}} is non empty finite V34() set
FCR is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() ext-real non negative set
IR . FCR is Element of the carrier of R
FCR + 1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real positive non negative V49() V72() V73() V74() V75() V76() V77() V293() V294() V295() V296() V297() Element of NAT
A is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() ext-real non negative set
IR . (FCR + 1) is Element of the carrier of R
IR . A is Element of the carrier of R
[(IR . (FCR + 1)),(IR . A)] is V1() Element of [: the carrier of R, the carrier of R:]
{(IR . (FCR + 1)),(IR . A)} is non empty finite set
{(IR . (FCR + 1))} is non empty trivial finite 1 -element set
{{(IR . (FCR + 1)),(IR . A)},{(IR . (FCR + 1))}} is non empty finite V34() set
R is non empty transitive RelStr
the carrier of R is non empty set
[:NAT, the carrier of R:] is non empty non trivial Relation-like non finite set
bool [:NAT, the carrier of R:] is non empty non trivial non finite cup-closed diff-closed preBoolean set
IR is non empty Relation-like NAT -defined the carrier of R -valued Function-like total V18( NAT , the carrier of R) Element of bool [:NAT, the carrier of R:]
the InternalRel of R is Relation-like the carrier of R -defined the carrier of R -valued Element of bool [: the carrier of R, the carrier of R:]
[: the carrier of R, the carrier of R:] is non empty Relation-like set
bool [: the carrier of R, the carrier of R:] is non empty cup-closed diff-closed preBoolean set
dom IR is non empty V72() V73() V74() V75() V76() V77() V293() V295() Element of bool NAT
rng IR is non empty set
FCR is set
the InternalRel of R -Seg FCR is set
( the InternalRel of R -Seg FCR) /\ (rng IR) is set
A is set
IR . A is set
zz is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() ext-real non negative set
IR . zz is Element of the carrier of R
zz is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() ext-real non negative set
IR . zz is Element of the carrier of R
[(IR . zz),(IR . zz)] is V1() Element of [: the carrier of R, the carrier of R:]
{(IR . zz),(IR . zz)} is non empty finite set
{(IR . zz)} is non empty trivial finite 1 -element set
{{(IR . zz),(IR . zz)},{(IR . zz)}} is non empty finite V34() set
Z is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of NAT
IR . Z is Element of the carrier of R
R is set
bool R is non empty cup-closed diff-closed preBoolean set
[:R,R:] is Relation-like set
bool [:R,R:] is non empty cup-closed diff-closed preBoolean set
IR is Element of R
{IR} is non empty trivial finite 1 -element set
<*IR*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like finite-support set
CR is finite Element of bool R
FIR is Relation-like R -defined R -valued total V18(R,R) reflexive antisymmetric transitive Element of bool [:R,R:]
SgmX (FIR,CR) is Relation-like NAT -defined R -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of R
len (SgmX (FIR,CR)) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of NAT
card CR is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of omega
rng (SgmX (FIR,CR)) is finite set
R is epsilon-transitive epsilon-connected ordinal set
IR is Relation-like R -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set
support IR is finite Element of bool R
bool R is non empty cup-closed diff-closed preBoolean set
RelIncl R is Relation-like R -defined R -valued total V18(R,R) reflexive antisymmetric connected transitive well_founded well-ordering Element of bool [:R,R:]
[:R,R:] is Relation-like set
bool [:R,R:] is non empty cup-closed diff-closed preBoolean set
SgmX ((RelIncl R),(support IR)) is Relation-like NAT -defined R -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of R
IR * (SgmX ((RelIncl R),(support IR))) is Relation-like NAT -defined NAT -valued RAT -valued Function-like finite complex-valued ext-real-valued real-valued natural-valued finite-support Element of bool [:NAT,NAT:]
dom IR is Element of bool R
rng IR is V72() V73() V74() V75() V76() V77() V295() Element of bool REAL
[:R,NAT:] is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
bool [:R,NAT:] is non empty cup-closed diff-closed preBoolean set
FIR is Relation-like R -defined NAT -valued Function-like total V18(R, NAT ) complex-valued ext-real-valued real-valued natural-valued Element of bool [:R,NAT:]
FCR is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued Cardinal-yielding finite-support FinSequence of NAT
Sum FCR is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of NAT
A is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() ext-real non negative set
CR is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() ext-real non negative set
FCR is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued Cardinal-yielding finite-support FinSequence of NAT
Sum FCR is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of NAT
FIR is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() ext-real non negative set
A is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued Cardinal-yielding finite-support FinSequence of NAT
Sum A is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of NAT
R is epsilon-transitive epsilon-connected ordinal set
bool R is non empty cup-closed diff-closed preBoolean set
RelIncl R is Relation-like R -defined R -valued total V18(R,R) reflexive antisymmetric connected transitive well_founded well-ordering Element of bool [:R,R:]
[:R,R:] is Relation-like set
bool [:R,R:] is non empty cup-closed diff-closed preBoolean set
IR is Relation-like R -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set
support IR is finite Element of bool R
SgmX ((RelIncl R),(support IR)) is Relation-like NAT -defined R -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of R
IR * (SgmX ((RelIncl R),(support IR))) is Relation-like NAT -defined NAT -valued RAT -valued Function-like finite complex-valued ext-real-valued real-valued natural-valued finite-support Element of bool [:NAT,NAT:]
CR is finite Element of bool R
(support IR) \/ CR is finite Element of bool R
SgmX ((RelIncl R),((support IR) \/ CR)) is Relation-like NAT -defined R -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of R
IR * (SgmX ((RelIncl R),((support IR) \/ CR))) is Relation-like NAT -defined NAT -valued RAT -valued Function-like finite complex-valued ext-real-valued real-valued natural-valued finite-support Element of bool [:NAT,NAT:]
FIR is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued Cardinal-yielding finite-support FinSequence of NAT
FCR is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued Cardinal-yielding finite-support FinSequence of NAT
Sum FIR is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of NAT
Sum FCR is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of NAT
((support IR) \/ CR) \ (support IR) is finite Element of bool R
SgmX ((RelIncl R),(((support IR) \/ CR) \ (support IR))) is Relation-like NAT -defined R -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of R
(SgmX ((RelIncl R),(support IR))) ^ (SgmX ((RelIncl R),(((support IR) \/ CR) \ (support IR)))) is Relation-like NAT -defined R -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of R
IR * ((SgmX ((RelIncl R),(support IR))) ^ (SgmX ((RelIncl R),(((support IR) \/ CR) \ (support IR))))) is Relation-like NAT -defined NAT -valued RAT -valued Function-like finite complex-valued ext-real-valued real-valued natural-valued finite-support Element of bool [:NAT,NAT:]
dom IR is Element of bool R
field (RelIncl R) is set
rng (SgmX ((RelIncl R),((support IR) \/ CR))) is finite set
rng (SgmX ((RelIncl R),(support IR))) is finite set
rng (SgmX ((RelIncl R),(((support IR) \/ CR) \ (support IR)))) is finite set
rng ((SgmX ((RelIncl R),(support IR))) ^ (SgmX ((RelIncl R),(((support IR) \/ CR) \ (support IR))))) is finite set
(support IR) \/ (((support IR) \/ CR) \ (support IR)) is finite Element of bool R
S0max is non empty epsilon-transitive epsilon-connected ordinal set
rng IR is V72() V73() V74() V75() V76() V77() V295() Element of bool REAL
[:S0max,REAL:] is non empty non trivial Relation-like non finite complex-valued ext-real-valued real-valued set
bool [:S0max,REAL:] is non empty non trivial non finite cup-closed diff-closed preBoolean set
S02 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
rng S02 is finite set
b0t is non empty Relation-like S0max -defined REAL -valued Function-like total V18(S0max, REAL ) complex-valued ext-real-valued real-valued Element of bool [:S0max,REAL:]
rng b0t is non empty V72() V73() V74() Element of bool REAL
(support IR) \/ (support IR) is finite Element of bool R
((support IR) \/ (support IR)) \/ CR is finite Element of bool R
(support IR) \/ ((support IR) \/ CR) is finite Element of bool R
len ((SgmX ((RelIncl R),(support IR))) ^ (SgmX ((RelIncl R),(((support IR) \/ CR) \ (support IR))))) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of NAT
a0 is Relation-like NAT -defined S0max -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of S0max
len a0 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of NAT
i0 is Relation-like NAT -defined S0max -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of S0max
len i0 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of NAT
(len a0) + (len i0) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of NAT
card (support IR) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of omega
(card (support IR)) + (len i0) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of NAT
card (((support IR) \/ CR) \ (support IR)) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of omega
(card (support IR)) + (card (((support IR) \/ CR) \ (support IR))) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of NAT
card ((support IR) \/ CR) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of omega
len (SgmX ((RelIncl R),((support IR) \/ CR))) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of NAT
dom (SgmX ((RelIncl R),((support IR) \/ CR))) is finite V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of bool NAT
dom ((SgmX ((RelIncl R),(support IR))) ^ (SgmX ((RelIncl R),(((support IR) \/ CR) \ (support IR))))) is finite V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of bool NAT
rng a0 is finite set
rng i0 is finite set
S is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued finite-support FinSequence of REAL
b0 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued finite-support FinSequence of REAL
dom i0 is finite V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of bool NAT
b0t * i0 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued finite-support FinSequence of REAL
dom (b0t * i0) is finite V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of bool NAT
Seg (len i0) is finite len i0 -element V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of bool NAT
(len i0) |-> 0 is Relation-like NAT -defined NAT -valued Function-like Function-yielding finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued natural-valued Cardinal-yielding FinSequence-yielding finite-support Element of (len i0) -tuples_on NAT
(len i0) -tuples_on NAT is FinSequenceSet of NAT
NAT * is non empty functional FinSequence-membered FinSequenceSet of NAT
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of NAT * : len b1 = len i0 } is set
(Seg (len i0)) --> 0 is Relation-like Seg (len i0) -defined RAT -valued INT -valued {0} -valued Function-like total V18( Seg (len i0),{0}) finite complex-valued ext-real-valued real-valued natural-valued finite-support Element of bool [:(Seg (len i0)),{0}:]
{0} is non empty trivial functional finite V34() 1 -element V72() V73() V74() V75() V76() V77() V293() V294() V295() V296() V297() set
[:(Seg (len i0)),{0}:] is Relation-like RAT -valued INT -valued finite complex-valued ext-real-valued real-valued natural-valued set
bool [:(Seg (len i0)),{0}:] is non empty finite V34() cup-closed diff-closed preBoolean set
dom ((len i0) |-> 0) is finite V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of bool NAT
a is set
i0 . a is set
b0t . (i0 . a) is V42() V43() ext-real Element of REAL
(b0t * i0) . a is V42() V43() ext-real Element of REAL
((len i0) |-> 0) . a is epsilon-transitive epsilon-connected ordinal natural finite cardinal FinSequence-like V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of NAT
(len i0) |-> 0 is Relation-like NAT -defined REAL -valued Function-like Function-yielding finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence-yielding finite-support Element of (len i0) -tuples_on REAL
(len i0) -tuples_on REAL is FinSequenceSet of REAL
REAL * is non empty functional FinSequence-membered FinSequenceSet of REAL
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of REAL * : len b1 = len i0 } is set
b0t * a0 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued finite-support FinSequence of REAL
(b0t * a0) ^ (b0t * i0) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued finite-support FinSequence of REAL
Sum b0 is V42() V43() ext-real Element of REAL
Sum (b0t * a0) is V42() V43() ext-real Element of REAL
Sum (b0t * i0) is V42() V43() ext-real Element of REAL
(Sum (b0t * a0)) + (Sum (b0t * i0)) is V42() V43() ext-real Element of REAL
(Sum FIR) + 0 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() V44() ext-real non negative V49() V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of NAT
R is epsilon-transitive epsilon-connected ordinal set
IR is Relation-like R -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set
CR is Relation-like R -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set
IR + CR is Relation-like R -defined RAT -valued Function-like total complex-valued ext-real-valued real-valued natural-valued finite-support set
(R,(IR + CR)) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() ext-real non negative set
(R,IR) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() ext-real non negative set
(R,CR) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43() ext-real non negative set
(R,IR) + (R,CR) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V42() V43