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

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

i is Element of c

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

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

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

proj1_3 c

proj1 c

proj1 (proj1 c

c

(c

proj1_3 c

proj1 c

proj1 (proj1 c

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

i is Element of c

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

proj1_3 c

proj1 c

proj1 (proj1 c

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

(c

proj1_3 c

proj1 c

proj1 (proj1 c

i is Element of (c

{ (b

{ (b

c

(c

proj1_3 c

proj1 c

proj1 (proj1 c

i is Element of (c

(c

{ (b

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

K41(a) is set

K41(K41(a)) is set

(c

{ (b

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

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

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

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

({[0,{},{}]},c

{ (b

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

({[0,{},{}]},c

{ (b

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

[c

{c

{c

{{c

[[c

{[c

{[c

{{[c

[c

[c

{c

{{c

[[c

{[c

{[c

{{[c

c

({[0,{},{}]},c

K41(c

K41(K41(c

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

K41(c

dom (c

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

c

(c

proj1_3 c

proj1 c

proj1 (proj1 c

i is Element of (c

(c

{ (b

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

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

K41(K41(II)) is set

c

c

K41(c

K41(c

(c

K41(K41(c

c

i is Element of c

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

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

dom (i `2_3) is V36() countable V71() V72() V73() V74() V75() V76() Element of bool NAT

(c

(c

proj1_3 c

proj1 c

proj1 (proj1 c

K41(K41(i)) is set

(c

{ (b

product" (c

I is set

(product" (c

proj1 (product" (c

{ (b

a is set

II is Relation-like Function-like Element of (c

II . I is set

c

c

K41(c

K41(c

(c

K41(K41(c

c

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

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

(c

proj1_3 c

proj1 c

proj1 (proj1 c

K41(K41(I)) is set

(c

{ (b

product" (c

a is set

(product" (c

proj1 (product" (c

{ (b

II is set

c

(I `2_3) +* (a,c

dom ((I `2_3) +* (a,c

I `3_3 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like countable V93() set

[(c

[(c

{(c

{(c

{{(c

[[(c

{[(c

{[(c

{{[(c

[(c

[(c

{(c

{{(c

[[(c

{[(c

{[(c

{{[(c

IT is Element of c

(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

c

c

i is Element of c

(c

(c

proj1_3 c

proj1 c

proj1 (proj1 c

K41(i) is set

K41(K41(i)) is set

I is Element of c

(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

(c

proj1_3 c

proj1 c

proj1 (proj1 c

i is Element of (c

(c

{ (b

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

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

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

K41(K41(IT)) is set

c

proj1 c

dom c

J is set

c

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

proj1 (product" (c

J is set

IT . J is set

(product" (c

(c

{ (b

product" (c

(product" (c

((dom (II `2_3)) --> NAT) . J is set

J is set

IT . J is set

(c

{ (b

product" (c

(product" (c

(product" (c

J is Element of c

(c

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

c

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

i is Element of c

(c

(c

proj1_3 c

proj1 c

proj1 (proj1 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

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

{ (b

product" (c

product (product" (c

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

{ (proj1 b

K24( { (proj1 b

proj1 (product" (c

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

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

(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

I + c

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

K41(K41(J)) is set

[(c

[(c

{(c

{(c

{{(c

[[(c

{[(c

{[(c

{{[(c

[(c

[(c

{(c

{{(c

[[(c

{[(c

{[(c

{{[(c

IT is Element of c

(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

(c

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

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

i is Element of c

(c

(c

(c

proj1_3 c

proj1 c

proj1 (proj1 c

K41((c

K41(K41((c

(c

K41(i) is set

K41(K41(i)) is set

(c

i `3_3 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like countable V93() set

(c

K41((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) `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

I is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer set

((c

(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

i is non empty Relation-like () () () set

I is Element of i

(i,I,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

(i,(i,I,c

(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

K41(K41((i,I,c

(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

I `3_3 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like countable V93() set

(i,I,c

K41((i,I,c

c

c

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

(i,I,c

(i,(i,I,c

K41((i,I,c

K41(K41((i,I,c

(i,(i,(i,I,c

{ (b

{ (b

{ (b

c

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

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

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

(c

(c

(c

proj1_3 c

proj1 c

proj1 (proj1 c

K41(i) is set

K41(K41(i)) is set

(c

K41((c

K41(K41((c

(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

I `3_3 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like countable V93() set

(c

K41((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) `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

(c

K41((c

K41((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) `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

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

a + ((i `2_3) . II) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer set

((c

a + ((I `2_3) . II) is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer set

c

i is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer set

c

I is non empty Relation-like () () () set

a is Element of I

(I,a,c

(I,(I,a,c

(I,a,(c

(I,(I,(I,a,c

(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

K41(K41((I,(I,a,c

(I,(I,a,c

K41((I,a,c

K41(K41((I,a,c

(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

K41((I,a,(c

K41(K41((I,a,(c

(I,(I,a,c

(I,a,c

a `3_3 is Relation-like NAT -defined Function-like V36() FinSequence-like FinSubsequence-like countable V93() set

(I,a,(c

(I,(I,a,c

K41((I,(I,a,c

(I,a,c

K41((I,a,c

i + ((I,a,c

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

(I,a,(c

K41((I,a,(c

(c

dom ((I,a,(c

dom (a `2_3) is V36() countable V71() V72() V73() V74() V75() V76() Element of bool NAT

dom ((I,a,c

dom ((I,(I,a,c

II is set

((I,(I,a,c

((I,a,(c

((I,a,c

(a `2_3) . II is ext-real non negative epsilon-transitive epsilon-connected ordinal natural V36() cardinal countable V57() V58() integer V60() set

c

i + (((I,a,c

(c

c

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

dom (i `2_3) is V36() countable V71() V72() V73() V74() V75() V76() Element of bool NAT

(c

(c

proj1_3 c

proj1 c

proj1 (proj1 c

K41(K41(i)) is set

(c

{ (b

product" (c

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

proj1 (product" (c

DOM (c

{ (proj1 b

K24( { (proj1 b

pi ((c

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

c

K41(c

K41(c

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

({[0,{},{}],[1,{},{}]},c

{ (b

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