:: EXCHSORT semantic presentation

REAL is complex-membered ext-real-membered real-membered V7() set

NAT is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V7() non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal limit_cardinal ordinal-membered Element of bool REAL

bool REAL is non empty set

NAT is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V7() non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal limit_cardinal ordinal-membered set

bool NAT is non empty non trivial non finite set

bool NAT is non empty non trivial non finite set

0 is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V7() V8() empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued finite finite-yielding V53() cardinal {} -element Ordinal-yielding increasing V67() real V70() V71() decreasing non-decreasing non-increasing V79() ordinal-membered Element of NAT

RAT is complex-membered ext-real-membered real-membered rational-membered V7() set

{} is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V7() empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued finite finite-yielding V53() cardinal {} -element Ordinal-yielding increasing V67() V71() decreasing non-decreasing non-increasing V79() ordinal-membered set

the complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V7() empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued finite finite-yielding V53() cardinal {} -element Ordinal-yielding increasing V67() V71() decreasing non-decreasing non-increasing V79() ordinal-membered set is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V7() empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued finite finite-yielding V53() cardinal {} -element Ordinal-yielding increasing V67() V71() decreasing non-decreasing non-increasing V79() ordinal-membered set

1 is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal real V70() ordinal-membered Element of NAT

K158(NAT,0,1) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty finite V53() Element of bool NAT

K158(NAT,0,1) ^omega is non empty functional set

bool (K158(NAT,0,1) ^omega) is non empty set

[:NAT,REAL:] is Relation-like complex-valued ext-real-valued real-valued set

bool [:NAT,REAL:] is non empty set

K326() is set

{{},1} is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty finite V53() set

INT is complex-membered ext-real-membered real-membered rational-membered integer-membered V7() set

K412() is set

bool K412() is non empty set

K413() is Element of bool K412()

K453() is non empty V136() L10()

the carrier of K453() is non empty set

K416( the carrier of K453()) is non empty M30( the carrier of K453())

K452(K453()) is Element of bool K416( the carrier of K453())

bool K416( the carrier of K453()) is non empty set

[:K452(K453()),NAT:] is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set

bool [:K452(K453()),NAT:] is non empty set

[:NAT,K452(K453()):] is Relation-like set

bool [:NAT,K452(K453()):] is non empty set

2 is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal real V70() ordinal-membered Element of NAT

K317(2,K326()) is M14(K326())

[:K317(2,K326()),K326():] is Relation-like set

bool [:K317(2,K326()),K326():] is non empty set

3 is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal real V70() ordinal-membered Element of NAT

K317(3,K326()) is M14(K326())

[:K317(3,K326()),K326():] is Relation-like set

bool [:K317(3,K326()),K326():] is non empty set

K509() is Relation-like K317(2,K326()) -defined K326() -valued Function-like quasi_total Element of bool [:K317(2,K326()),K326():]

{{}} is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty trivial functional finite V53() 1 -element V90() set

O is epsilon-transitive epsilon-connected ordinal ordinal-membered set

A is epsilon-transitive epsilon-connected ordinal ordinal-membered set

O +^ A is epsilon-transitive epsilon-connected ordinal ordinal-membered set

(O +^ A) \ O is ordinal-membered Element of bool (O +^ A)

bool (O +^ A) is non empty set

C is set

B is epsilon-transitive epsilon-connected ordinal ordinal-membered set

B -^ O is epsilon-transitive epsilon-connected ordinal ordinal-membered set

c

O +^ c

B is epsilon-transitive epsilon-connected ordinal ordinal-membered set

O +^ B is epsilon-transitive epsilon-connected ordinal ordinal-membered set

O is epsilon-transitive epsilon-connected ordinal ordinal-membered set

A is epsilon-transitive epsilon-connected ordinal ordinal-membered set

C is epsilon-transitive epsilon-connected ordinal ordinal-membered set

B is epsilon-transitive epsilon-connected ordinal ordinal-membered set

O is set

A is set

{O} is non empty trivial finite 1 -element set

A \/ {O} is non empty set

(A \/ {O}) \ A is Element of bool (A \/ {O})

bool (A \/ {O}) is non empty set

O is set

succ O is non empty set

{O} is non empty trivial finite 1 -element set

O \/ {O} is non empty set

(succ O) \ O is Element of bool (succ O)

bool (succ O) is non empty set

O is Relation-like Function-like set

proj1 O is set

A is Relation-like set

O .: A is set

C is set

B is set

O . B is set

c

f is set

