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

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:]

{ [b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

{ 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

{ b

(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

{ b

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