:: COMPOS_0 semantic presentation

REAL is non empty non trivial V5() V36() V71() V72() V73() V77() set
NAT is non empty non trivial V5() epsilon-transitive epsilon-connected ordinal limit_ordinal V36() cardinal limit_cardinal countable denumerable V71() V72() V73() V74() V75() V76() V77() Element of bool REAL
bool REAL is non empty non trivial V5() V36() set
omega is non empty non trivial V5() epsilon-transitive epsilon-connected ordinal limit_ordinal V36() cardinal limit_cardinal countable denumerable V71() V72() V73() V74() V75() V76() V77() set
bool omega is non empty non trivial V5() V36() set
bool NAT is non empty non trivial V5() V36() set
COMPLEX is non empty non trivial V5() V36() V71() V77() set
RAT is non empty non trivial V5() V36() V71() V72() V73() V74() V77() set
INT is non empty non trivial V5() V36() V71() V72() V73() V74() V75() V77() set
{} is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-yielding V35() V36() V37() V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V47() Cardinal-yielding countable V57() V58() integer complex-valued ext-real-valued real-valued natural-valued V65() decreasing non-decreasing non-increasing V71() V72() V73() V74() V75() V76() V77() V92() V93() V96() V100() set
the empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-yielding V35() V36() V37() V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V47() Cardinal-yielding countable V57() V58() integer complex-valued ext-real-valued real-valued natural-valued V65() decreasing non-decreasing non-increasing V71() V72() V73() V74() V75() V76() V77() V92() V93() V96() V100() set is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-yielding V35() V36() V37() V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V47() Cardinal-yielding countable V57() V58() integer complex-valued ext-real-valued real-valued natural-valued V65() decreasing non-decreasing non-increasing V71() V72() V73() V74() V75() V76() V77() V92() V93() V96() V100() set
2 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer V60() V71() V72() V73() V74() V75() V76() Element of NAT
1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer V60() V71() V72() V73() V74() V75() V76() Element of NAT
3 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer V60() V71() V72() V73() V74() V75() V76() Element of NAT
product {} is non empty functional with_common_domain product-like set
{{}} is non empty trivial functional V36() V40() 1 -element with_common_domain countable V71() V72() V73() V74() V75() V76() set
NAT * is non empty functional FinSequence-membered set
0 is empty trivial Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-yielding V35() V36() V37() V40() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V47() Cardinal-yielding countable V57() V58() integer V60() complex-valued ext-real-valued real-valued natural-valued V65() decreasing non-decreasing non-increasing V71() V72() V73() V74() V75() V76() V77() V92() V93() V96() V100() Element of NAT
[0,{},{}] is V7() triple set
[0,{}] is non empty V7() set
{0,{}} is non empty functional V36() V40() countable V71() V72() V73() V74() V75() V76() set
{0} is non empty trivial functional V36() V40() 1 -element with_common_domain countable V71() V72() V73() V74() V75() V76() set
{{0,{}},{0}} is non empty V4() V5() V36() V40() countable set
[[0,{}],{}] is non empty V7() set
{[0,{}],{}} is non empty V36() countable set
{[0,{}]} is non empty trivial V4() V5() Relation-like Function-like constant V36() 1 -element countable V93() set
{{[0,{}],{}},{[0,{}]}} is non empty V4() V5() V36() V40() countable set
{[0,{},{}]} is non empty trivial V36() 1 -element countable set
{{}} * is non empty functional FinSequence-membered set
[:NAT,(NAT *),({{}} *):] is non empty set
[:NAT,(NAT *):] is non empty non trivial V5() Relation-like V36() set
[:[:NAT,(NAT *):],({{}} *):] is non empty non trivial V5() Relation-like V36() set
{0} is non empty trivial functional V36() V40() 1 -element with_common_domain countable V71() V72() V73() V74() V75() V76() Element of bool NAT
[:{0},{{}},{{}}:] is non empty V36() countable set
[:{0},{{}}:] is non empty Relation-like RAT -valued INT -valued V36() countable complex-valued ext-real-valued real-valued natural-valued set
[:[:{0},{{}}:],{{}}:] is non empty Relation-like RAT -valued INT -valued V36() countable complex-valued ext-real-valued real-valued natural-valued set
[1,{},{}] is V7() triple set
[1,{}] is non empty V7() set
{1,{}} is non empty V36() V40() countable V71() V72() V73() V74() V75() V76() set
{1} is non empty trivial V4() V5() V36() V40() 1 -element countable V71() V72() V73() V74() V75() V76() set
{{1,{}},{1}} is non empty V4() V5() V36() V40() countable set
[[1,{}],{}] is non empty V7() set
{[1,{}],{}} is non empty V36() countable set
{[1,{}]} is non empty trivial V4() V5() Relation-like Function-like constant V36() 1 -element countable V93() set
{{[1,{}],{}},{[1,{}]}} is non empty V4() V5() V36() V40() countable set
{[1,{},{}]} is non empty trivial V36() 1 -element countable set
{{}} * is non empty functional FinSequence-membered set
[:NAT,(NAT *),({{}} *):] is non empty set
[:NAT,(NAT *):] is non empty non trivial V5() Relation-like V36() set
[:[:NAT,(NAT *):],({{}} *):] is non empty non trivial V5() Relation-like V36() set
{1} is non empty trivial V4() V5() V36() V40() 1 -element countable V71() V72() V73() V74() V75() V76() Element of bool NAT
[:{1},{{}},{{}}:] is non empty V36() countable set
[:{1},{{}}:] is non empty Relation-like RAT -valued INT -valued V36() countable complex-valued ext-real-valued real-valued natural-valued set
[:[:{1},{{}}:],{{}}:] is non empty Relation-like RAT -valued INT -valued V36() countable complex-valued ext-real-valued real-valued natural-valued set
c₁ is non empty () set
i is Element of c₁
i `3_3 is set
I is non empty set
I * is non empty functional FinSequence-membered set
[:NAT,(NAT *),(I *):] is non empty set
[:NAT,(NAT *):] is non empty non trivial V5() Relation-like V36() set
[:[:NAT,(NAT *):],(I *):] is non empty non trivial V5() Relation-like V36() set
i `2_3 is set
K41(i) is set
K41(i) `3_3 is set
I is non empty set
I * is non empty functional FinSequence-membered set
[:NAT,(NAT *),(I *):] is non empty set
[:NAT,(NAT *):] is non empty non trivial V5() Relation-like V36() set
[:[:NAT,(NAT *):],(I *):] is non empty non trivial V5() Relation-like V36() set
c<sub>1</sub> is non empty () set
i is Element of c<sub>1</sub>
i `3_3 is Relation-like Function-like set
I is non empty set
I * is non empty functional FinSequence-membered set
[:NAT,(NAT *),(I *):] is non empty set
[:NAT,(NAT *):] is non empty non trivial V5() Relation-like V36() set
[:[:NAT,(NAT *):],(I *):] is non empty non trivial V5() Relation-like V36() set
i `2_3 is Relation-like Function-like set
K41(i) is set
K41(i) `3_3 is set
I is non empty set
I * is non empty functional FinSequence-membered set
[:NAT,(NAT *),(I *):] is non empty set
[:NAT,(NAT *):] is non empty non trivial V5() Relation-like V36() set
[:[:NAT,(NAT *):],(I *):] is non empty non trivial V5() Relation-like V36() set
c₁ is non empty () set
i is Element of c₁
i `1_3 is set
K41(i) is set
K41(K41(i)) is set
I is non empty set
I * is non empty functional FinSequence-membered set
[:NAT,(NAT *),(I *):] is non empty set
[:NAT,(NAT *):] is non empty non trivial V5() Relation-like V36() set
[:[:NAT,(NAT *):],(I *):] is non empty non trivial V5() Relation-like V36() set
c<sub>1</sub> is set
i is non empty set
i * is non empty functional FinSequence-membered set
[:NAT,(NAT *),(i *):] is non empty set
[:NAT,(NAT *):] is non empty non trivial V5() Relation-like V36() set
[:[:NAT,(NAT *):],(i *):] is non empty non trivial V5() Relation-like V36() set
c<sub>1</sub> is Relation-like () set
proj1_3 c<sub>1</sub> is set
proj1 c<sub>1</sub> is set
proj1 (proj1 c<sub>1</sub>) is set
c<sub>1</sub> is non empty Relation-like () set
(c<sub>1</sub>) is set
proj1_3 c<sub>1</sub> is set
proj1 c<sub>1</sub> is non empty set
proj1 (proj1 c<sub>1</sub>) is set
I is non empty set
I * is non empty functional FinSequence-membered set
[:NAT,(NAT *),(I *):] is non empty set
[:NAT,(NAT *):] is non empty non trivial V5() Relation-like V36() set
[:[:NAT,(NAT *):],(I *):] is non empty non trivial V5() Relation-like V36() set
i is Relation-like set
c<sub>1</sub> is non empty Relation-like () set
i is Element of c<sub>1</sub>
i `1_3 is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer set
K41(i) is set
K41(K41(i)) is set
(c₁) is non empty set
proj1_3 c₁ is set
proj1 c₁ is non empty set
proj1 (proj1 c₁) is set
I is non empty set
I * is non empty functional FinSequence-membered set
[:NAT,(NAT *),(I *):] is non empty set
[:NAT,(NAT *):] is non empty non trivial V5() Relation-like V36() set
[:[:NAT,(NAT *):],(I *):] is non empty non trivial V5() Relation-like V36() set
i `2_3 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like countable V93() set
K41(i) `3_3 is set
i `3_3 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like countable V93() set
[(i `1_3),(i `2_3),(i `3_3)] is V7() triple set
[(i `1_3),(i `2_3)] is non empty V7() set
{(i `1_3),(i `2_3)} is non empty V36() V40() countable set
{(i `1_3)} is non empty trivial V36() V40() 1 -element countable V71() V72() V73() V74() V75() V76() set
{{(i `1_3),(i `2_3)},{(i `1_3)}} is non empty V4() V5() V36() V40() countable set
[[(i `1_3),(i `2_3)],(i `3_3)] is non empty V7() set
{[(i `1_3),(i `2_3)],(i `3_3)} is non empty V36() countable set
{[(i `1_3),(i `2_3)]} is non empty trivial V4() V5() Relation-like Function-like constant V36() 1 -element countable V93() set
{{[(i `1_3),(i `2_3)],(i `3_3)},{[(i `1_3),(i `2_3)]}} is non empty V4() V5() V36() V40() countable set
c<sub>1</sub> is non empty Relation-like () set
(c<sub>1</sub>) is non empty set
proj1_3 c<sub>1</sub> is set
proj1 c<sub>1</sub> is non empty set
proj1 (proj1 c<sub>1</sub>) is set
i is Element of (c<sub>1</sub>)
{ (b<sub>1</sub> `2_3) where b₁ is Element of c₁ : (c₁,b₁) = i } is set
{ (b₁ `3_3) where b<sub>1</sub> is Element of c<sub>1</sub> : (c<sub>1</sub>,b<sub>1</sub>) = i } is set
c<sub>1</sub> is non empty Relation-like () set
(c<sub>1</sub>) is non empty set
proj1_3 c<sub>1</sub> is set
proj1 c<sub>1</sub> is non empty set
proj1 (proj1 c<sub>1</sub>) is set
i is Element of (c<sub>1</sub>)
(c<sub>1</sub>,i) is set
{ (b<sub>1</sub> `3_3) where b₁ is Element of c₁ : (c₁,b₁) = i } is set
I is set
a is Element of c₁
a `3_3 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like countable V93() set
(c<sub>1</sub>,a) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer Element of (c<sub>1</sub>)
K41(a) is set
K41(K41(a)) is set
(c<sub>1</sub>,i) is set
{ (b<sub>1</sub> `2_3) where b₁ is Element of c₁ : (c₁,b₁) = i } is set
I is set
[i,I] is non empty V7() set
{i,I} is non empty V36() countable set
{i} is non empty trivial V36() 1 -element countable set
{{i,I},{i}} is non empty V4() V5() V36() V40() countable set
a is set
[[i,I],a] is non empty V7() set
{[i,I],a} is non empty V36() countable set
{[i,I]} is non empty trivial V4() V5() Relation-like Function-like constant V36() 1 -element countable V93() set
{{[i,I],a},{[i,I]}} is non empty V4() V5() V36() V40() countable set
[i,I,a] is V7() triple set
II is Element of c₁
(c₁,II) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer Element of (c₁)
K41(II) is set
K41(K41(II)) is set
II `2_3 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like countable V93() set
K41(II) `3_3 is set
c₆ is set
J is Element of c₁
J `2_3 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like countable V93() set
K41(J) is set
K41(J) `3_3 is set
(c₁,J) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer Element of (c₁)
K41(K41(J)) is set
({[0,{},{}]}) is non empty set
proj1_3 {[0,{},{}]} is set
proj1 {[0,{},{}]} is non empty trivial V36() 1 -element countable set
proj1 (proj1 {[0,{},{}]}) is set
{0} is non empty trivial functional V36() V40() 1 -element with_common_domain countable V71() V72() V73() V74() V75() V76() Element of bool NAT
c₁ is Element of ({[0,{},{}]})
({[0,{},{}]},c₁) is non empty functional set
{ (b₁ `2_3) where b<sub>1</sub> is Element of {[0,{},{}]} : ({[0,{},{}]},b<sub>1</sub>) = c<sub>1</sub> } is set
I is set
[0,0,0] is V7() triple Element of [:NAT,NAT,NAT:]
[:NAT,NAT,NAT:] is non empty set
[:NAT,NAT:] is non empty non trivial V5() Relation-like RAT -valued INT -valued V36() complex-valued ext-real-valued real-valued natural-valued set
[:[:NAT,NAT:],NAT:] is non empty non trivial V5() Relation-like RAT -valued INT -valued V36() complex-valued ext-real-valued real-valued natural-valued set
[0,0] is non empty V7() set
{0,0} is non empty functional V36() V40() countable V71() V72() V73() V74() V75() V76() set
{{0,0},{0}} is non empty V4() V5() V36() V40() countable set
[[0,0],0] is non empty V7() set
{[0,0],0} is non empty V36() countable set
{[0,0]} is non empty trivial V4() V5() Relation-like Function-like constant V36() 1 -element countable V93() set
{{[0,0],0},{[0,0]}} is non empty V4() V5() V36() V40() countable set
a is Element of {[0,{},{}]}
a `2_3 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like countable V93() set
K41(a) is set
K41(a) `3_3 is set
({[0,{},{}]},a) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer Element of ({[0,{},{}]})
K41(K41(a)) is set
I is set
a is Element of {[0,{},{}]}
a `2_3 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like countable V93() set
K41(a) is set
K41(a) `3_3 is set
({[0,{},{}]},a) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer Element of ({[0,{},{}]})
K41(K41(a)) is set
c<sub>1</sub> is Element of ({[0,{},{}]})
({[0,{},{}]},c<sub>1</sub>) is non empty functional set
{ (b<sub>1</sub> `2_3) where b₁ is Element of {[0,{},{}]} : ({[0,{},{}]},b₁) = c₁ } is set
i is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued set
proj1 i is set
I is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued set
proj1 I is set
a is set
[c₁,i,a] is V7() triple set
[c₁,i] is non empty V7() set
{c₁,i} is non empty V36() countable set
{c₁} is non empty trivial V36() 1 -element countable set
{{c₁,i},{c₁}} is non empty V4() V5() V36() V40() countable set
[[c₁,i],a] is non empty V7() set
{[c₁,i],a} is non empty V36() countable set
{[c₁,i]} is non empty trivial V4() V5() Relation-like Function-like constant V36() 1 -element countable V93() set
{{[c₁,i],a},{[c₁,i]}} is non empty V4() V5() V36() V40() countable set
[c₁,I,a] is V7() triple set
[c₁,I] is non empty V7() set
{c₁,I} is non empty V36() countable set
{{c₁,I},{c₁}} is non empty V4() V5() V36() V40() countable set
[[c₁,I],a] is non empty V7() set
{[c₁,I],a} is non empty V36() countable set
{[c₁,I]} is non empty trivial V4() V5() Relation-like Function-like constant V36() 1 -element countable V93() set
{{[c₁,I],a},{[c₁,I]}} is non empty V4() V5() V36() V40() countable set
c₁ is Element of {[0,{},{}]}
({[0,{},{}]},c₁) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer Element of ({[0,{},{}]})
K41(c₁) is set
K41(K41(c₁)) is set
i is Element of {[0,{},{}]}
({[0,{},{}]},i) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer Element of ({[0,{},{}]})
K41(i) is set
K41(K41(i)) is set
c₁ `2_3 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like countable V93() set
K41(c<sub>1</sub>) `3_3 is set
dom (c₁ `2_3) is V36() countable V71() V72() V73() V74() V75() V76() Element of bool NAT
i `2_3 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like countable V93() set
K41(i) `3_3 is set
dom (i `2_3) is V36() countable V71() V72() V73() V74() V75() V76() Element of bool NAT
c₁ is non empty trivial Relation-like V36() 1 -element countable () () () set
c₁ is non empty Relation-like () () set
(c₁) is non empty set
proj1_3 c₁ is set
proj1 c₁ is non empty set
proj1 (proj1 c₁) is set
i is Element of (c₁)
(c₁,i) is non empty functional set
{ (b₁ `2_3) where b<sub>1</sub> is Element of c<sub>1</sub> : (c<sub>1</sub>,b<sub>1</sub>) = i } is set
I is Relation-like Function-like set
a is Relation-like Function-like set
proj1 I is set
proj1 a is set
II is Element of c<sub>1</sub>
II `2_3 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like countable V93() set
K41(II) is set
K41(II) `3_3 is set
(c<sub>1</sub>,II) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer Element of (c<sub>1</sub>)
K41(K41(II)) is set
c<sub>6</sub> is Element of c<sub>1</sub>
c<sub>6</sub> `2_3 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like countable V93() set
K41(c₆) is set
K41(c₆) `3_3 is set
(c<sub>1</sub>,c<sub>6</sub>) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer Element of (c<sub>1</sub>)
K41(K41(c<sub>6</sub>)) is set
c<sub>1</sub> is non empty Relation-like () set
i is Element of c<sub>1</sub>
i `2_3 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like countable V93() set
K41(i) is set
K41(i) `3_3 is set
I is Relation-like Function-like set
a is non empty set
a * is non empty functional FinSequence-membered set
[:NAT,(NAT *),(a *):] is non empty set
[:NAT,(NAT *):] is non empty non trivial V5() Relation-like V36() set
[:[:NAT,(NAT *):],(a *):] is non empty non trivial V5() Relation-like V36() set
c<sub>1</sub> is non empty Relation-like () () set
i is Element of c<sub>1</sub>
i `2_3 is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like countable complex-valued ext-real-valued real-valued natural-valued V93() set
K41(i) is set
K41(i) `3_3 is set
dom (i `2_3) is V36() countable V71() V72() V73() V74() V75() V76() Element of bool NAT
(c₁,i) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer Element of (c₁)
(c₁) is non empty set
proj1_3 c₁ is set
proj1 c₁ is non empty set
proj1 (proj1 c₁) is set
K41(K41(i)) is set
(c₁,(c₁,i)) is non empty functional with_common_domain set
{ (b₁ `2_3) where b<sub>1</sub> is Element of c<sub>1</sub> : (c<sub>1</sub>,b<sub>1</sub>) = (c<sub>1</sub>,i) } is set
product" (c<sub>1</sub>,(c<sub>1</sub>,i)) is Relation-like Function-like set
I is set
(product" (c<sub>1</sub>,(c<sub>1</sub>,i))) . I is set
proj1 (product" (c<sub>1</sub>,(c<sub>1</sub>,i))) is set
{ (b<sub>1</sub> . I) where b<sub>1</sub> is Relation-like Function-like Element of (c<sub>1</sub>,(c<sub>1</sub>,i)) : verum } is set
a is set
II is Relation-like Function-like Element of (c<sub>1</sub>,(c<sub>1</sub>,i))
II . I is set
c<sub>6</sub> is Element of c<sub>1</sub>
c<sub>6</sub> `2_3 is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like countable complex-valued ext-real-valued real-valued natural-valued V93() set
K41(c₆) is set
K41(c₆) `3_3 is set
(c<sub>1</sub>,c<sub>6</sub>) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer Element of (c<sub>1</sub>)
K41(K41(c<sub>6</sub>)) is set
c<sub>1</sub> is non empty Relation-like () () set
i is non empty set
i * is non empty functional FinSequence-membered set
[:NAT,(NAT *),(i *):] is non empty set
[:NAT,(NAT *):] is non empty non trivial V5() Relation-like V36() set
[:[:NAT,(NAT *):],(i *):] is non empty non trivial V5() Relation-like V36() set
I is Element of c<sub>1</sub>
I `2_3 is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like countable complex-valued ext-real-valued real-valued natural-valued V93() set
K41(I) is set
K41(I) `3_3 is set
dom (I `2_3) is V36() countable V71() V72() V73() V74() V75() V76() Element of bool NAT
(c₁,I) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer Element of (c₁)
(c₁) is non empty set
proj1_3 c₁ is set
proj1 c₁ is non empty set
proj1 (proj1 c₁) is set
K41(K41(I)) is set
(c₁,(c₁,I)) is non empty functional with_common_domain set
{ (b₁ `2_3) where b<sub>1</sub> is Element of c<sub>1</sub> : (c<sub>1</sub>,b<sub>1</sub>) = (c<sub>1</sub>,I) } is set
product" (c<sub>1</sub>,(c<sub>1</sub>,I)) is Relation-like Function-like set
a is set
(product" (c<sub>1</sub>,(c<sub>1</sub>,I))) . a is set
proj1 (product" (c<sub>1</sub>,(c<sub>1</sub>,I))) is set
{ (b<sub>1</sub> . a) where b<sub>1</sub> is Relation-like Function-like Element of (c<sub>1</sub>,(c<sub>1</sub>,I)) : verum } is set
II is set
c<sub>6</sub> is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer V60() V71() V72() V73() V74() V75() V76() Element of NAT
(I `2_3) +* (a,c₆) is Relation-like NAT -defined NAT -valued RAT -valued Function-like V36() FinSequence-like FinSubsequence-like countable complex-valued ext-real-valued real-valued natural-valued V93() set
dom ((I `2_3) +* (a,c<sub>6</sub>)) is V36() countable V71() V72() V73() V74() V75() V76() Element of bool NAT
I `3_3 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like countable V93() set
[(c₁,I),(I `2_3),(I `3_3)] is V7() triple set
[(c₁,I),(I `2_3)] is non empty V7() set
{(c<sub>1</sub>,I),(I `2_3)} is non empty V36() V40() countable set
{(c₁,I)} is non empty trivial V36() V40() 1 -element countable V71() V72() V73() V74() V75() V76() set
{{(c₁,I),(I `2_3)},{(c<sub>1</sub>,I)}} is non empty V4() V5() V36() V40() countable set
[[(c<sub>1</sub>,I),(I `2_3)],(I `3_3)] is non empty V7() set
{[(c<sub>1</sub>,I),(I `2_3)],(I `3_3)} is non empty V36() countable set
{[(c<sub>1</sub>,I),(I `2_3)]} is non empty trivial V4() V5() Relation-like Function-like constant V36() 1 -element countable V93() set
{{[(c₁,I),(I `2_3)],(I `3_3)},{[(c₁,I),(I `2_3)]}} is non empty V4() V5() V36() V40() countable set
[(c<sub>1</sub>,I),((I `2_3) +* (a,c₆)),(I `3_3)] is V7() triple set
[(c<sub>1</sub>,I),((I `2_3) +* (a,c₆))] is non empty V7() set
{(c₁,I),((I `2_3) +* (a,c<sub>6</sub>))} is non empty V36() V40() countable set
{{(c<sub>1</sub>,I),((I `2_3) +* (a,c₆))},{(c₁,I)}} is non empty V4() V5() V36() V40() countable set
[[(c₁,I),((I `2_3) +* (a,c<sub>6</sub>))],(I `3_3)] is non empty V7() set
{[(c₁,I),((I `2_3) +* (a,c<sub>6</sub>))],(I `3_3)} is non empty V36() countable set
{[(c₁,I),((I `2_3) +* (a,c<sub>6</sub>))]} is non empty trivial V4() V5() Relation-like Function-like constant V36() 1 -element countable V93() set
{{[(c<sub>1</sub>,I),((I `2_3) +* (a,c₆))],(I `3_3)},{[(c<sub>1</sub>,I),((I `2_3) +* (a,c₆))]}} is non empty V4() V5() V36() V40() countable set
IT is Element of c₁
(c₁,IT) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer Element of (c₁)
K41(IT) is set
K41(K41(IT)) is set
IT `2_3 is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like countable complex-valued ext-real-valued real-valued natural-valued V93() set
K41(IT) `3_3 is set
c₉ is Relation-like Function-like Element of (c₁,(c₁,I))
c₉ . a is set
c₁ is non empty Relation-like () set
i is Element of c₁
(c₁,i) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer Element of (c₁)
(c₁) is non empty set
proj1_3 c₁ is set
proj1 c₁ is non empty set
proj1 (proj1 c₁) is set
K41(i) is set
K41(K41(i)) is set
I is Element of c₁
(c₁,I) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer Element of (c₁)
K41(I) is set
K41(K41(I)) is set
i `2_3 is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like countable complex-valued ext-real-valued real-valued natural-valued V93() set
K41(i) `3_3 is set
I `2_3 is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like countable complex-valued ext-real-valued real-valued natural-valued V93() set
K41(I) `3_3 is set
i `3_3 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like countable V93() set
I `3_3 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like countable V93() set
a is non empty set
a * is non empty functional FinSequence-membered set
[:NAT,(NAT *),(a *):] is non empty set
[:NAT,(NAT *):] is non empty non trivial V5() Relation-like V36() set
[:[:NAT,(NAT *):],(a *):] is non empty non trivial V5() Relation-like V36() set
c₁ is non empty Relation-like () () () set
(c₁) is non empty set
proj1_3 c₁ is set
proj1 c₁ is non empty set
proj1 (proj1 c₁) is set
i is Element of (c₁)
(c₁,i) is non empty functional with_common_domain set
{ (b₁ `2_3) where b<sub>1</sub> is Element of c<sub>1</sub> : (c<sub>1</sub>,b<sub>1</sub>) = i } is set
I is set
[i,I] is non empty V7() set
{i,I} is non empty V36() countable set
{i} is non empty trivial V36() 1 -element countable set
{{i,I},{i}} is non empty V4() V5() V36() V40() countable set
a is set
[[i,I],a] is non empty V7() set
{[i,I],a} is non empty V36() countable set
{[i,I]} is non empty trivial V4() V5() Relation-like Function-like constant V36() 1 -element countable V93() set
{{[i,I],a},{[i,I]}} is non empty V4() V5() V36() V40() countable set
[i,I,a] is V7() triple set
II is Element of c<sub>1</sub>
(c<sub>1</sub>,II) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer Element of (c<sub>1</sub>)
K41(II) is set
K41(K41(II)) is set
II `2_3 is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like countable complex-valued ext-real-valued real-valued natural-valued V93() set
K41(II) `3_3 is set
dom (II `2_3) is V36() countable V71() V72() V73() V74() V75() V76() Element of bool NAT
(dom (II `2_3)) --> NAT is Relation-like non-empty dom (II `2_3) -defined bool REAL -valued Function-like constant V20( dom (II `2_3)) V21( dom (II `2_3), bool REAL) V36() Cardinal-yielding countable V93() Element of bool [:(dom (II `2_3)),(bool REAL):]
[:(dom (II `2_3)),(bool REAL):] is Relation-like set
bool [:(dom (II `2_3)),(bool REAL):] is non empty set
{NAT} is non empty trivial V4() V5() V36() 1 -element countable set
[:(dom (II `2_3)),{NAT}:] is Relation-like V36() countable set
proj1 ((dom (II `2_3)) --> NAT) is V36() countable set
J is set
IT is Element of c<sub>1</sub>
IT `2_3 is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like countable complex-valued ext-real-valued real-valued natural-valued V93() set
K41(IT) is set
K41(IT) `3_3 is set
(c<sub>1</sub>,IT) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer Element of (c<sub>1</sub>)
K41(K41(IT)) is set
c<sub>9</sub> is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like countable complex-valued ext-real-valued real-valued natural-valued V93() set
proj1 c<sub>9</sub> is V36() countable V71() V72() V73() V74() V75() V76() set
dom c<sub>9</sub> is V36() countable V71() V72() V73() V74() V75() V76() Element of bool NAT
J is set
c<sub>9</sub> . J is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer set
((dom (II `2_3)) --> NAT) . J is set
IT is Relation-like Function-like set
proj1 IT is set
[i,IT,a] is V7() triple set
[i,IT] is non empty V7() set
{i,IT} is non empty V36() countable set
{{i,IT},{i}} is non empty V4() V5() V36() V40() countable set
[[i,IT],a] is non empty V7() set
{[i,IT],a} is non empty V36() countable set
{[i,IT]} is non empty trivial V4() V5() Relation-like Function-like constant V36() 1 -element countable V93() set
{{[i,IT],a},{[i,IT]}} is non empty V4() V5() V36() V40() countable set
product" (c₁,i) is Relation-like Function-like set
proj1 (product" (c₁,i)) is set
J is set
IT . J is set
(product" (c₁,i)) . J is set
(c₁,(c₁,II)) is non empty functional with_common_domain set
{ (b₁ `2_3) where b<sub>1</sub> is Element of c<sub>1</sub> : (c<sub>1</sub>,b<sub>1</sub>) = (c<sub>1</sub>,II) } is set
product" (c<sub>1</sub>,(c<sub>1</sub>,II)) is Relation-like Function-like set
(product" (c<sub>1</sub>,(c<sub>1</sub>,II))) . J is set
((dom (II `2_3)) --> NAT) . J is set
J is set
IT . J is set
(c₁,(c₁,II)) is non empty functional with_common_domain set
{ (b₁ `2_3) where b<sub>1</sub> is Element of c<sub>1</sub> : (c<sub>1</sub>,b<sub>1</sub>) = (c<sub>1</sub>,II) } is set
product" (c<sub>1</sub>,(c<sub>1</sub>,II)) is Relation-like Function-like set
(product" (c<sub>1</sub>,(c<sub>1</sub>,II))) . J is set
(product" (c<sub>1</sub>,i)) . J is set
J is Element of c<sub>1</sub>
(c<sub>1</sub>,J) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer Element of (c<sub>1</sub>)
K41(J) is set
K41(K41(J)) is set
J `2_3 is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like countable complex-valued ext-real-valued real-valued natural-valued V93() set
K41(J) `3_3 is set
product ((dom (II `2_3)) --> NAT) is non empty functional with_common_domain product-like set
c₁ is Relation-like () set
c₁ is non empty Relation-like () set
i is Element of c₁
i `2_3 is Relation-like NAT -defined NAT -valued Function-like V36() FinSequence-like FinSubsequence-like countable complex-valued ext-real-valued real-valued natural-valued V93() set
K41(i) is set
K41(i) `3_3 is set
I is Relation-like Function-like set
c₁ is non empty Relation-like () () () set
i is Element of c₁
(c₁,i) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer Element of (c₁)
(c₁) is non empty set
proj1_3 c₁ is set
proj1 c₁ is non empty set
proj1 (proj1 c₁) is set
K41(i) is set
K41(K41(i)) is set
i `3_3 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like countable V93() set
i `2_3 is Relation-like NAT -defined NAT -valued RAT -valued Function-like V36() FinSequence-like FinSubsequence-like countable complex-valued ext-real-valued real-valued natural-valued V93() set
K41(i) `3_3 is set
I is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer set
I + (i `2_3) is Relation-like NAT -defined RAT -valued Function-like V36() FinSequence-like FinSubsequence-like countable complex-valued ext-real-valued real-valued natural-valued V93() set
a is non empty set
a * is non empty functional FinSequence-membered set
[:NAT,(NAT *),(a *):] is non empty set
[:NAT,(NAT *):] is non empty non trivial V5() Relation-like V36() set
[:[:NAT,(NAT *):],(a *):] is non empty non trivial V5() Relation-like V36() set
(c₁,(c₁,i)) is non empty functional with_common_domain product-like set
{ (b₁ `2_3) where b<sub>1</sub> is Element of c<sub>1</sub> : (c<sub>1</sub>,b<sub>1</sub>) = (c<sub>1</sub>,i) } is set
product" (c<sub>1</sub>,(c<sub>1</sub>,i)) is Relation-like Function-like set
product (product" (c<sub>1</sub>,(c<sub>1</sub>,i))) is functional with_common_domain product-like set
dom (I + (i `2_3)) is V36() countable V71() V72() V73() V74() V75() V76() Element of bool NAT
dom (i `2_3) is V36() countable V71() V72() V73() V74() V75() V76() Element of bool NAT
DOM (c<sub>1</sub>,(c<sub>1</sub>,i)) is set
{ (proj1 b<sub>1</sub>) where b<sub>1</sub> is Relation-like Function-like Element of (c<sub>1</sub>,(c<sub>1</sub>,i)) : verum } is set
K24( { (proj1 b<sub>1</sub>) where b<sub>1</sub> is Relation-like Function-like Element of (c<sub>1</sub>,(c<sub>1</sub>,i)) : verum } ) is set
proj1 (product" (c<sub>1</sub>,(c<sub>1</sub>,i))) is set
J is set
(I + (i `2_3)) . J is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer V60() set
(product" (c₁,(c₁,i))) . J is set
IT is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer V60() V71() V72() V73() V74() V75() V76() Element of NAT
(product" (c₁,(c₁,i))) . IT is set
(i `2_3) . IT is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer V60() set
(I + (i `2_3)) . IT is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer V60() set
c₉ is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer V60() V71() V72() V73() V74() V75() V76() Element of NAT
I + c₉ is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer V60() V71() V72() V73() V74() V75() V76() Element of NAT
J is Element of c₁
J `2_3 is Relation-like NAT -defined NAT -valued RAT -valued Function-like V36() FinSequence-like FinSubsequence-like countable complex-valued ext-real-valued real-valued natural-valued V93() set
K41(J) is set
K41(J) `3_3 is set
(c₁,J) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer Element of (c₁)
K41(K41(J)) is set
[(c₁,i),(i `2_3),(i `3_3)] is V7() triple set
[(c₁,i),(i `2_3)] is non empty V7() set
{(c<sub>1</sub>,i),(i `2_3)} is non empty V36() V40() countable set
{(c₁,i)} is non empty trivial V36() V40() 1 -element countable V71() V72() V73() V74() V75() V76() set
{{(c₁,i),(i `2_3)},{(c<sub>1</sub>,i)}} is non empty V4() V5() V36() V40() countable set
[[(c<sub>1</sub>,i),(i `2_3)],(i `3_3)] is non empty V7() set
{[(c<sub>1</sub>,i),(i `2_3)],(i `3_3)} is non empty V36() countable set
{[(c<sub>1</sub>,i),(i `2_3)]} is non empty trivial V4() V5() Relation-like Function-like constant V36() 1 -element countable V93() set
{{[(c₁,i),(i `2_3)],(i `3_3)},{[(c₁,i),(i `2_3)]}} is non empty V4() V5() V36() V40() countable set
[(c<sub>1</sub>,i),(J `2_3),(i `3_3)] is V7() triple set
[(c<sub>1</sub>,i),(J `2_3)] is non empty V7() set
{(c₁,i),(J `2_3)} is non empty V36() V40() countable set
{{(c<sub>1</sub>,i),(J `2_3)},{(c₁,i)}} is non empty V4() V5() V36() V40() countable set
[[(c₁,i),(J `2_3)],(i `3_3)] is non empty V7() set
{[(c₁,i),(J `2_3)],(i `3_3)} is non empty V36() countable set
{[(c₁,i),(J `2_3)]} is non empty trivial V4() V5() Relation-like Function-like constant V36() 1 -element countable V93() set
{{[(c<sub>1</sub>,i),(J `2_3)],(i `3_3)},{[(c<sub>1</sub>,i),(J `2_3)]}} is non empty V4() V5() V36() V40() countable set
IT is Element of c₁
(c₁,IT) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer Element of (c₁)
K41(IT) is set
K41(K41(IT)) is set
IT `3_3 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like countable V93() set
IT `2_3 is Relation-like NAT -defined NAT -valued RAT -valued Function-like V36() FinSequence-like FinSubsequence-like countable complex-valued ext-real-valued real-valued natural-valued V93() set
K41(IT) `3_3 is set
a is Element of c<sub>1</sub>
(c<sub>1</sub>,a) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer Element of (c<sub>1</sub>)
K41(a) is set
K41(K41(a)) is set
a `3_3 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like countable V93() set
a `2_3 is Relation-like NAT -defined NAT -valued RAT -valued Function-like V36() FinSequence-like FinSubsequence-like countable complex-valued ext-real-valued real-valued natural-valued V93() set
K41(a) `3_3 is set
II is Element of c₁
(c₁,II) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer Element of (c₁)
K41(II) is set
K41(K41(II)) is set
II `3_3 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like countable V93() set
II `2_3 is Relation-like NAT -defined NAT -valued RAT -valued Function-like V36() FinSequence-like FinSubsequence-like countable complex-valued ext-real-valued real-valued natural-valued V93() set
K41(II) `3_3 is set
c<sub>1</sub> is non empty Relation-like () () () set
i is Element of c<sub>1</sub>
(c<sub>1</sub>,i,0) is Element of c<sub>1</sub>
(c<sub>1</sub>,(c<sub>1</sub>,i,0)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer Element of (c<sub>1</sub>)
(c<sub>1</sub>) is non empty set
proj1_3 c<sub>1</sub> is set
proj1 c<sub>1</sub> is non empty set
proj1 (proj1 c<sub>1</sub>) is set
K41((c<sub>1</sub>,i,0)) is set
K41(K41((c<sub>1</sub>,i,0))) is set
(c<sub>1</sub>,i) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer Element of (c<sub>1</sub>)
K41(i) is set
K41(K41(i)) is set
(c<sub>1</sub>,i,0) `3_3 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like countable V93() set
i `3_3 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like countable V93() set
(c<sub>1</sub>,i,0) `2_3 is Relation-like NAT -defined NAT -valued RAT -valued Function-like V36() FinSequence-like FinSubsequence-like countable complex-valued ext-real-valued real-valued natural-valued V93() set
K41((c₁,i,0)) `3_3 is set
i `2_3 is Relation-like NAT -defined NAT -valued RAT -valued Function-like V36() FinSequence-like FinSubsequence-like countable complex-valued ext-real-valued real-valued natural-valued V93() set
K41(i) `3_3 is set
0 + (i `2_3) is Relation-like NAT -defined RAT -valued Function-like V36() FinSequence-like FinSubsequence-like countable complex-valued ext-real-valued real-valued natural-valued V93() set
dom (i `2_3) is V36() countable V71() V72() V73() V74() V75() V76() Element of bool NAT
dom ((c<sub>1</sub>,i,0) `2_3) is V36() countable V71() V72() V73() V74() V75() V76() Element of bool NAT
I is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer set
((c₁,i,0) `2_3) . I is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer V60() set
(i `2_3) . I is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer V60() set
0 + ((i `2_3) . I) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer set
c<sub>1</sub> is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer set
i is non empty Relation-like () () () set
I is Element of i
(i,I,c<sub>1</sub>) is Element of i
I `2_3 is Relation-like NAT -defined NAT -valued RAT -valued Function-like V36() FinSequence-like FinSubsequence-like countable complex-valued ext-real-valued real-valued natural-valued V93() set
K41(I) is set
K41(I) `3_3 is set
(i,(i,I,c<sub>1</sub>)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer Element of (i)
(i) is non empty set
proj1_3 i is set
proj1 i is non empty set
proj1 (proj1 i) is set
K41((i,I,c<sub>1</sub>)) is set
K41(K41((i,I,c<sub>1</sub>))) is set
(i,I) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer Element of (i)
K41(K41(I)) is set
(i,I,c<sub>1</sub>) `3_3 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like countable V93() set
I `3_3 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like countable V93() set
(i,I,c<sub>1</sub>) `2_3 is Relation-like NAT -defined NAT -valued RAT -valued Function-like V36() FinSequence-like FinSubsequence-like countable complex-valued ext-real-valued real-valued natural-valued V93() set
K41((i,I,c₁)) `3_3 is set
c<sub>1</sub> + (I `2_3) is Relation-like NAT -defined RAT -valued Function-like V36() FinSequence-like FinSubsequence-like countable complex-valued ext-real-valued real-valued natural-valued V93() set
c₁ is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer set
i is non empty Relation-like () () () set
I is Element of i
(i,I) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer Element of (i)
(i) is non empty set
proj1_3 i is set
proj1 i is non empty set
proj1 (proj1 i) is set
K41(I) is set
K41(K41(I)) is set
(i,(i,I)) is non empty functional with_common_domain product-like set
{ (b₁ `2_3) where b<sub>1</sub> is Element of i : (i,b<sub>1</sub>) = (i,I) } is set
(i,I,c<sub>1</sub>) is Element of i
(i,(i,I,c<sub>1</sub>)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer Element of (i)
K41((i,I,c<sub>1</sub>)) is set
K41(K41((i,I,c<sub>1</sub>))) is set
(i,(i,(i,I,c<sub>1</sub>))) is non empty functional with_common_domain product-like set
{ (b<sub>1</sub> `2_3) where b₁ is Element of i : (i,b₁) = (i,(i,I,c₁)) } is set
{ (b₁ `2_3) where b<sub>1</sub> is Element of i : (i,I) = (i,b<sub>1</sub>) } is set
{ (b<sub>1</sub> `2_3) where b₁ is Element of i : (i,(i,I,c₁)) = (i,b₁) } is set
c₆ is set
J is Element of i
J `2_3 is Relation-like NAT -defined NAT -valued RAT -valued Function-like V36() FinSequence-like FinSubsequence-like countable complex-valued ext-real-valued real-valued natural-valued V93() set
K41(J) is set
K41(J) `3_3 is set
(i,J) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer Element of (i)
K41(K41(J)) is set
c₆ is set
J is Element of i
J `2_3 is Relation-like NAT -defined NAT -valued RAT -valued Function-like V36() FinSequence-like FinSubsequence-like countable complex-valued ext-real-valued real-valued natural-valued V93() set
K41(J) is set
K41(J) `3_3 is set
(i,J) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer Element of (i)
K41(K41(J)) is set
c₁ is non empty Relation-like () () () set
i is Element of c₁
I is Element of c₁
a is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer set
(c₁,i,a) is Element of c₁
(c₁,I,a) is Element of c₁
(c₁,i) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer Element of (c₁)
(c₁) is non empty set
proj1_3 c₁ is set
proj1 c₁ is non empty set
proj1 (proj1 c₁) is set
K41(i) is set
K41(K41(i)) is set
(c₁,(c₁,i,a)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer Element of (c₁)
K41((c₁,i,a)) is set
K41(K41((c₁,i,a))) is set
(c₁,I) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer Element of (c₁)
K41(I) is set
K41(K41(I)) is set
i `3_3 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like countable V93() set
(c<sub>1</sub>,i,a) `3_3 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like countable V93() set
I `3_3 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like countable V93() set
(c<sub>1</sub>,i,a) `2_3 is Relation-like NAT -defined NAT -valued RAT -valued Function-like V36() FinSequence-like FinSubsequence-like countable complex-valued ext-real-valued real-valued natural-valued V93() set
K41((c₁,i,a)) `3_3 is set
i `2_3 is Relation-like NAT -defined NAT -valued RAT -valued Function-like V36() FinSequence-like FinSubsequence-like countable complex-valued ext-real-valued real-valued natural-valued V93() set
K41(i) `3_3 is set
a + (i `2_3) is Relation-like NAT -defined RAT -valued Function-like V36() FinSequence-like FinSubsequence-like countable complex-valued ext-real-valued real-valued natural-valued V93() set
dom (i `2_3) is V36() countable V71() V72() V73() V74() V75() V76() Element of bool NAT
dom ((c<sub>1</sub>,i,a) `2_3) is V36() countable V71() V72() V73() V74() V75() V76() Element of bool NAT
(c₁,I,a) `2_3 is Relation-like NAT -defined NAT -valued RAT -valued Function-like V36() FinSequence-like FinSubsequence-like countable complex-valued ext-real-valued real-valued natural-valued V93() set
K41((c<sub>1</sub>,I,a)) is set
K41((c<sub>1</sub>,I,a)) `3_3 is set
I `2_3 is Relation-like NAT -defined NAT -valued RAT -valued Function-like V36() FinSequence-like FinSubsequence-like countable complex-valued ext-real-valued real-valued natural-valued V93() set
K41(I) `3_3 is set
a + (I `2_3) is Relation-like NAT -defined RAT -valued Function-like V36() FinSequence-like FinSubsequence-like countable complex-valued ext-real-valued real-valued natural-valued V93() set
dom (I `2_3) is V36() countable V71() V72() V73() V74() V75() V76() Element of bool NAT
dom ((c₁,I,a) `2_3) is V36() countable V71() V72() V73() V74() V75() V76() Element of bool NAT
II is set
(i `2_3) . II is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer V60() set
(I `2_3) . II is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer V60() set
((c<sub>1</sub>,i,a) `2_3) . II is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer V60() set
a + ((i `2_3) . II) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer set
((c<sub>1</sub>,I,a) `2_3) . II is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer V60() set
a + ((I `2_3) . II) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer set
c<sub>1</sub> is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer set
i is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer set
c<sub>1</sub> + i is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer set
I is non empty Relation-like () () () set
a is Element of I
(I,a,c<sub>1</sub>) is Element of I
(I,(I,a,c<sub>1</sub>),i) is Element of I
(I,a,(c<sub>1</sub> + i)) is Element of I
(I,(I,(I,a,c<sub>1</sub>),i)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer Element of (I)
(I) is non empty set
proj1_3 I is set
proj1 I is non empty set
proj1 (proj1 I) is set
K41((I,(I,a,c<sub>1</sub>),i)) is set
K41(K41((I,(I,a,c<sub>1</sub>),i))) is set
(I,(I,a,c<sub>1</sub>)) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer Element of (I)
K41((I,a,c<sub>1</sub>)) is set
K41(K41((I,a,c<sub>1</sub>))) is set
(I,a) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer Element of (I)
K41(a) is set
K41(K41(a)) is set
(I,(I,a,(c<sub>1</sub> + i))) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer Element of (I)
K41((I,a,(c<sub>1</sub> + i))) is set
K41(K41((I,a,(c<sub>1</sub> + i)))) is set
(I,(I,a,c<sub>1</sub>),i) `3_3 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like countable V93() set
(I,a,c₁) `3_3 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like countable V93() set
a `3_3 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like countable V93() set
(I,a,(c₁ + i)) `3_3 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like countable V93() set
(I,(I,a,c<sub>1</sub>),i) `2_3 is Relation-like NAT -defined NAT -valued RAT -valued Function-like V36() FinSequence-like FinSubsequence-like countable complex-valued ext-real-valued real-valued natural-valued V93() set
K41((I,(I,a,c₁),i)) `3_3 is set
(I,a,c<sub>1</sub>) `2_3 is Relation-like NAT -defined NAT -valued RAT -valued Function-like V36() FinSequence-like FinSubsequence-like countable complex-valued ext-real-valued real-valued natural-valued V93() set
K41((I,a,c₁)) `3_3 is set
i + ((I,a,c<sub>1</sub>) `2_3) is Relation-like NAT -defined RAT -valued Function-like V36() FinSequence-like FinSubsequence-like countable complex-valued ext-real-valued real-valued natural-valued V93() set
a `2_3 is Relation-like NAT -defined NAT -valued RAT -valued Function-like V36() FinSequence-like FinSubsequence-like countable complex-valued ext-real-valued real-valued natural-valued V93() set
K41(a) `3_3 is set
c₁ + (a `2_3) is Relation-like NAT -defined RAT -valued Function-like V36() FinSequence-like FinSubsequence-like countable complex-valued ext-real-valued real-valued natural-valued V93() set
(I,a,(c<sub>1</sub> + i)) `2_3 is Relation-like NAT -defined NAT -valued RAT -valued Function-like V36() FinSequence-like FinSubsequence-like countable complex-valued ext-real-valued real-valued natural-valued V93() set
K41((I,a,(c₁ + i))) `3_3 is set
(c<sub>1</sub> + i) + (a `2_3) is Relation-like NAT -defined RAT -valued Function-like V36() FinSequence-like FinSubsequence-like countable complex-valued ext-real-valued real-valued natural-valued V93() set
dom ((I,a,(c₁ + i)) `2_3) is V36() countable V71() V72() V73() V74() V75() V76() Element of bool NAT
dom (a `2_3) is V36() countable V71() V72() V73() V74() V75() V76() Element of bool NAT
dom ((I,a,c₁) `2_3) is V36() countable V71() V72() V73() V74() V75() V76() Element of bool NAT
dom ((I,(I,a,c<sub>1</sub>),i) `2_3) is V36() countable V71() V72() V73() V74() V75() V76() Element of bool NAT
II is set
((I,(I,a,c₁),i) `2_3) . II is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer V60() set
((I,a,(c<sub>1</sub> + i)) `2_3) . II is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer V60() set
((I,a,c₁) `2_3) . II is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer V60() set
(a `2_3) . II is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer V60() set
c₁ + ((a `2_3) . II) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer set
i + (((I,a,c<sub>1</sub>) `2_3) . II) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer set
(c₁ + i) + ((a `2_3) . II) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer set
c<sub>1</sub> is non empty Relation-like () () () set
i is Element of c<sub>1</sub>
i `2_3 is Relation-like NAT -defined NAT -valued RAT -valued Function-like V36() FinSequence-like FinSubsequence-like countable complex-valued ext-real-valued real-valued natural-valued V93() set
K41(i) is set
K41(i) `3_3 is set
dom (i `2_3) is V36() countable V71() V72() V73() V74() V75() V76() Element of bool NAT
(c₁,i) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer Element of (c₁)
(c₁) is non empty set
proj1_3 c₁ is set
proj1 c₁ is non empty set
proj1 (proj1 c₁) is set
K41(K41(i)) is set
(c₁,(c₁,i)) is non empty functional with_common_domain product-like set
{ (b₁ `2_3) where b<sub>1</sub> is Element of c<sub>1</sub> : (c<sub>1</sub>,b<sub>1</sub>) = (c<sub>1</sub>,i) } is set
product" (c<sub>1</sub>,(c<sub>1</sub>,i)) is Relation-like Function-like set
I is set
(i `2_3) . I is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer V60() set
(product" (c₁,(c₁,i))) . I is set
proj1 (product" (c₁,(c₁,i))) is set
DOM (c₁,(c₁,i)) is set
{ (proj1 b₁) where b₁ is Relation-like Function-like Element of (c₁,(c₁,i)) : verum } is set
K24( { (proj1 b₁) where b₁ is Relation-like Function-like Element of (c₁,(c₁,i)) : verum } ) is set
pi ((c₁,(c₁,i)),I) is set
{[0,{},{}],[1,{},{}]} is non empty V36() countable set
{{}} * is non empty functional FinSequence-membered set
[:NAT,(NAT *),({{}} *):] is non empty set
[:NAT,(NAT *):] is non empty non trivial V5() Relation-like V36() set
[:[:NAT,(NAT *):],({{}} *):] is non empty non trivial V5() Relation-like V36() set
[:{0},{{}},{{}}:] is non empty V36() countable set
[:{0},{{}}:] is non empty Relation-like RAT -valued INT -valued V36() countable complex-valued ext-real-valued real-valued natural-valued set
[:[:{0},{{}}:],{{}}:] is non empty Relation-like RAT -valued INT -valued V36() countable complex-valued ext-real-valued real-valued natural-valued set
{1} is non empty trivial V4() V5() V36() V40() 1 -element countable V71() V72() V73() V74() V75() V76() Element of bool NAT
[:{1},{{}},{{}}:] is non empty V36() countable set
[:{1},{{}}:] is non empty Relation-like RAT -valued INT -valued V36() countable complex-valued ext-real-valued real-valued natural-valued set
[:[:{1},{{}}:],{{}}:] is non empty Relation-like RAT -valued INT -valued V36() countable complex-valued ext-real-valued real-valued natural-valued set
{[0,{},{}]} \/ {[1,{},{}]} is non empty Relation-like V36() countable set
[1,0,0] is V7() triple Element of [:NAT,NAT,NAT:]
[:NAT,NAT,NAT:] is non empty set
[:NAT,NAT:] is non empty non trivial V5() Relation-like RAT -valued INT -valued V36() complex-valued ext-real-valued real-valued natural-valued set
[:[:NAT,NAT:],NAT:] is non empty non trivial V5() Relation-like RAT -valued INT -valued V36() complex-valued ext-real-valued real-valued natural-valued set
[1,0] is non empty V7() set
{1,0} is non empty V36() V40() countable V71() V72() V73() V74() V75() V76() set
{{1,0},{1}} is non empty V4() V5() V36() V40() countable set
[[1,0],0] is non empty V7() set
{[1,0],0} is non empty V36() countable set
{[1,0]} is non empty trivial V4() V5() Relation-like Function-like constant V36() 1 -element countable V93() set
{{[1,0],0},{[1,0]}} is non empty V4() V5() V36() V40() countable set
{[0,{},{}],[1,0,0]} is non empty V36() countable set
c₁ is Element of {[0,{},{}],[1,{},{}]}
c₁ `2_3 is Relation-like NAT -defined NAT -valued RAT -valued Function-like V36() FinSequence-like FinSubsequence-like countable complex-valued ext-real-valued real-valued natural-valued V93() set
K41(c<sub>1</sub>) is set
K41(c<sub>1</sub>) `3_3 is set
({[0,{},{}],[1,{},{}]}) is non empty set
proj1_3 {[0,{},{}],[1,{},{}]} is set
proj1 {[0,{},{}],[1,{},{}]} is non empty V36() countable set
proj1 (proj1 {[0,{},{}],[1,{},{}]}) is set
c₁ is Element of ({[0,{},{}],[1,{},{}]})
({[0,{},{}],[1,{},{}]},c₁) is non empty functional set
{ (b₁ `2_3) where b<sub>1</sub> is Element of {[0,{},{}],[1,{},{}]} : ({[0,{},{}],[1,{},{}]},b<sub>1</sub>) = c<sub>1</sub> } is set
I is set
({[1,{},{}]}) is non empty set
proj1_3 {[1,{},{}]} is set
proj1 {[1,{},{}]} is non empty trivial V36() 1 -element countable set
proj1 (proj1 {[1,{},{}]}) is set
{1} is non empty trivial V4() V5() V36() V40() 1 -element countable V71() V72() V73() V74() V75() V76() Element of bool NAT
{[0,{},{}]} \/ {[1,{},{}]} is non empty Relation-like V36() countable set
proj1_3 ({[0,{},{}]} \/ {[1,{},{}]}) is set
proj1 ({[0,{},{}]} \/ {[1,{},{}]}) is non empty V36() countable set
proj1 (proj1 ({[0,{},{}]} \/ {[1,{},{}]})) is set
({[0,{},{}]}) \/ ({[1,{},{}]}) is non empty set
[0,0,0] is V7() triple Element of [:NAT,NAT,NAT:]
[:NAT,NAT,NAT:] is non empty set
[:NAT,NAT:] is non empty non trivial V5() Relation-like RAT -valued INT -valued V36() complex-valued ext-real-valued real-valued natural-valued set
[:[:NAT,NAT:],NAT:] is non empty non trivial V5() Relation-like RAT -valued INT -valued V36() complex-valued ext-real-valued real-valued natural-valued set
[0,0] is non empty V7() set
{0,0} is non empty functional V36() V40() countable V71() V72() V73() V74() V75() V76() set
{{0,0},{0}} is non empty V4() V5() V36() V40() countable set
[[0,0],0] is non empty V7() set
{[0,0],0} is non empty V36() countable set
{[0,0]} is non empty trivial V4() V5() Relation-like Function-like constant V36() 1 -element countable V93() set
{{[0,0],0},{[0,0]}} is non empty V4() V5() V36() V40() countable set
[1,0,0] is V7() triple Element of [:NAT,NAT,NAT:]
[1,0] is non empty V7() set
{1,0} is non empty V36() V40() countable V71() V72() V73() V74() V75() V76() set
{{1,0},{1}} is non empty V4() V5() V36() V40() countable set
[[1,0],0] is non empty V7() set
{[1,0],0} is non empty V36() countable set
{[1,0]} is non empty trivial V4() V5() Relation-like Function-like constant V36() 1 -element countable V93() set
{{[1,0],0},{[1,0]}} is non empty V4() V5() V36() V40() countable set
a is Element of {[0,{},{}],[1,{},{}]}
a `2_3 is Relation-like NAT -defined NAT -valued RAT -valued Function-like V36() FinSequence-like FinSubsequence-like countable complex-valued ext-real-valued real-valued natural-valued V93() set
K41(a) is set
K41(a) `3_3 is set
II is Element of {[0,{},{}],[1,{},{}]}
II `2_3 is Relation-like NAT -defined NAT -valued RAT -valued Function-like V36() FinSequence-like FinSubsequence-like countable complex-valued ext-real-valued real-valued natural-valued V93() set
K41(II) is set
K41(II) `3_3 is set
({[0,{},{}],[1,{},{}]},a) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer Element of ({[0,{},{}],[1,{},{}]})
K41(K41(a)) is set
({[0,{},{}],[1,{},{}]},II) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer Element of ({[0,{},{}],[1,{},{}]})
K41(K41(II)) is set
I is set
a is Element of {[0,{},{}],[1,{},{}]}
a `2_3 is Relation-like NAT -defined NAT -valued RAT -valued Function-like V36() FinSequence-like FinSubsequence-like countable complex-valued ext-real-valued real-valued natural-valued V93() set
K41(a) is set
K41(a) `3_3 is set
({[0,{},{}],[1,{},{}]},a) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer Element of ({[0,{},{}],[1,{},{}]})
K41(K41(a)) is set
i is Element of ({[0,{},{}],[1,{},{}]})
({[0,{},{}],[1,{},{}]},i) is non empty functional set
{ (b<sub>1</sub> `2_3) where b₁ is Element of {[0,{},{}],[1,{},{}]} : ({[0,{},{}],[1,{},{}]},b₁) = i } is set
I is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued set
proj1 I is set
a is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued set
proj1 a is set
II is set
[i,I,II] is V7() triple set
[i,I] is non empty V7() set
{i,I} is non empty V36() countable set
{i} is non empty trivial V36() 1 -element countable set
{{i,I},{i}} is non empty V4() V5() V36() V40() countable set
[[i,I],II] is non empty V7() set
{[i,I],II} is non empty V36() countable set
{[i,I]} is non empty trivial V4() V5() Relation-like Function-like constant V36() 1 -element countable V93() set
{{[i,I],II},{[i,I]}} is non empty V4() V5() V36() V40() countable set
[i,a,II] is V7() triple set
[i,a] is non empty V7() set
{i,a} is non empty V36() countable set
{{i,a},{i}} is non empty V4() V5() V36() V40() countable set
[[i,a],II] is non empty V7() set
{[i,a],II} is non empty V36() countable set
{[i,a]} is non empty trivial V4() V5() Relation-like Function-like constant V36() 1 -element countable V93() set
{{[i,a],II},{[i,a]}} is non empty V4() V5() V36() V40() countable set
i is Element of {[0,{},{}],[1,{},{}]}
({[0,{},{}],[1,{},{}]},i) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer Element of ({[0,{},{}],[1,{},{}]})
K41(i) is set
K41(K41(i)) is set
I is Element of {[0,{},{}],[1,{},{}]}
({[0,{},{}],[1,{},{}]},I) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer Element of ({[0,{},{}],[1,{},{}]})
K41(I) is set
K41(K41(I)) is set
i `2_3 is Relation-like NAT -defined NAT -valued RAT -valued Function-like V36() FinSequence-like FinSubsequence-like countable complex-valued ext-real-valued real-valued natural-valued V93() set
K41(i) `3_3 is set
dom (i `2_3) is V36() countable V71() V72() V73() V74() V75() V76() Element of bool NAT
I `2_3 is Relation-like NAT -defined NAT -valued RAT -valued Function-like V36() FinSequence-like FinSubsequence-like countable complex-valued ext-real-valued real-valued natural-valued V93() set
K41(I) `3_3 is set
dom (I `2_3) is V36() countable V71() V72() V73() V74() V75() V76() Element of bool NAT
c₁ is non empty Relation-like () set
(c₁) is non empty set
proj1_3 c₁ is set
proj1 c₁ is non empty set
proj1 (proj1 c₁) is set
i is Element of (c₁)
I is set
[i,I] is non empty V7() set
{i,I} is non empty V36() countable set
{i} is non empty trivial V36() 1 -element countable set
{{i,I},{i}} is non empty V4() V5() V36() V40() countable set
a is set
[[i,I],a] is non empty V7() set
{[i,I],a} is non empty V36() countable set
{[i,I]} is non empty trivial V4() V5() Relation-like Function-like constant V36() 1 -element countable V93() set
{{[i,I],a},{[i,I]}} is non empty V4() V5() V36() V40() countable set
II is Element of c₁
(c₁,II) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer Element of (c₁)
K41(II) is set
K41(K41(II)) is set
[i,I,a] is V7() triple set
c₁ is non empty Relation-like () () set
i is Element of c₁
i `2_3 is Relation-like NAT -defined NAT -valued RAT -valued Function-like V36() FinSequence-like FinSubsequence-like countable complex-valued ext-real-valued real-valued natural-valued V93() set
K41(i) is set
K41(i) `3_3 is set
(c₁,i) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer Element of (c₁)
(c₁) is non empty set
proj1_3 c₁ is set
proj1 c₁ is non empty set
proj1 (proj1 c₁) is set
K41(K41(i)) is set
(c₁,(c₁,i)) is non empty functional with_common_domain set
{ (b₁ `2_3) where b<sub>1</sub> is Element of c<sub>1</sub> : (c<sub>1</sub>,b<sub>1</sub>) = (c<sub>1</sub>,i) } is set
a is set
II is Element of c<sub>1</sub>
II `2_3 is Relation-like NAT -defined NAT -valued RAT -valued Function-like V36() FinSequence-like FinSubsequence-like countable complex-valued ext-real-valued real-valued natural-valued V93() set
K41(II) is set
K41(II) `3_3 is set
(c<sub>1</sub>,II) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer Element of (c<sub>1</sub>)
K41(K41(II)) is set
dom (II `2_3) is V36() countable V71() V72() V73() V74() V75() V76() Element of bool NAT
dom (i `2_3) is V36() countable V71() V72() V73() V74() V75() V76() Element of bool NAT
a is set
c<sub>1</sub> is set
c<sub>1</sub> is non empty trivial Relation-like V36() 1 -element countable () () () () set
c<sub>1</sub> is non empty trivial Relation-like V36() 1 -element countable () () () () set
c<sub>1</sub> is non empty () set
c<sub>1</sub> is non empty Relation-like () () set
(c<sub>1</sub>) is Element of c<sub>1</sub>
(c<sub>1</sub>) `2_3 is Relation-like NAT -defined NAT -valued RAT -valued Function-like V36() FinSequence-like FinSubsequence-like countable complex-valued ext-real-valued real-valued natural-valued V93() set
K41((c₁)) is set
K41((c₁)) `3_3 is set
c<sub>1</sub> is non empty Relation-like () () set
(c<sub>1</sub>) is (c<sub>1</sub>) Element of c<sub>1</sub>
c<sub>1</sub> is non empty Relation-like () () set
i is (c<sub>1</sub>) Element of c<sub>1</sub>
i `2_3 is Relation-like NAT -defined NAT -valued RAT -valued Function-like V36() FinSequence-like FinSubsequence-like countable complex-valued ext-real-valued real-valued natural-valued V93() set
K41(i) is set
K41(i) `3_3 is set
c₁ is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer set
i is non empty Relation-like () () () () set
(i) is (i) Element of i
I is Element of i
(i,I,c₁) is Element of i
(i,(i),c₁) is Element of i
c₁ is non empty Relation-like () () () () set