:: BAGORDER semantic presentation

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

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

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

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

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

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

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

{ [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

RelStr(# NAT,NATOrd #) is non empty strict RelStr

Sum () is V42() V43() ext-real Element of REAL

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

IR \ {CR} is Element of bool IR

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

IR is set

support (R | IR) is set

CR is set
(R | IR) . CR is set
dom (R | IR) is set
R . CR is set

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

{ } is set
Seg (len R) is finite len R -element V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of bool NAT

is non empty trivial functional finite V34() 1 -element V72() V73() V74() V75() V76() V77() V293() V294() V295() V296() V297() set

bool [:(Seg (len R)),:] 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

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

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

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
{ 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

dom FCR 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 . 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

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,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

(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

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

(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

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

{ 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

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

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

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

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

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

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

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

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

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

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

IR . zz is Element of the carrier of R

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

[:R,R:] is Relation-like set

IR is Element of R
{IR} is non empty trivial finite 1 -element set

CR is finite Element of bool 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

support IR is finite Element of bool R

[:R,R:] is Relation-like set

dom IR is Element of bool R
rng IR is V72() V73() V74() V75() V76() V77() V295() Element of bool REAL

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

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

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,R:] is Relation-like set

support IR is finite Element of bool R

CR is finite Element of bool R
(support IR) \/ CR is finite Element of bool R

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 ((),(support IR))) ^ (SgmX ((),(((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 ((),(support IR))) ^ (SgmX ((),(((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
dom IR is Element of bool R
field () is set
rng (SgmX ((),((support IR) \/ CR))) is finite set
rng (SgmX ((),(support IR))) is finite set
rng (SgmX ((),(((support IR) \/ CR) \ (support IR)))) is finite set
rng ((SgmX ((),(support IR))) ^ (SgmX ((),(((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

bool [:S0max,REAL:] is non empty non trivial non finite cup-closed diff-closed preBoolean 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 ((),(support IR))) ^ (SgmX ((),(((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

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

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 ((),((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 ((),((support IR) \/ CR))) is finite V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of bool NAT
dom ((SgmX ((),(support IR))) ^ (SgmX ((),(((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

dom i0 is finite V72() V73() V74() V75() V76() V77() V295() V296() V297() Element of bool NAT

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) -tuples_on NAT is FinSequenceSet of NAT

{ } is set

is non empty trivial functional finite V34() 1 -element V72() V73() V74() V75() V76() V77() V293() V294() V295() V296() V297() set

bool [:(Seg (len i0)),:] 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) -tuples_on REAL is FinSequenceSet of REAL

{ } is set

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