[c

{c

{c

{{c

O . (c

O . [c

B is set

c

[B,c

{B,c

{B} is non empty trivial finite 1 -element set

{{B,c

O . (B,c

O . [B,c

O is epsilon-transitive epsilon-connected ordinal ordinal-membered set

union O is epsilon-transitive epsilon-connected ordinal ordinal-membered set

A is epsilon-transitive epsilon-connected ordinal ordinal-membered set

O \ A is ordinal-membered Element of bool O

bool O is non empty set

inf (O \ A) is epsilon-transitive epsilon-connected ordinal ordinal-membered set

On (O \ A) is ordinal-membered set

K181((On (O \ A))) is set

sup (O \ A) is epsilon-transitive epsilon-connected ordinal ordinal-membered set

union (O \ A) is epsilon-transitive epsilon-connected ordinal ordinal-membered set

the epsilon-transitive epsilon-connected ordinal ordinal-membered Element of O \ A is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of O \ A

B is epsilon-transitive epsilon-connected ordinal ordinal-membered set

B is set

c

f is epsilon-transitive epsilon-connected ordinal ordinal-membered set

f is epsilon-transitive epsilon-connected ordinal ordinal-membered set

f is epsilon-transitive epsilon-connected ordinal ordinal-membered set

O is epsilon-transitive epsilon-connected ordinal ordinal-membered set

A is epsilon-transitive epsilon-connected ordinal ordinal-membered set

O \ A is ordinal-membered Element of bool O

bool O is non empty set

the epsilon-transitive epsilon-connected ordinal ordinal-membered Element of O \ A is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of O \ A

B is epsilon-transitive epsilon-connected ordinal ordinal-membered set

A +^ B is epsilon-transitive epsilon-connected ordinal ordinal-membered set

c

proj1 c

f is set

c

k is set

c

f is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal real V70() ordinal-membered Element of NAT

c

A +^ f is epsilon-transitive epsilon-connected ordinal ordinal-membered set

c

c

A +^ c

proj2 c

A +^ NAT is epsilon-transitive epsilon-connected ordinal ordinal-membered set

f is set

k is set

c

f is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal real V70() ordinal-membered Element of NAT

A +^ f is epsilon-transitive epsilon-connected ordinal ordinal-membered set

O is Relation-like Function-like set

proj1 O is set

A is Relation-like Function-like set

proj1 A is set

C is epsilon-transitive epsilon-connected ordinal ordinal-membered set

B is epsilon-transitive epsilon-connected ordinal ordinal-membered set

C \ B is ordinal-membered Element of bool C

bool C is non empty set

O is Relation-like Function-like set

proj1 O is set

A is epsilon-transitive epsilon-connected ordinal ordinal-membered set

C is epsilon-transitive epsilon-connected ordinal ordinal-membered set

A \ C is ordinal-membered Element of bool A

bool A is non empty set

B is epsilon-transitive epsilon-connected ordinal ordinal-membered set

c

f is epsilon-transitive epsilon-connected ordinal ordinal-membered set

O is Relation-like Function-like set

A is T-Sequence-like Relation-like Function-like set

proj1 A is epsilon-transitive epsilon-connected ordinal ordinal-membered set

proj1 O is set

(proj1 A) \ {} is ordinal-membered Element of bool (proj1 A)

bool (proj1 A) is non empty set

O is Relation-like Function-like set

A is Relation-like Function-like FinSequence-like set

len A is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal real V70() ordinal-membered Element of NAT

succ (len A) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal ordinal-membered set

{(len A)} is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty trivial finite V53() 1 -element set

(len A) \/ {(len A)} is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty finite set

proj1 O is set

C is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal ordinal-membered set

B is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal real V70() ordinal-membered Element of NAT

C \ B is finite ordinal-membered Element of bool C

bool C is non empty finite V53() set

f is set

dom A is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT

k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set

c

succ {} is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal ordinal-membered set

{} \/ {{}} is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty finite V53() set

k is set

f is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal real V70() ordinal-membered Element of NAT

f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set

c

O is epsilon-transitive epsilon-connected ordinal ordinal-membered set

A is Relation-like Function-like set

proj1 A is set

C is epsilon-transitive epsilon-connected ordinal ordinal-membered set

B is epsilon-transitive epsilon-connected ordinal ordinal-membered set

C \ B is ordinal-membered Element of bool C

bool C is non empty set

the epsilon-transitive epsilon-connected ordinal ordinal-membered Element of C \ B is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of C \ B

O \ O is ordinal-membered Element of bool O

bool O is non empty set

C is epsilon-transitive epsilon-connected ordinal ordinal-membered set

C \ O is ordinal-membered Element of bool C

bool C is non empty set

B is epsilon-transitive epsilon-connected ordinal ordinal-membered set

O is epsilon-transitive epsilon-connected ordinal ordinal-membered set

A is Relation-like Function-like set

proj1 A is set

sup (proj1 A) is epsilon-transitive epsilon-connected ordinal ordinal-membered set

C is epsilon-transitive epsilon-connected ordinal ordinal-membered set

B is epsilon-transitive epsilon-connected ordinal ordinal-membered set

C \ B is ordinal-membered Element of bool C

bool C is non empty set

the epsilon-transitive epsilon-connected ordinal ordinal-membered Element of C \ B is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of C \ B

f is epsilon-transitive epsilon-connected ordinal ordinal-membered set

O \ f is ordinal-membered Element of bool O

bool O is non empty set

C is epsilon-transitive epsilon-connected ordinal ordinal-membered set

O \ C is ordinal-membered Element of bool O

bool O is non empty set

sup (proj1 A) is epsilon-transitive epsilon-connected ordinal ordinal-membered set

O is Relation-like Function-like set

C is epsilon-transitive epsilon-connected ordinal ordinal-membered set

proj1 O is set

A is T-Sequence-like Relation-like Function-like () set

proj1 A is epsilon-transitive epsilon-connected ordinal ordinal-membered set

O is Relation-like Function-like set

C is epsilon-transitive epsilon-connected ordinal ordinal-membered set

proj1 O is set

A is Relation-like Function-like FinSequence-like () set

dom A is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT

B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set

len A is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal real V70() ordinal-membered Element of NAT

O is Relation-like Function-like set

proj1 O is set

inf (proj1 O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set

On (proj1 O) is ordinal-membered set

K181((On (proj1 O))) is set

C is epsilon-transitive epsilon-connected ordinal ordinal-membered set

O is Relation-like Function-like set

proj1 O is set

sup (proj1 O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set

O is epsilon-transitive epsilon-connected ordinal ordinal-membered set

A is epsilon-transitive epsilon-connected ordinal ordinal-membered set

C is Relation-like Function-like set

proj1 C is set

sup (proj1 C) is epsilon-transitive epsilon-connected ordinal ordinal-membered set

O is Relation-like Function-like set

proj1 O is set

inf (proj1 O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set

On (proj1 O) is ordinal-membered set

K181((On (proj1 O))) is set

C is epsilon-transitive epsilon-connected ordinal ordinal-membered set

B is epsilon-transitive epsilon-connected ordinal ordinal-membered set

A is epsilon-transitive epsilon-connected ordinal ordinal-membered set

C is epsilon-transitive epsilon-connected ordinal ordinal-membered set

B is epsilon-transitive epsilon-connected ordinal ordinal-membered set

sup (proj1 O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set

C is epsilon-transitive epsilon-connected ordinal ordinal-membered set

B is epsilon-transitive epsilon-connected ordinal ordinal-membered set

A is epsilon-transitive epsilon-connected ordinal ordinal-membered set

C is epsilon-transitive epsilon-connected ordinal ordinal-membered set

B is epsilon-transitive epsilon-connected ordinal ordinal-membered set

sup (proj1 O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set

O is Relation-like Function-like set

(O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set

(O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set

(O) -^ (O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set

({}) is epsilon-transitive epsilon-connected ordinal ordinal-membered set

({}) is epsilon-transitive epsilon-connected ordinal ordinal-membered set

({}) is epsilon-transitive epsilon-connected ordinal ordinal-membered set

({}) -^ ({}) is epsilon-transitive epsilon-connected ordinal ordinal-membered set

dom {} is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V7() empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued finite finite-yielding V53() cardinal {} -element Ordinal-yielding increasing V67() V71() decreasing non-decreasing non-increasing V79() ordinal-membered () ( {} ) Element of bool NAT

O is epsilon-transitive epsilon-connected ordinal ordinal-membered set

O is Relation-like Function-like set

(O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set

proj1 O is set

sup (proj1 O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set

On (proj1 O) is ordinal-membered set

A is set

A is epsilon-transitive epsilon-connected ordinal ordinal-membered set

A is epsilon-transitive epsilon-connected ordinal ordinal-membered set

O is Relation-like Function-like set

(O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set

proj1 O is set

sup (proj1 O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set

O is epsilon-transitive epsilon-connected ordinal ordinal-membered set

A is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V7() empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued finite finite-yielding V53() cardinal {} -element Ordinal-yielding increasing V67() V71() decreasing non-decreasing non-increasing V79() ordinal-membered () ( {} ) set

C is epsilon-transitive epsilon-connected ordinal ordinal-membered set

proj1 A is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V7() empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued finite finite-yielding V53() cardinal {} -element Ordinal-yielding increasing V67() V71() decreasing non-decreasing non-increasing V79() ordinal-membered () ( {} ) set

C is set

A is set

O is epsilon-transitive epsilon-connected ordinal ordinal-membered set

[:C,A:] is Relation-like set

bool [:C,A:] is non empty set

{} [:C,A:] is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V7() empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued finite finite-yielding V53() cardinal {} -element Ordinal-yielding increasing V67() V71() decreasing non-decreasing non-increasing V79() ordinal-membered () ( {} ) Element of bool [:C,A:]

B is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V7() empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued finite finite-yielding V53() cardinal {} -element Ordinal-yielding increasing V67() V71() decreasing non-decreasing non-increasing V79() ordinal-membered () ( {} ) Element of bool [:C,A:]

O is Relation-like Function-like () set

proj1 O is set

A is epsilon-transitive epsilon-connected ordinal ordinal-membered set

C is epsilon-transitive epsilon-connected ordinal ordinal-membered set

A \ C is ordinal-membered Element of bool A

bool A is non empty set

O is Relation-like Function-like () set

proj1 O is ordinal-membered set

sup (proj1 O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set

proj1 O is ordinal-membered set

sup (proj1 O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set

O is Relation-like Function-like () set

proj1 O is ordinal-membered set

A is epsilon-transitive epsilon-connected ordinal ordinal-membered set

C is epsilon-transitive epsilon-connected ordinal ordinal-membered set

A \ C is ordinal-membered Element of bool A

bool A is non empty set

the epsilon-transitive epsilon-connected ordinal ordinal-membered Element of A \ C is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of A \ C

O is Relation-like Function-like set

(O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set

proj1 O is set

inf (proj1 O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set

On (proj1 O) is ordinal-membered set

K181((On (proj1 O))) is set

B is epsilon-transitive epsilon-connected ordinal ordinal-membered set

the epsilon-transitive epsilon-connected ordinal ordinal-membered Element of On (proj1 O) is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of On (proj1 O)

B is epsilon-transitive epsilon-connected ordinal ordinal-membered set

O is Relation-like Function-like set

(O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set

proj1 O is set

inf (proj1 O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set

On (proj1 O) is ordinal-membered set

K181((On (proj1 O))) is set

O is Relation-like Function-like () set

proj1 O is ordinal-membered set

(O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set

(O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set

(O) \ (O) is ordinal-membered Element of bool (O)

bool (O) is non empty set

A is epsilon-transitive epsilon-connected ordinal ordinal-membered set

C is epsilon-transitive epsilon-connected ordinal ordinal-membered set

A \ C is ordinal-membered Element of bool A

bool A is non empty set

sup (proj1 O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set

inf (proj1 O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set

On (proj1 O) is ordinal-membered set

K181((On (proj1 O))) is set

B is set

B is set

c

f is epsilon-transitive epsilon-connected ordinal ordinal-membered set

O is epsilon-transitive epsilon-connected ordinal ordinal-membered set

A is epsilon-transitive epsilon-connected ordinal ordinal-membered set

O \ A is ordinal-membered Element of bool O

bool O is non empty set

C is Relation-like Function-like () set

proj1 C is ordinal-membered set

(C) is epsilon-transitive epsilon-connected ordinal ordinal-membered set

(C) is epsilon-transitive epsilon-connected ordinal ordinal-membered set

the epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 C is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 C

sup (proj1 C) is epsilon-transitive epsilon-connected ordinal ordinal-membered set

c

c

sup O is epsilon-transitive epsilon-connected ordinal ordinal-membered set

O is T-Sequence-like Relation-like Function-like () ( {} ) set

(O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set

(O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set

proj1 O is epsilon-transitive epsilon-connected ordinal ordinal-membered set

(O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set

(O) -^ (O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set

(proj1 O) \ {} is ordinal-membered Element of bool (proj1 O)

bool (proj1 O) is non empty set

O is epsilon-transitive epsilon-connected ordinal ordinal-membered set

C is set

A is epsilon-transitive epsilon-connected ordinal ordinal-membered set

the complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V7() empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like non-empty empty-yielding O -defined C -valued Function-like one-to-one constant functional ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued finite finite-yielding V53() cardinal {} -element Ordinal-yielding increasing V67() V71() decreasing non-decreasing non-increasing V79() ordinal-membered () ( {} ) set is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V7() empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like non-empty empty-yielding O -defined C -valued Function-like one-to-one constant functional ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued finite finite-yielding V53() cardinal {} -element Ordinal-yielding increasing V67() V71() decreasing non-decreasing non-increasing V79() ordinal-membered () ( {} ) set

O is epsilon-transitive epsilon-connected ordinal ordinal-membered set

A is set

[O,A] is V30() set

{O,A} is non empty finite set

{O} is non empty trivial finite 1 -element set

{{O,A},{O}} is non empty finite V53() set

{[O,A]} is non empty trivial Relation-like Function-like constant finite 1 -element set

succ O is non empty epsilon-transitive epsilon-connected ordinal ordinal-membered set

O \/ {O} is non empty set

proj1 {[O,A]} is non empty trivial finite 1 -element set

(succ O) \ O is ordinal-membered Element of bool (succ O)

bool (succ O) is non empty set

O is epsilon-transitive epsilon-connected ordinal ordinal-membered set

A is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set

[O,A] is V30() set

{O,A} is non empty finite set

{O} is non empty trivial finite 1 -element set

{{O,A},{O}} is non empty finite V53() set

{[O,A]} is non empty trivial Relation-like Function-like constant finite 1 -element () set

C is Relation-like Function-like () set

proj2 C is set

{A} is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty trivial finite V53() 1 -element set

O is epsilon-transitive epsilon-connected ordinal ordinal-membered set

A is real set

[O,A] is V30() set

{O,A} is non empty finite set

{O} is non empty trivial finite 1 -element set

{{O,A},{O}} is non empty finite V53() set

{[O,A]} is non empty trivial Relation-like Function-like constant finite 1 -element () set

C is Relation-like Function-like () set

proj2 C is set

{A} is complex-membered ext-real-membered real-membered non empty trivial finite 1 -element set

A is non empty set

O is epsilon-transitive epsilon-connected ordinal ordinal-membered set

C is Element of A

[O,C] is V30() set

{O,C} is non empty finite set

{O} is non empty trivial finite 1 -element set

{{O,C},{O}} is non empty finite V53() set

{[O,C]} is non empty trivial Relation-like Function-like constant finite 1 -element () set

B is Relation-like Function-like () set

proj2 B is set

{C} is non empty trivial finite 1 -element set

O is epsilon-transitive epsilon-connected ordinal ordinal-membered set

A is set

[O,A] is V30() set

{O,A} is non empty finite set

{O} is non empty trivial finite 1 -element set

{{O,A},{O}} is non empty finite V53() set

{[O,A]} is non empty trivial Relation-like Function-like constant finite 1 -element () set

succ O is non empty epsilon-transitive epsilon-connected ordinal ordinal-membered set

O \/ {O} is non empty set

C is Relation-like Function-like () set

proj1 C is ordinal-membered set

B is epsilon-transitive epsilon-connected ordinal ordinal-membered set

sup (proj1 C) is epsilon-transitive epsilon-connected ordinal ordinal-membered set

O is epsilon-transitive epsilon-connected ordinal ordinal-membered set

the epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set

[O, the epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set ] is V30() set

{O, the epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set } is non empty finite set

{O} is non empty trivial finite 1 -element set

{{O, the epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set },{O}} is non empty finite V53() set

{[O, the epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set ]} is non empty trivial Relation-like RAT -valued Function-like constant complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing finite 1 -element () (O) ( succ O) set

succ O is non empty epsilon-transitive epsilon-connected ordinal ordinal-membered set

O \/ {O} is non empty set

C is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued () set

A is non empty set

the Element of A is Element of A

[O, the Element of A] is V30() set

{O, the Element of A} is non empty finite set

{O} is non empty trivial finite 1 -element set

{{O, the Element of A},{O}} is non empty finite V53() set

{[O, the Element of A]} is non empty trivial Relation-like A -valued Function-like constant finite 1 -element () (O) ( succ O) set

succ O is non empty epsilon-transitive epsilon-connected ordinal ordinal-membered set

O \/ {O} is non empty set

B is Relation-like A -valued Function-like () set

O is Relation-like Function-like () set

proj1 O is ordinal-membered set

union (proj1 O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set

O . (union (proj1 O)) is set

O is T-Sequence-like Relation-like Function-like () ( {} ) set

last O is set

proj1 O is epsilon-transitive epsilon-connected ordinal ordinal-membered set

union (proj1 O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set

O . (union (proj1 O)) is set

(O) is set

O is Relation-like Function-like finite () set

proj1 O is finite ordinal-membered set

A is epsilon-transitive epsilon-connected ordinal ordinal-membered set

O . A is set

C is epsilon-transitive epsilon-connected ordinal ordinal-membered set

O . C is set

B is epsilon-transitive epsilon-connected ordinal ordinal-membered set

c

B \ c

bool B is non empty set

f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set

c

k is epsilon-transitive epsilon-connected ordinal ordinal-membered set

c

f is epsilon-transitive epsilon-connected ordinal ordinal-membered set

c

c

succ c

{c

c

succ A is non empty epsilon-transitive epsilon-connected ordinal ordinal-membered set

{A} is non empty trivial finite 1 -element set

A \/ {A} is non empty set

c

p is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set

q is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal real V70() ordinal-membered Element of NAT

y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set

q + y is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal real V70() ordinal-membered Element of NAT

(succ A) +^ {} is epsilon-transitive epsilon-connected ordinal ordinal-membered set

O . H

b is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set

(succ A) +^ b is epsilon-transitive epsilon-connected ordinal ordinal-membered set

O . H

b + 1 is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal real V70() ordinal-membered Element of NAT

(succ A) +^ (b + 1) is epsilon-transitive epsilon-connected ordinal ordinal-membered set

O . H

succ b is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal ordinal-membered set

{b} is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty trivial finite V53() 1 -element set

b \/ {b} is non empty finite set

succ H

{((succ A) +^ b)} is non empty trivial finite 1 -element set

((succ A) +^ b) \/ {((succ A) +^ b)} is non empty set

y is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal real V70() ordinal-membered Element of NAT

q +^ y is epsilon-transitive epsilon-connected ordinal ordinal-membered set

c

(succ A) +^ y is epsilon-transitive epsilon-connected ordinal ordinal-membered set

O is Relation-like Function-like () set

(O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set

(O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set

(O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set

(O) -^ (O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set

proj1 O is ordinal-membered set

A is epsilon-transitive epsilon-connected ordinal ordinal-membered set

O . A is set

C is epsilon-transitive epsilon-connected ordinal ordinal-membered set

O . C is set

B is epsilon-transitive epsilon-connected ordinal ordinal-membered set

c

B \ c

bool B is non empty set

c

f is epsilon-transitive epsilon-connected ordinal ordinal-membered set

c

k is epsilon-transitive epsilon-connected ordinal ordinal-membered set

c

f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set

succ f is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal ordinal-membered set

{f} is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty trivial finite V53() 1 -element set

f \/ {f} is non empty finite set

succ A is non empty epsilon-transitive epsilon-connected ordinal ordinal-membered set

{A} is non empty trivial finite 1 -element set

A \/ {A} is non empty set

c

c

p is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal real V70() ordinal-membered Element of NAT

q is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set

p + q is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal real V70() ordinal-membered Element of NAT

(succ A) +^ {} is epsilon-transitive epsilon-connected ordinal ordinal-membered set

O . H

y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set

(succ A) +^ y is epsilon-transitive epsilon-connected ordinal ordinal-membered set

O . H

y + 1 is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal real V70() ordinal-membered Element of NAT

(succ A) +^ (y + 1) is epsilon-transitive epsilon-connected ordinal ordinal-membered set

O . H

succ y is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal ordinal-membered set

{y} is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty trivial finite V53() 1 -element set

y \/ {y} is non empty finite set

succ H

{((succ A) +^ y)} is non empty trivial finite 1 -element set

((succ A) +^ y) \/ {((succ A) +^ y)} is non empty set

y is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal real V70() ordinal-membered Element of NAT

p +^ y is epsilon-transitive epsilon-connected ordinal ordinal-membered set

c

(succ A) +^ y is epsilon-transitive epsilon-connected ordinal ordinal-membered set

O is T-Sequence-like Relation-like Function-like () ( {} ) set

O . {} is set

proj1 O is epsilon-transitive epsilon-connected ordinal ordinal-membered set

A is T-Sequence-like Relation-like Function-like () ( {} ) set

proj1 A is epsilon-transitive epsilon-connected ordinal ordinal-membered set

C is epsilon-transitive epsilon-connected ordinal ordinal-membered set

O . C is set

succ C is non empty epsilon-transitive epsilon-connected ordinal ordinal-membered set

{C} is non empty trivial finite 1 -element set

C \/ {C} is non empty set

O . (succ C) is set

C is epsilon-transitive epsilon-connected ordinal ordinal-membered set

O . C is set

C is epsilon-transitive epsilon-connected ordinal ordinal-membered set

A . C is set

B is epsilon-transitive epsilon-connected ordinal ordinal-membered set

A . B is set

O . C is set

len (O . C) is epsilon-transitive epsilon-connected ordinal cardinal ordinal-membered set

O . B is set

len (O . B) is epsilon-transitive epsilon-connected ordinal cardinal ordinal-membered set

O is T-Sequence-like Relation-like Function-like () ( {} ) set

O . {} is set

proj1 O is epsilon-transitive epsilon-connected ordinal ordinal-membered set

(O) is set

union (proj1 O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set

O . (union (proj1 O)) is set

A is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set

union A is epsilon-transitive epsilon-connected ordinal ordinal-membered set

B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set

B + 1 is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal real V70() ordinal-membered Element of NAT

succ B is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal ordinal-membered set

{B} is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty trivial finite V53() 1 -element set

B \/ {B} is non empty finite set

O . (union A) is set

F

F

F

proj1 F

O is T-Sequence-like Relation-like Function-like () ( {} ) set

proj1 O is epsilon-transitive epsilon-connected ordinal ordinal-membered set

O | NAT is T-Sequence-like Relation-like proj2 O -valued Function-like () ( {} ) set

proj2 O is set

proj1 (O | NAT) is epsilon-transitive epsilon-connected ordinal ordinal-membered set

((O | NAT)) is epsilon-transitive epsilon-connected ordinal ordinal-membered set

((O | NAT)) is epsilon-transitive epsilon-connected ordinal ordinal-membered set

((O | NAT)) is epsilon-transitive epsilon-connected ordinal ordinal-membered set

((O | NAT)) -^ ((O | NAT)) is epsilon-transitive epsilon-connected ordinal ordinal-membered set

(O | NAT) . {} is set

O . {} is set

C is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set

(O | NAT) . C is set

C + 1 is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal real V70() ordinal-membered Element of NAT

(O | NAT) . (C + 1) is set

succ C is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal ordinal-membered set

{C} is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty trivial finite V53() 1 -element set

C \/ {C} is non empty finite set

O . C is set

(O | NAT) . (succ C) is set

O . (succ C) is set

F

F

F

F

C is epsilon-transitive epsilon-connected ordinal ordinal-membered set

succ C is non empty epsilon-transitive epsilon-connected ordinal ordinal-membered set

{C} is non empty trivial finite 1 -element set

C \/ {C} is non empty set

(O | NAT) . (succ C) is set

(O | NAT) . C is set

B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set

(O | NAT) . B is set

O . C is set

O . (succ C) is set

F

F

F

F

O is set

A is Relation-like O -defined Function-like set

C is set

B is set

Swap (A,C,B) is Relation-like Function-like set

proj1 (Swap (A,C,B)) is set

dom A is Element of bool O

bool O is non empty set

O is set

A is Relation-like O -valued Function-like set

C is set

B is set

Swap (A,C,B) is Relation-like Function-like set

proj2 (Swap (A,C,B)) is set

proj2 A is set

O is set

A is set

C is Relation-like Function-like set

proj1 C is set

Swap (C,O,A) is Relation-like Function-like set

(Swap (C,O,A)) . O is set

C . A is set

C +* (O,(C . A)) is Relation-like Function-like set

C . O is set

(C +* (O,(C . A))) +* (A,(C . O)) is Relation-like Function-like set

proj1 (C +* (O,(C . A))) is set

(C +* (O,(C . A))) . O is set

O is set

A is set

C is set

B is Relation-like O -valued Function-like () set

proj1 B is ordinal-membered set

Swap (B,A,C) is Relation-like O -valued Function-like set

(Swap (B,A,C)) /. A is Element of O

B /. C is Element of O

proj1 (Swap (B,A,C)) is set

(Swap (B,A,C)) . A is set

B . C is set

O is set

A is set

C is Relation-like Function-like set

proj1 C is set

Swap (C,O,A) is Relation-like Function-like set

(Swap (C,O,A)) . A is set

C . O is set

C . A is set

C +* (O,(C . A)) is Relation-like Function-like set

(C +* (O,(C . A))) +* (A,(C . O)) is Relation-like Function-like set

proj1 (C +* (O,(C . A))) is set

O is set

A is set

C is set

B is Relation-like O -valued Function-like () set

proj1 B is ordinal-membered set

Swap (B,A,C) is Relation-like O -valued Function-like set

(Swap (B,A,C)) /. C is Element of O

B /. A is Element of O

proj1 (Swap (B,A,C)) is set

(Swap (B,A,C)) . C is set

B . A is set

O is set

A is set

C is set

B is Relation-like Function-like set

Swap (B,A,C) is Relation-like Function-like set

(Swap (B,A,C)) . O is set

B . O is set

proj1 B is set

B . C is set

B +* (A,(B . C)) is Relation-like Function-like set

B . A is set

(B +* (A,(B . C))) +* (C,(B . A)) is Relation-like Function-like set

(B +* (A,(B . C))) . O is set

proj1 B is set

proj1 B is set

O is set

A is set

C is set

B is set

c

proj1 c

Swap (c

(Swap (c

c

proj1 (Swap (c

(Swap (c

c

O is set

A is set

C is Relation-like Function-like set

proj1 C is set

Swap (C,O,A) is Relation-like Function-like set

Swap (C,A,O) is Relation-like Function-like set

proj1 (Swap (C,O,A)) is set

proj1 (Swap (C,A,O)) is set

B is set

(Swap (C,O,A)) . B is set

(Swap (C,A,O)) . B is set

(Swap (C,O,A)) . B is set

C . A is set

(Swap (C,A,O)) . B is set

(Swap (C,O,A)) . B is set

C . O is set

(Swap (C,A,O)) . B is set

(Swap (C,O,A)) . B is set

C . B is set

(Swap (C,A,O)) . B is set

O is non empty set

id O is non empty Relation-like O -defined O -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:O,O:]

[:O,O:] is non empty Relation-like set

bool [:O,O:] is non empty set

O is non empty set

A is non empty Relation-like O -valued Function-like onto set

proj1 A is non empty set

C is Element of proj1 A

B is Element of proj1 A

Swap (A,C,B) is Relation-like O -valued Function-like set

proj2 (Swap (A,C,B)) is set

proj2 A is non empty set

O is Relation-like Function-like () set

A is set

C is set

Swap (O,A,C) is Relation-like Function-like set

proj1 O is ordinal-membered set

B is epsilon-transitive epsilon-connected ordinal ordinal-membered set

c

B \ c

bool B is non empty set

proj1 (Swap (O,A,C)) is set

O is set

A is set

C is Relation-like Function-like () set

proj1 C is ordinal-membered set

Swap (C,O,A) is Relation-like Function-like () set

Swap ((Swap (C,O,A)),O,A) is Relation-like Function-like () set

proj1 (Swap ((Swap (C,O,A)),O,A)) is ordinal-membered set

proj1 (Swap (C,O,A)) is ordinal-membered set

f is set

(Swap ((Swap (C,O,A)),O,A)) . f is set

(Swap (C,O,A)) . f is set

C . f is set

(Swap ((Swap (C,O,A)),O,A)) . f is set

(Swap (C,O,A)) . A is set

C . f is set

(Swap ((Swap (C,O,A)),O,A)) . f is set

(Swap (C,O,A)) . O is set

C . f is set

O is Relation-like Function-like complex-valued ext-real-valued real-valued () set

A is set

C is set

Swap (O,A,C) is Relation-like Function-like () set

B is Relation-like Function-like () set

c

proj1 B is ordinal-membered set

B . c

proj1 O is ordinal-membered set

O . C is V8() ext-real real set

O . A is V8() ext-real real set

O . c

O is Relation-like Function-like () set

proj1 O is ordinal-membered set

[:(proj1 O),(proj1 O):] is Relation-like set

bool [:(proj1 O),(proj1 O):] is non empty set

id (proj1 O) is Relation-like proj1 O -defined proj1 O -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(proj1 O),(proj1 O):]

(id (proj1 O)) * O is Relation-like proj1 O -defined Function-like set

O is Relation-like Function-like () set

proj1 O is ordinal-membered set

proj2 O is set

A is Relation-like Function-like () (O)

proj1 A is ordinal-membered set

proj2 A is set

[:(proj1 O),(proj1 O):] is Relation-like set

bool [:(proj1 O),(proj1 O):] is non empty set

C is Relation-like proj1 O -defined proj1 O -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(proj1 O),(proj1 O):]

C * O is Relation-like proj1 O -defined Function-like set

proj2 C is set

dom C is Element of bool (proj1 O)

bool (proj1 O) is non empty set

O is Relation-like Function-like () set

proj1 O is ordinal-membered set

id (proj1 O) is Relation-like proj1 O -defined proj1 O -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(proj1 O),(proj1 O):]

[:(proj1 O),(proj1 O):] is Relation-like set

bool [:(proj1 O),(proj1 O):] is non empty set

(id (proj1 O)) * O is Relation-like proj1 O -defined Function-like set

O is Relation-like Function-like () set

A is Relation-like Function-like () set

proj1 O is ordinal-membered set

proj1 A is ordinal-membered set

[:(proj1 A),(proj1 A):] is Relation-like set

bool [:(proj1 A),(proj1 A):] is non empty set

C is Relation-like proj1 A -defined proj1 A -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(proj1 A),(proj1 A):]

C * A is Relation-like proj1 A -defined Function-like set

[:(proj1 O),(proj1 O):] is Relation-like set

bool [:(proj1 O),(proj1 O):] is non empty set

C " is Relation-like proj1 A -defined proj1 A -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(proj1 A),(proj1 A):]

B is Relation-like proj1 O -defined proj1 O -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(proj1 O),(proj1 O):]

B * O is Relation-like proj1 O -defined Function-like set

id (proj1 A) is Relation-like proj1 A -defined proj1 A -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(proj1 A),(proj1 A):]

(id (proj1 A)) * A is Relation-like proj1 A -defined Function-like set

C * B is Relation-like proj1 O -defined proj1 A -valued Function-like one-to-one Element of bool [:(proj1 O),(proj1 A):]

[:(proj1 O),(proj1 A):] is Relation-like set

bool [:(proj1 O),(proj1 A):] is non empty set

(C * B) * A is Relation-like proj1 O -defined Function-like set

O is Relation-like Function-like () set

A is Relation-like Function-like () set

C is Relation-like Function-like () set

proj1 C is ordinal-membered set

proj1 A is ordinal-membered set

[:(proj1 A),(proj1 A):] is Relation-like set

bool [:(proj1 A),(proj1 A):] is non empty set

B is Relation-like proj1 A -defined proj1 A -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(proj1 A),(proj1 A):]

B * A is Relation-like proj1 A -defined Function-like set

[:(proj1 C),(proj1 C):] is Relation-like set

bool [:(proj1 C),(proj1 C):] is non empty set

c

c

c

[:(proj1 A),(proj1 C):] is Relation-like set

bool [:(proj1 A),(proj1 C):] is non empty set

f is Relation-like proj1 C -defined proj1 C -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(proj1 C),(proj1 C):]

f * C is Relation-like proj1 C -defined Function-like set

O is set

id O is Relation-like O -defined O -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:O,O:]

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

bool [:O,O:] is non empty set

A is set

C is set

Swap ((id O),A,C) is Relation-like O -defined O -valued Function-like set

dom (id O) is Element of bool O

bool O is non empty set

f is set

proj1 (Swap ((id O),A,C)) is set

(Swap ((id O),A,C)) . f is set

k is set

(Swap ((id O),A,C)) . k is set

dom (Swap ((id O),A,C)) is Element of bool O

(id O) . f is set

(id O) . k is set

(id O) . A is set

(id O) . C is set

O is non empty set

id O is non empty Relation-like O -defined O -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:O,O:]

[:O,O:] is non empty Relation-like set

bool [:O,O:] is non empty set

A is Element of O

C is Element of O

Swap ((id O),A,C) is Relation-like O -defined O -valued Function-like set

O is non empty set

id O is non empty Relation-like O -defined O -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:O,O:]

[:O,O:] is non empty Relation-like set

bool [:O,O:] is non empty set

A is Element of O

C is Element of O

Swap ((id O),A,C) is Relation-like O -defined O -valued Function-like one-to-one set

dom (id O) is non empty Element of bool O

bool O is non empty set

B is Element of dom (id O)

c

Swap ((id O),B,c

dom (Swap ((id O),A,C)) is Element of bool O

O is non empty set

A is non empty set

[:O,A:] is non empty Relation-like set

bool [:O,A:] is non empty set

C is non empty Relation-like O -defined A -valued Function-like total quasi_total Element of bool [:O,A:]

B is Element of O

c

Swap (C,B,c

dom C is non empty Element of bool O

bool O is non empty set

dom (Swap (C,B,c

proj2 (Swap (C,B,c

proj2 C is non empty set

O is set

A is set

id A is Relation-like A -defined A -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:A,A:]

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

bool [:A,A:] is non empty set

C is set

Swap ((id A),O,C) is Relation-like A -defined A -valued Function-like set

B is Relation-like Function-like set

c

proj1 c

Swap (c

B * c

dom (id A) is Element of bool A

bool A is non empty set

proj2 (id A) is set

proj1 B is set

proj2 B is set

proj1 (Swap (c

proj1 (B * c

f is set

(id A) . O is set

(id A) . C is set

(id A) . f is set

(Swap (c

c

B . f is set

c

c

(B * c

O is set

A is set

C is Relation-like Function-like () set

proj1 C is ordinal-membered set

Swap (C,O,A) is Relation-like Function-like () set

c

[:(proj1 C),(proj1 C):] is Relation-like set

bool [:(proj1 C),(proj1 C):] is non empty set

id c

[:c

bool [:c

f is Element of c

k is Element of c

(c

f is Relation-like proj1 C -defined proj1 C -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(proj1 C),(proj1 C):]

f * C is Relation-like proj1 C -defined Function-like set

O is set

A is set

C is Relation-like Function-like () set

proj1 C is ordinal-membered set

Swap (C,O,A) is Relation-like Function-like () set

B is Relation-like Function-like () set

Swap (B,O,A) is Relation-like Function-like () set

proj1 B is ordinal-membered set

O is RelStr

the carrier of O is set

A is Relation-like the carrier of O -valued Function-like () set

proj1 A is ordinal-membered set

{ [b

O is RelStr

the carrier of O is set

A is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V7() empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like non-empty empty-yielding NAT -defined the carrier of O -valued Function-like one-to-one constant functional ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued finite finite-yielding V53() cardinal {} -element Ordinal-yielding increasing V67() V71() decreasing non-decreasing non-increasing V79() ordinal-membered () ( {} ) set

C is epsilon-transitive epsilon-connected ordinal ordinal-membered set

proj1 A is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V7() empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued finite finite-yielding V53() cardinal {} -element Ordinal-yielding increasing V67() V71() decreasing non-decreasing non-increasing V79() ordinal-membered () ( {} ) set

A /. C is Element of the carrier of O

B is epsilon-transitive epsilon-connected ordinal ordinal-membered set

A /. B is Element of the carrier of O

A is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V7() empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like non-empty empty-yielding NAT -defined the carrier of O -valued the carrier of O -valued Function-like one-to-one constant functional ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued finite finite-yielding V53() cardinal {} -element Ordinal-yielding increasing V67() V71() decreasing non-decreasing non-increasing V79() ordinal-membered () ( {} ) (O) set

(O,A) is set

proj1 A is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V7() empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued finite finite-yielding V53() cardinal {} -element Ordinal-yielding increasing V67() V71() decreasing non-decreasing non-increasing V79() ordinal-membered () ( {} ) set

{ [b

the Element of (O,A) is Element of (O,A)

dom A is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V7() empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued finite finite-yielding V53() cardinal {} -element Ordinal-yielding increasing V67() V71() decreasing non-decreasing non-increasing V79() ordinal-membered () ( {} ) Element of bool NAT

B is V8() epsilon-transitive epsilon-connected ordinal natural Relation-like Function-like ext-real non negative finite cardinal real V70() ordinal-membered Element of dom A

c

[B,c

{B,c

{B} is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty trivial functional finite V53() 1 -element V90() set

{{B,c

A /. B is Element of the carrier of O

A /. c

O is non empty reflexive transitive antisymmetric connected RelStr

the carrier of O is non empty set

C is Element of the carrier of O

A is Element of the carrier of O

O is non empty reflexive transitive antisymmetric connected RelStr

the carrier of O is non empty set

A is Relation-like the carrier of O -valued Function-like () set

(O,A) is set

proj1 A is ordinal-membered set

{ [b

{ [b

B is set

c

f is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A

[c

{c

{c

{{c

A /. c

A /. f is Element of the carrier of O

B is set

c

f is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A

[c

{c

{c

{{c

A /. f is Element of the carrier of O

A /. c

B is set

c

O is set

A is set

[O,A] is V30() set

{O,A} is non empty finite set

{O} is non empty trivial finite 1 -element set

{{O,A},{O}} is non empty finite V53() set

C is non empty reflexive transitive antisymmetric connected RelStr

the carrier of C is non empty set

B is Relation-like the carrier of C -valued Function-like () set

(C,B) is set

proj1 B is ordinal-membered set

{ [b

{ [b

B /. A is Element of the carrier of C

B /. O is Element of the carrier of C

c

proj1 c

f is Element of proj1 c

k is Element of proj1 c

[f,k] is V30() set

{f,k} is non empty finite set

{f} is non empty trivial finite 1 -element set

{{f,k},{f}} is non empty finite V53() set

B /. f is Element of the carrier of C

B /. k is Element of the carrier of C

O is non empty reflexive transitive antisymmetric connected RelStr

the carrier of O is non empty set

A is Relation-like the carrier of O -valued Function-like () set

(O,A) is set

proj1 A is ordinal-membered set

{ [b

{ [b

[:(proj1 A),(proj1 A):] is Relation-like set

C is set

B is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A

c

[B,c

{B,c

{B} is non empty trivial finite 1 -element set

{{B,c

A /. c

A /. B is Element of the carrier of O

O is non empty reflexive transitive antisymmetric connected RelStr

the carrier of O is non empty set

A is Relation-like the carrier of O -valued Function-like finite () set

(O,A) is set

proj1 A is finite ordinal-membered set

{ [b

{ [b

[:(proj1 A),(proj1 A):] is Relation-like finite set

O is non empty reflexive transitive antisymmetric connected RelStr

the carrier of O is non empty set

A is Relation-like the carrier of O -valued Function-like () set

(O,A) is set

proj1 A is ordinal-membered set

{ [b

{ [b

the Element of (O,A) is Element of (O,A)

B is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A

c

[B,c

{B,c

{B} is non empty trivial finite 1 -element set

{{B,c

A /. c

A /. B is Element of the carrier of O

C is epsilon-transitive epsilon-connected ordinal ordinal-membered set

A /. C is Element of the carrier of O

B is epsilon-transitive epsilon-connected ordinal ordinal-membered set

A /. B is Element of the carrier of O

[C,B] is V30() set

{C,B} is non empty finite set

{C} is non empty trivial finite 1 -element set

{{C,B},{C}} is non empty finite V53() set

O is set

A is set

[O,A] is V30() set

{O,A} is non empty finite set

{O} is non empty trivial finite 1 -element set

{{O,A},{O}} is non empty finite V53() set

[A,O] is V30() set

{A,O} is non empty finite set

{A} is non empty trivial finite 1 -element set

{{A,O},{A}} is non empty finite V53() set

C is non empty reflexive transitive antisymmetric connected RelStr

the carrier of C is non empty set

B is Relation-like the carrier of C -valued Function-like () set

(C,B) is set

proj1 B is ordinal-membered set

{ [b

{ [b

O is set

A is set

[O,A] is V30() set

{O,A} is non empty finite set

{O} is non empty trivial finite 1 -element set

{{O,A},{O}} is non empty finite V53() set

C is set

[A,C] is V30() set

{A,C} is non empty finite set

{A} is non empty trivial finite 1 -element set

{{A,C},{A}} is non empty finite V53() set

[O,C] is V30() set

{O,C} is non empty finite set

{{O,C},{O}} is non empty finite V53() set

B is non empty reflexive transitive antisymmetric connected RelStr

the carrier of B is non empty set

c

(B,c

proj1 c

{ [b

{ [b

f is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 c

k is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 c

c

c

f is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 c

c

O is non empty reflexive transitive antisymmetric connected RelStr

the carrier of O is non empty set

A is Relation-like the carrier of O -valued Function-like () set

(O,A) is set

proj1 A is ordinal-membered set

{ [b

{ [b

[:(proj1 A),(proj1 A):] is Relation-like set

O is non empty reflexive transitive antisymmetric connected RelStr

the carrier of O is non empty set

A is Relation-like the carrier of O -valued Function-like () set

(O,A) is Relation-like set

proj1 A is ordinal-membered set

{ [b

{ [b

C is Relation-like set

B is set

field C is set

proj1 C is set

proj2 C is set

(proj1 C) \/ (proj2 C) is set

c

[B,c

{B,c

{B} is non empty trivial finite 1 -element set

{{B,c

[c

{c

{c

{{c

B is set

field C is set

proj1 C is set

proj2 C is set

(proj1 C) \/ (proj2 C) is set

c