:: CGAMES_1 semantic presentation

K100() is set

K104() is epsilon-transitive epsilon-connected ordinal non empty V39() cardinal limit_cardinal Element of K53(K100())

K53(K100()) is non empty set

omega is epsilon-transitive epsilon-connected ordinal non empty V39() cardinal limit_cardinal set

K53(omega) is non empty V39() set

K53(K104()) is non empty V39() set

K101() is set

K102() is set

K103() is set

{} is epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like non-empty empty-yielding K104() -defined Function-like one-to-one constant functional empty complex V32() ext-real non positive non negative V39() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V83() V89() set

1 is epsilon-transitive epsilon-connected ordinal natural non empty complex V32() ext-real positive non negative V39() cardinal Element of K104()

{{},1} is non empty set

K351() is set

K169(K104()) is functional non empty FinSequence-membered M9(K104())

K366(K104()) is functional non empty M13(K169(K104()),K104())

K53(K366(K104())) is non empty set

K123(K366(K104())) is non empty Element of K53(K53(K366(K104())))

K53(K53(K366(K104()))) is non empty set

K54(K104(),K123(K366(K104()))) is Relation-like non empty V39() set

K53(K54(K104(),K123(K366(K104())))) is non empty V39() set

2 is epsilon-transitive epsilon-connected ordinal natural non empty complex V32() ext-real positive non negative V39() cardinal Element of K104()

K105() is epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like non-empty empty-yielding K104() -defined Function-like one-to-one constant functional empty complex V32() ext-real non positive non negative V39() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V83() V89() Element of K104()

3 is epsilon-transitive epsilon-connected ordinal natural non empty complex V32() ext-real positive non negative V39() cardinal Element of K104()

Seg 1 is non empty V25() V39() 1 -element Element of K53(K104())

{ b

{1} is non empty V25() 1 -element set

Seg 2 is non empty V39() 2 -element Element of K53(K104())

{ b

{1,2} is non empty set

({},{}) is () ()

() is set

{ (b

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

dom g is epsilon-transitive epsilon-connected ordinal set

gR is epsilon-transitive epsilon-connected ordinal set

g | gR is T-Sequence-like Relation-like rng g -valued Function-like set

rng g is set

dom (g | gR) is epsilon-transitive epsilon-connected ordinal set

gR is epsilon-transitive epsilon-connected ordinal set

(g | gR) . gR is set

(g | gR) | gR is T-Sequence-like Relation-like rng g -valued rng (g | gR) -valued Function-like set

rng (g | gR) is set

rng ((g | gR) | gR) is set

union (rng ((g | gR) | gR)) is set

K53((union (rng ((g | gR) | gR)))) is non empty set

{ (b

g . gR is set

g | gR is T-Sequence-like Relation-like rng g -valued Function-like set

rng (g | gR) is set

union (rng (g | gR)) is set

K53((union (rng (g | gR)))) is non empty set

{ (b

g is epsilon-transitive epsilon-connected ordinal set

succ g is epsilon-transitive epsilon-connected ordinal non empty set

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

dom gR is epsilon-transitive epsilon-connected ordinal set

gR . g is set

gR is epsilon-transitive epsilon-connected ordinal set

gR . gR is set

gR | gR is T-Sequence-like Relation-like rng gR -valued Function-like set

rng gR is set

rng (gR | gR) is set

union (rng (gR | gR)) is set

K53((union (rng (gR | gR)))) is non empty set

{ (b

gR is set

gR is set

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

dom gRL is epsilon-transitive epsilon-connected ordinal set

gRL . g is set

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

dom gRL is epsilon-transitive epsilon-connected ordinal set

gRL . g is set

succ g is epsilon-transitive epsilon-connected ordinal non empty set

gRL | (succ g) is T-Sequence-like Relation-like rng gRL -valued Function-like set

rng gRL is set

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

dom g1 is epsilon-transitive epsilon-connected ordinal set

g1 . g is set

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

dom g1 is epsilon-transitive epsilon-connected ordinal set

g1 . g is set

g1 | (succ g) is T-Sequence-like Relation-like rng g1 -valued Function-like set

rng g1 is set

dom (gRL | (succ g)) is epsilon-transitive epsilon-connected ordinal set

gRL is epsilon-transitive epsilon-connected ordinal set

(gRL | (succ g)) | gRL is T-Sequence-like Relation-like rng gRL -valued rng (gRL | (succ g)) -valued Function-like set

rng (gRL | (succ g)) is set

(gRL | (succ g)) . gRL is set

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

rng s0 is set

union (rng s0) is set

K53((union (rng s0))) is non empty set

{ (b

dom (g1 | (succ g)) is epsilon-transitive epsilon-connected ordinal set

gRL is epsilon-transitive epsilon-connected ordinal set

(g1 | (succ g)) | gRL is T-Sequence-like Relation-like rng g1 -valued rng (g1 | (succ g)) -valued Function-like set

rng (g1 | (succ g)) is set

(g1 | (succ g)) . gRL is set

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

rng s0 is set

union (rng s0) is set

K53((union (rng s0))) is non empty set

{ (b

(gRL | (succ g)) . g is set

(g1 | (succ g)) . g is set

g is set

gR is epsilon-transitive epsilon-connected ordinal set

(gR) is set

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

dom gR is epsilon-transitive epsilon-connected ordinal set

gR . gR is set

gR | gR is T-Sequence-like Relation-like rng gR -valued Function-like set

rng gR is set

rng (gR | gR) is set

union (rng (gR | gR)) is set

K53((union (rng (gR | gR)))) is non empty set

{ (b

gRL is Element of K53((union (rng (gR | gR))))

gLR is Element of K53((union (rng (gR | gR))))

(gRL,gLR) is () ()

g1 is () ()

gR is () ()

gRL is set

the of gR is set

the of gR is set

the of gR \/ the of gR is set

s0 is set

dom (gR | gR) is epsilon-transitive epsilon-connected ordinal set

s1 is set

(gR | gR) . s1 is set

s1 is epsilon-transitive epsilon-connected ordinal set

(gR | gR) . s1 is set

gL is epsilon-transitive epsilon-connected ordinal set

gR . gL is set

(gL) is set

gRL is () ()

the of gRL is set

the of gRL is set

the of gRL \/ the of gRL is set

gRL is () ()

the of gRL is set

the of gRL is set

the of gRL \/ the of gRL is set

gLR is set

g1 is epsilon-transitive epsilon-connected ordinal set

(g1) is set

gR . g1 is set

({}) is set

{()} is non empty V25() 1 -element set

g is set

gR is () ()

the of gR is set

the of gR is set

the of gR \/ the of gR is set

gR is set

gRL is epsilon-transitive epsilon-connected ordinal set

(gRL) is set

{} \/ {} is Relation-like set

g is set

g is epsilon-transitive epsilon-connected ordinal set

(g) is set

gR is epsilon-transitive epsilon-connected ordinal set

(gR) is set

gR is set

gRL is () ()

the of gRL is set

the of gRL is set

the of gRL \/ the of gRL is set

gLR is set

g1 is epsilon-transitive epsilon-connected ordinal set

(g1) is set

g is epsilon-transitive epsilon-connected ordinal set

(g) is set

g is epsilon-transitive epsilon-connected ordinal set

(g) is non empty set

gR is Element of (g)

() is () Element of ({})

{()} is non empty V25() 1 -element set

({()},{}) is () ()

(1) is non empty set

the of ({()},{}) is set

the of ({()},{}) is set

the of ({()},{}) \/ the of ({()},{}) is set

gR is set

succ {} is epsilon-transitive epsilon-connected ordinal natural non empty complex V32() ext-real positive non negative V39() cardinal Element of omega

({()},{()}) is () ()

the of ({()},{()}) is set

the of ({()},{()}) is set

the of ({()},{()}) \/ the of ({()},{()}) is set

gR is set

succ {} is epsilon-transitive epsilon-connected ordinal natural non empty complex V32() ext-real positive non negative V39() cardinal Element of omega

() is () Element of (1)

() is () Element of (1)

g is () set

gR is epsilon-transitive epsilon-connected ordinal set

(gR) is non empty set

gR is () ()

the of gR is set

the of gR is set

the of gR \/ the of gR is set

g is ()

g is () set

gR is ()

the of gR is set

gRL is ()

gR is set

the of gRL is set

gLR is ()

gR is set

the of gLR is set

gR is ()

the of gR is set

gRL is ()

gR is set

the of gRL is set

gLR is ()

gR is set

the of gLR is set

g is () set

(g) is set

(g) is set

(g) \/ (g) is set

g is () set

(g) is set

(g) is set

gR is () set

(gR) is set

(gR) is set

gR is () ()

the of gR is set

gRL is () ()

the of gRL is set

the of gR is set

the of gRL is set

(()) is set

(()) is set

(()) is set

g is () set

(g) is set

(g) is set

(g) is set

(g) \/ (g) is set

gR is () ()

the of gR is set

the of gR is set

(()) is set

g is set

(()) is set

(()) is set

(()) is set

(()) \/ (()) is set

g is set

g is epsilon-transitive epsilon-connected ordinal set

(g) is non empty set

gR is () set

(gR) is set

(gR) is set

(gR) is set

(gR) \/ (gR) is set

gR is () ()

the of gR is set

the of gR is set

the of gR \/ the of gR is set

gRL is set

gR is () ()

the of gR is set

the of gR is set

the of gR \/ the of gR is set

gRL is set

gR is ()

the of gR is set

the of gR is set

the of gR \/ the of gR is set

g is set

gR is epsilon-transitive epsilon-connected ordinal set

(gR) is non empty set

gR is epsilon-transitive epsilon-connected ordinal set

(gR) is non empty set

gR is epsilon-transitive epsilon-connected ordinal set

(gR) is non empty set

gR is epsilon-transitive epsilon-connected ordinal set

(gR) is non empty set

g is set

gR is epsilon-transitive epsilon-connected ordinal set

(gR) is non empty set

gR is () set

(gR) is set

(gR) is set

(gR) is set

(gR) \/ (gR) is set

gRL is epsilon-transitive epsilon-connected ordinal set

(gRL) is non empty set

g is set

gR is epsilon-transitive epsilon-connected ordinal set

(gR) is non empty set

gR is () set

(gR) is set

(gR) is set

(gR) is set

(gR) \/ (gR) is set

g is epsilon-transitive epsilon-connected ordinal set

(g) is non empty set

gR is () set

(gR) is epsilon-transitive epsilon-connected ordinal set

((gR)) is non empty set

g is epsilon-transitive epsilon-connected ordinal set

gR is () set

(gR) is epsilon-transitive epsilon-connected ordinal set

gR is epsilon-transitive epsilon-connected ordinal set

(gR) is non empty set

gR is epsilon-transitive epsilon-connected ordinal set

(gR) is non empty set

gR is epsilon-transitive epsilon-connected ordinal set

(gR) is non empty set

g is () set

(g) is epsilon-transitive epsilon-connected ordinal set

gR is () set

(gR) is set

(gR) is set

(gR) is set

(gR) \/ (gR) is set

(gR) is epsilon-transitive epsilon-connected ordinal set

((gR)) is non empty set

gRL is epsilon-transitive epsilon-connected ordinal set

(gRL) is non empty set

g is () set

(g) is epsilon-transitive epsilon-connected ordinal set

gR is () set

(gR) is set

(gR) is set

(gR) is epsilon-transitive epsilon-connected ordinal set

(gR) is set

(gR) \/ (gR) is set

g is () set

(g) is set

(g) is set

(g) is set

(g) \/ (g) is set

(g) is epsilon-transitive epsilon-connected ordinal set

g is set

gR is () set

(gR) is set

(gR) is set

(gR) is set

(gR) \/ (gR) is set

gR is epsilon-transitive epsilon-connected ordinal set

(gR) is non empty set

g is set

gR is () set

(gR) is set

(gR) is set

(gR) is set

(gR) \/ (gR) is set

g is () ()

the of g is set

the of g is set

the of g \/ the of g is set

gR is () set

(gR) is set

(gR) is set

(gR) is set

(gR) \/ (gR) is set

gR is set

{ (b

sup { (b

gRL is set

(gRL) is epsilon-transitive epsilon-connected ordinal set

On { (b

gLR is epsilon-transitive epsilon-connected ordinal set

succ (sup { (b

(gLR) is non empty set

((succ (sup { (b

g is epsilon-transitive epsilon-connected ordinal set

(g) is non empty set

gR is () set

(gR) is epsilon-transitive epsilon-connected ordinal set

gR is () set

(gR) is epsilon-transitive epsilon-connected ordinal set

gRL is epsilon-transitive epsilon-connected ordinal set

(gRL) is non empty set

g is () set

g is () set

gR is epsilon-transitive epsilon-connected ordinal set

(gR) is non empty set

g is () set

(g) is epsilon-transitive epsilon-connected ordinal set

(g) is set

(g) is set

(g) is set

(g) \/ (g) is set

gR is () set

(gR) is epsilon-transitive epsilon-connected ordinal set

g is () set

(g) is set

(g) is set

(g) is set

(g) \/ (g) is set

g is () set

<*g*> is Relation-like K104() -defined Function-like constant non empty V25() V39() 1 -element FinSequence-like FinSubsequence-like set

[1,g] is set

{1,g} is non empty set

{{1,g},{1}} is non empty set

{[1,g]} is Relation-like Function-like constant non empty V25() 1 -element set

gR is set

dom <*g*> is non empty V25() 1 -element set

<*g*> . gR is set

dom <*g*> is non empty V25() 1 -element Element of K53(K104())

<*()*> is Relation-like K104() -defined ({}) -valued Function-like constant non empty V25() V39() 1 -element FinSequence-like FinSubsequence-like () FinSequence of ({})

[1,()] is set

{1,()} is non empty set

{{1,()},{1}} is non empty set

{[1,()]} is Relation-like Function-like constant non empty V25() 1 -element set

g is Relation-like K104() -defined Function-like non empty V39() FinSequence-like FinSubsequence-like set

dom g is non empty Element of K53(K104())

gR is Element of dom g

gR is Element of dom g

g is Relation-like Function-like non empty () set

dom g is non empty set

gR is Element of dom g

g . gR is set

g is Relation-like K104() -defined Function-like V39() FinSequence-like FinSubsequence-like set

dom g is Element of K53(K104())

gR is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative V39() cardinal set

Seg gR is V39() gR -element Element of K53(K104())

{ b

gR is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative V39() cardinal set

gR - 1 is complex V32() ext-real set

g is () set

<*g*> is Relation-like K104() -defined Function-like constant non empty V25() V39() 1 -element FinSequence-like FinSubsequence-like () set

[1,g] is set

{1,g} is non empty set

{{1,g},{1}} is non empty set

{[1,g]} is Relation-like Function-like constant non empty V25() 1 -element set

dom <*g*> is non empty V25() 1 -element Element of K53(K104())

gR is epsilon-transitive epsilon-connected ordinal natural non empty complex V32() ext-real positive non negative V39() cardinal Element of dom <*g*>

gR - 1 is complex V32() ext-real set

<*g*> . (gR - 1) is set

<*g*> . gR is () set

((<*g*> . gR)) is set

((<*g*> . gR)) is set

((<*g*> . gR)) is set

((<*g*> . gR)) \/ ((<*g*> . gR)) is set

the () set is () set

<* the () set *> is Relation-like K104() -defined Function-like constant non empty V25() V39() 1 -element FinSequence-like FinSubsequence-like () () set

[1, the () set ] is set

{1, the () set } is non empty set

{{1, the () set },{1}} is non empty set

{[1, the () set ]} is Relation-like Function-like constant non empty V25() 1 -element set

g is Relation-like K104() -defined Function-like non empty V39() FinSequence-like FinSubsequence-like () () set

dom g is non empty Element of K53(K104())

gR is epsilon-transitive epsilon-connected ordinal natural non empty complex V32() ext-real positive non negative V39() cardinal Element of dom g

gR is epsilon-transitive epsilon-connected ordinal natural non empty complex V32() ext-real positive non negative V39() cardinal Element of dom g

g . gR is () set

((g . gR)) is epsilon-transitive epsilon-connected ordinal set

g . gR is () set

((g . gR)) is epsilon-transitive epsilon-connected ordinal set

gRL is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative V39() cardinal set

Seg gRL is V39() gRL -element Element of K53(K104())

{ b

gR - 1 is complex V32() ext-real set

g . (gR - 1) is set

((g . (gR - 1))) is epsilon-transitive epsilon-connected ordinal set

gLR is epsilon-transitive epsilon-connected ordinal natural non empty complex V32() ext-real positive non negative V39() cardinal Element of dom g

g . gLR is () set

((g . gR)) is set

((g . gR)) is set

((g . gR)) is set

((g . gR)) \/ ((g . gR)) is set

gLR is epsilon-transitive epsilon-connected ordinal natural non empty complex V32() ext-real positive non negative V39() cardinal set

gR - gLR is complex V32() ext-real set

g . (gR - gLR) is set

((g . (gR - gLR))) is epsilon-transitive epsilon-connected ordinal set

gLR + 1 is epsilon-transitive epsilon-connected ordinal natural non empty complex V32() ext-real positive non negative V39() cardinal set

gR - (gLR + 1) is complex V32() ext-real set

g . (gR - (gLR + 1)) is set

((g . (gR - (gLR + 1)))) is epsilon-transitive epsilon-connected ordinal set

g1 is epsilon-transitive epsilon-connected ordinal natural non empty complex V32() ext-real positive non negative V39() cardinal Element of dom g

g1 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty complex V32() ext-real positive non negative V39() cardinal set

gR is epsilon-transitive epsilon-connected ordinal natural non empty complex V32() ext-real positive non negative V39() cardinal Element of dom g

gR - 1 is complex V32() ext-real set

g . g1 is () set

g . gR is () set

((g . gR)) is set

((g . gR)) is set

((g . gR)) is set

((g . gR)) \/ ((g . gR)) is set

((g . g1)) is epsilon-transitive epsilon-connected ordinal set

((g . gR)) is epsilon-transitive epsilon-connected ordinal set

gR - gR is complex V32() ext-real set

gLR is epsilon-transitive epsilon-connected ordinal natural non empty complex V32() ext-real positive non negative V39() cardinal set

gR - gLR is complex V32() ext-real set

g is Relation-like K104() -defined Function-like non empty V39() FinSequence-like FinSubsequence-like () () set

dom g is non empty Element of K53(K104())

gR is epsilon-transitive epsilon-connected ordinal natural non empty complex V32() ext-real positive non negative V39() cardinal Element of dom g

gR is epsilon-transitive epsilon-connected ordinal natural non empty complex V32() ext-real positive non negative V39() cardinal Element of dom g

g . gR is () set

((g . gR)) is epsilon-transitive epsilon-connected ordinal set

g . gR is () set

((g . gR)) is epsilon-transitive epsilon-connected ordinal set

g is epsilon-transitive epsilon-connected ordinal set

(g) is non empty set

gR is Relation-like K104() -defined Function-like non empty V39() FinSequence-like FinSubsequence-like () () set

len gR is epsilon-transitive epsilon-connected ordinal natural non empty complex V32() ext-real positive non negative V39() cardinal Element of K104()

gR . (len gR) is set

gR . 1 is set

dom gR is non empty Element of K53(K104())

gR is epsilon-transitive epsilon-connected ordinal natural non empty complex V32() ext-real positive non negative V39() cardinal Element of dom gR

gRL is epsilon-transitive epsilon-connected ordinal natural non empty complex V32() ext-real positive non negative V39() cardinal Element of dom gR

gR . gR is () set

((gR . gR)) is epsilon-transitive epsilon-connected ordinal set

gR . gRL is () set

((gR . gRL)) is epsilon-transitive epsilon-connected ordinal set

g is () set

<*g*> is Relation-like K104() -defined Function-like constant non empty V25() V39() 1 -element FinSequence-like FinSubsequence-like () () set

[1,g] is set

{1,g} is non empty set

{{1,g},{1}} is non empty set

{[1,g]} is Relation-like Function-like constant non empty V25() 1 -element set

gR is Relation-like K104() -defined Function-like constant non empty V25() V39() 1 -element FinSequence-like FinSubsequence-like () () set

gR . 1 is set

len gR is epsilon-transitive epsilon-connected ordinal natural non empty complex V32() ext-real positive non negative V39() cardinal Element of K104()

gR . (len gR) is set

g is () set

gR is epsilon-transitive epsilon-connected ordinal set

(gR) is non empty set

{ b

( b

gR is set

gRL is set

gLR is () Element of (gR)

g1 is Relation-like K104() -defined Function-like non empty V39() FinSequence-like FinSubsequence-like () () set

g1 . 1 is set

len g1 is epsilon-transitive epsilon-connected ordinal natural non empty complex V32() ext-real positive non negative V39() cardinal Element of K104()

g1 . (len g1) is set

gLR is Relation-like K104() -defined Function-like non empty V39() FinSequence-like FinSubsequence-like () () set

gLR . 1 is set

len gLR is epsilon-transitive epsilon-connected ordinal natural non empty complex V32() ext-real positive non negative V39() cardinal Element of K104()

gLR . (len gLR) is set

gLR is Relation-like K104() -defined Function-like non empty V39() FinSequence-like FinSubsequence-like () () set

gLR . 1 is set

len gLR is epsilon-transitive epsilon-connected ordinal natural non empty complex V32() ext-real positive non negative V39() cardinal Element of K104()

gLR . (len gLR) is set

gR is set

gR is set

gRL is set

gLR is Relation-like K104() -defined Function-like non empty V39() FinSequence-like FinSubsequence-like () () set

gLR . 1 is set

len gLR is epsilon-transitive epsilon-connected ordinal natural non empty complex V32() ext-real positive non negative V39() cardinal Element of K104()

gLR . (len gLR) is set

gLR is Relation-like K104() -defined Function-like non empty V39() FinSequence-like FinSubsequence-like () () set

gLR . 1 is set

len gLR is epsilon-transitive epsilon-connected ordinal natural non empty complex V32() ext-real positive non negative V39() cardinal Element of K104()

gLR . (len gLR) is set

g is () set

(g) is set

gR is Relation-like K104() -defined Function-like non empty V39() FinSequence-like FinSubsequence-like () () set

gR . 1 is set

len gR is epsilon-transitive epsilon-connected ordinal natural non empty complex V32() ext-real positive non negative V39() cardinal Element of K104()

gR . (len gR) is set

g is () set

(g) is non empty set

{g} is non empty V25() 1 -element set

(g) \ {g} is Element of K53((g))

K53((g)) is non empty set

g is () set

(g) is non empty set

gR is Relation-like K104() -defined Function-like non empty V39() FinSequence-like FinSubsequence-like () () set

gR . 1 is set

len gR is epsilon-transitive epsilon-connected ordinal natural non empty complex V32() ext-real positive non negative V39() cardinal Element of K104()

gR . (len gR) is set

g is epsilon-transitive epsilon-connected ordinal set

(g) is non empty set

gR is () Element of (g)

(gR) is non empty set

K53((g)) is non empty set

gR is set

gRL is Relation-like K104() -defined Function-like non empty V39() FinSequence-like FinSubsequence-like () () set

gRL . 1 is set

len gRL is epsilon-transitive epsilon-connected ordinal natural non empty complex V32() ext-real positive non negative V39() cardinal Element of K104()

gRL . (len gRL) is set

g is () set

(g) is non empty set

gR is Element of (g)

gR is epsilon-transitive epsilon-connected ordinal set

(gR) is non empty set

gRL is Relation-like K104() -defined Function-like non empty V39() FinSequence-like FinSubsequence-like () () set

gRL . 1 is set

len gRL is epsilon-transitive epsilon-connected ordinal natural non empty complex V32() ext-real positive non negative V39() cardinal Element of K104()

gRL . (len gRL) is set

g is Relation-like K104() -defined Function-like non empty V39() FinSequence-like FinSubsequence-like () () set

gR is epsilon-transitive epsilon-connected ordinal natural non empty complex V32() ext-real positive non negative V39() cardinal set

g | gR is Relation-like K104() -defined Function-like V39() FinSequence-like FinSubsequence-like set

Seg gR is non empty V39() gR -element Element of K53(K104())

{ b

g | (Seg gR) is Relation-like K104() -defined Seg gR -defined K104() -defined Function-like FinSubsequence-like set

len (g | gR) is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative V39() cardinal Element of K104()

gRL is set

dom (g | gR) is set

(g | gR) . gRL is set

dom (g | gR) is Element of K53(K104())

dom g is non empty Element of K53(K104())

g . gRL is set

len g is epsilon-transitive epsilon-connected ordinal natural non empty complex V32() ext-real positive non negative V39() cardinal Element of K104()

min (gR,(len g)) is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative V39() cardinal set

gRL is Relation-like K104() -defined Function-like non empty V39() FinSequence-like FinSubsequence-like () set

dom gRL is non empty Element of K53(K104())

gLR is epsilon-transitive epsilon-connected ordinal natural non empty complex V32() ext-real positive non negative V39() cardinal Element of dom gRL

gLR - 1 is complex V32() ext-real set

gRL . (gLR - 1) is set

gRL . gLR is () set

((gRL . gLR)) is set

((gRL . gLR)) is set

((gRL . gLR)) is set

((gRL . gLR)) \/ ((gRL . gLR)) is set

dom g is non empty Element of K53(K104())

g . gLR is set

g . (gLR - 1) is set

gR is Relation-like K104() -defined Function-like non empty V39() FinSequence-like FinSubsequence-like () () set

gR . 1 is set

g is Relation-like K104() -defined Function-like non empty V39() FinSequence-like FinSubsequence-like () () set

len g is epsilon-transitive epsilon-connected ordinal natural non empty complex V32() ext-real positive non negative V39() cardinal Element of K104()

g . (len g) is set

g ^ gR is Relation-like K104() -defined Function-like non empty V39() FinSequence-like FinSubsequence-like set

gRL is () set

(gRL) is set

(gRL) is set

(gRL) is set

(gRL) \/ (gRL) is set

gRL is set

dom (g ^ gR) is non empty set

(g ^ gR) . gRL is set

dom (g ^ gR) is non empty Element of K53(K104())

rng (g ^ gR) is non empty set

rng g is non empty set

rng gR is non empty set

(rng g) \/ (rng gR) is non empty set

dom g is non empty Element of K53(K104())

g1 is set

g . g1 is set

dom gR is non empty Element of K53(K104())

g1 is set

gR . g1 is set

gRL is Relation-like K104() -defined Function-like non empty V39() FinSequence-like FinSubsequence-like () set

dom gRL is non empty Element of K53(K104())

gLR is epsilon-transitive epsilon-connected ordinal natural non empty complex V32() ext-real positive non negative V39() cardinal Element of dom gRL

gLR - 1 is complex V32() ext-real set

gRL . (gLR - 1) is set

gRL . gLR is () set

((gRL . gLR)) is set

((gRL . gLR)) is set

((gRL . gLR)) is set

((gRL . gLR)) \/ ((gRL . gLR)) is set

(len g) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty complex V32() ext-real positive non negative V39() cardinal set

dom g is non empty Element of K53(K104())

g1 is epsilon-transitive epsilon-connected ordinal natural non empty complex V32() ext-real positive non negative V39() cardinal Element of dom g

g1 - 1 is complex V32() ext-real set

g . g1 is () set

gRL . g1 is set

g . (g1 - 1) is set

gRL . (g1 - 1) is set

(len g) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty complex V32() ext-real positive non negative V39() cardinal set

dom g is non empty Element of K53(K104())

dom gR is non empty Element of K53(K104())

g1 is () set

(g1) is set

(g1) is set

(g1) is set

(g1) \/ (g1) is set

(len g) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty complex V32() ext-real positive non negative V39() cardinal set

len gRL is epsilon-transitive epsilon-connected ordinal natural non empty complex V32() ext-real positive non negative V39() cardinal Element of K104()

len gR is epsilon-transitive epsilon-connected ordinal natural non empty complex V32() ext-real positive non negative V39() cardinal Element of K104()

(len g) + (len gR) is epsilon-transitive epsilon-connected ordinal natural non empty complex V32() ext-real positive non negative V39() cardinal set

gLR - (len g) is complex V32() ext-real set

dom gR is non empty Element of K53(K104())

g1 is epsilon-transitive epsilon-connected ordinal natural non empty complex V32() ext-real positive non negative V39() cardinal Element of dom gR

g1 - 1 is complex V32() ext-real set

(len g) + g1 is epsilon-transitive epsilon-connected ordinal natural non empty complex V32() ext-real positive non negative V39() cardinal set

gRL . ((len g) + g1) is set

gR . g1 is () set

(len g) + (g1 - 1) is complex V32() ext-real set

gRL . ((len g) + (g1 - 1)) is set

gR . (g1 - 1) is set

(len g) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty complex V32() ext-real positive non negative V39() cardinal set

g is set

gR is () set

(gR) is non empty set

(gR) is set

(gR) is set

(gR) is set

(gR) \/ (gR) is set

gR is Relation-like K104() -defined Function-like non empty V39() FinSequence-like FinSubsequence-like () () set

gR . 1 is set

len gR is epsilon-transitive epsilon-connected ordinal natural non empty complex V32() ext-real positive non negative V39() cardinal Element of K104()

gR . (len gR) is set

dom gR is non empty Element of K53(K104())

gRL is epsilon-transitive epsilon-connected ordinal natural non empty complex V32() ext-real positive non negative V39() cardinal Element of dom gR

gRL - 1 is complex V32() ext-real set

gLR is epsilon-transitive epsilon-connected ordinal natural non empty complex V32() ext-real positive non negative V39() cardinal Element of dom gR

gR . gLR is () set

g1 is () set

gR | gLR is Relation-like K104() -defined Function-like V39() FinSequence-like FinSubsequence-like set

Seg gLR is non empty V39() gLR -element Element of K53(K104())

{ b

gR | (Seg gLR) is Relation-like K104() -defined Seg gLR -defined K104() -defined Function-like FinSubsequence-like set

gR is Relation-like K104() -defined Function-like non empty V39() FinSequence-like FinSubsequence-like () () set

dom gR is non empty Element of K53(K104())

len gR is epsilon-transitive epsilon-connected ordinal natural non empty complex V32() ext-real positive non negative V39() cardinal Element of K104()

gR . 1 is set

gR . (len gR) is set

gR . (len gR) is set

(g1) is non empty set

gR is () set

(gR) is non empty set

gR is () set

(gR) is non empty set

gRL is Relation-like K104() -defined Function-like non empty V39() FinSequence-like FinSubsequence-like () () set

gRL . 1 is set

len gRL is epsilon-transitive epsilon-connected ordinal natural non empty complex V32() ext-real positive non negative V39() cardinal Element of K104()

gRL . (len gRL) is set

<*gR*> is Relation-like K104() -defined Function-like constant non empty V25() V39() 1 -element FinSequence-like FinSubsequence-like () () set

[1,gR] is set

{1,gR} is non empty set

{{1,gR},{1}} is non empty set

{[1,gR]} is Relation-like Function-like constant non empty V25() 1 -element set

<*gR*> . 1 is set

gRL ^ <*gR*> is Relation-like K104() -defined Function-like non empty V39() FinSequence-like FinSubsequence-like set

g1 is () set

(g1) is set

(g1) is set

(g1) is set

(g1) \/ (g1) is set

dom gRL is non empty Element of K53(K104())

gLR is Relation-like K104() -defined Function-like non empty V39() FinSequence-like FinSubsequence-like () () set

len gLR is epsilon-transitive epsilon-connected ordinal natural non empty complex V32() ext-real positive non negative V39() cardinal Element of K104()

(len gRL) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty complex V32() ext-real positive non negative V39() cardinal set

gLR . 1 is set

gLR . (len gLR) is set

gR is () set

(gR) is non empty set

g is () set

(g) is epsilon-transitive epsilon-connected ordinal set

gR is () set

(gR) is non empty set

(gR) is epsilon-transitive epsilon-connected ordinal set

gR is Relation-like K104() -defined Function-like non empty V39() FinSequence-like FinSubsequence-like () () set

gR . 1 is set

len gR is epsilon-transitive epsilon-connected ordinal natural non empty complex V32() ext-real positive non negative V39() cardinal Element of K104()

gR . (len gR) is set

dom gR is non empty Element of K53(K104())

gLR is epsilon-transitive epsilon-connected ordinal natural non empty complex V32() ext-real positive non negative V39() cardinal Element of dom gR

gRL is epsilon-transitive epsilon-connected ordinal natural non empty complex V32() ext-real positive non negative V39() cardinal Element of dom gR

gR . gRL is () set

((gR . gRL)) is epsilon-transitive epsilon-connected ordinal set

gR . gLR is () set

((gR . gLR)) is epsilon-transitive epsilon-connected ordinal set

g is () set

(g) is epsilon-transitive epsilon-connected ordinal set

gR is () set

(gR) is non empty set

(gR) is epsilon-transitive epsilon-connected ordinal set

g is () set

(g) is non empty set

gR is set

gR is set

gRL is Relation-like K104() -defined Function-like non empty V39() FinSequence-like FinSubsequence-like () () set

gRL . 1 is set

len gRL is epsilon-transitive epsilon-connected ordinal natural non empty complex V32() ext-real positive non negative V39() cardinal Element of K104()

gRL . (len gRL) is set

(len gRL) - 1 is complex V32() ext-real set

gLR is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative V39() cardinal set

gLR + 1 is epsilon-transitive epsilon-connected ordinal natural non empty complex V32() ext-real positive non negative V39() cardinal set

gRL . (gLR + 1) is set

g1 is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative V39() cardinal set

g1 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty complex V32() ext-real positive non negative V39() cardinal set

gRL . (g1 + 1) is set

g1 - 1 is complex V32() ext-real set

gR is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative V39() cardinal set

gR + 1 is epsilon-transitive epsilon-connected ordinal natural non empty complex V32() ext-real positive non negative V39() cardinal set

gRL . (gR + 1) is set

dom gRL is non empty Element of K53(K104())

gRL is epsilon-transitive epsilon-connected ordinal natural non empty complex V32() ext-real positive non negative V39() cardinal Element of dom gRL

gRL - 1 is complex V32() ext-real set

gRL . (gRL - 1) is set

gRL . gRL is () set

((gRL . gRL)) is set

((gRL . gRL)) is set

((gRL . gRL)) is set

((gRL . gRL)) \/ ((gRL . gRL)) is set

{} + 1 is epsilon-transitive epsilon-connected ordinal natural non empty complex V32() ext-real positive non negative V39() cardinal set

gRL . ({} + 1) is set

g is () set

(g) is non empty set

gR is () set

(gR) is non empty set

gR is Relation-like K104() -defined Function-like non empty V39() FinSequence-like FinSubsequence-like () () set

gR . 1 is set

len gR is epsilon-transitive epsilon-connected ordinal natural non empty complex V32() ext-real positive non negative V39() cardinal Element of K104()

gR . (len gR) is set

gRL is set

gLR is Relation-like K104() -defined Function-like non empty V39() FinSequence-like FinSubsequence-like () () set

gLR . 1 is set

len gLR is epsilon-transitive epsilon-connected ordinal natural non empty complex V32() ext-real positive non negative V39() cardinal Element of K104()

gLR . (len gLR) is set

(len gLR) - 1 is complex V32() ext-real set

g1 is epsilon-transitive epsilon-connected ordinal natural non empty complex V32() ext-real positive non negative V39() cardinal set

gLR | g1 is Relation-like K104() -defined Function-like V39() FinSequence-like FinSubsequence-like set

Seg g1 is non empty V39() g1 -element Element of K53(K104())

{ b

gLR | (Seg g1) is Relation-like K104() -defined Seg g1 -defined K104() -defined Function-like FinSubsequence-like set

dom gLR is non empty Element of K53(K104())

gLR . g1 is set

(g) is set

(g) is set

(g) is set

(g) \/ (g) is set

gR is Relation-like K104() -defined Function-like non empty V39() FinSequence-like FinSubsequence-like () () set

gR . g1 is set

len gR is epsilon-transitive epsilon-connected ordinal natural non empty complex V32() ext-real positive non negative V39() cardinal Element of K104()

gR ^ gR is Relation-like K104() -defined Function-like non empty V39() FinSequence-like FinSubsequence-like set

dom gR is non empty Element of K53(K104())

dom gR is non empty Element of K53(K104())

gR . 1 is set

gRL is Relation-like K104() -defined Function-like non empty V39() FinSequence-like FinSubsequence-like () () set

len gRL is epsilon-transitive epsilon-connected ordinal natural non empty complex V32() ext-real positive non negative V39() cardinal Element of K104()

(len gR) + (len gR) is epsilon-transitive epsilon-connected ordinal natural non empty complex V32() ext-real positive non negative V39() cardinal set

gRL . 1 is set

gRL . (len gRL) is set

g is () set

(g) is Element of K53((g))

(g) is non empty set

K53((g)) is non empty set

{g} is non empty V25() 1 -element set

(g) \ {g} is Element of K53((g))

gR is () set

(gR) is non empty set

(gR) is Element of K53((gR))

K53((gR)) is non empty set

{gR} is non empty V25() 1 -element set

(gR) \ {gR} is Element of K53((gR))

gR is set

(g) is epsilon-transitive epsilon-connected ordinal set

(gR) is epsilon-transitive epsilon-connected ordinal set

gRL is () set

(gRL) is epsilon-transitive epsilon-connected ordinal set

(g) is epsilon-transitive epsilon-connected ordinal set

(gR) is epsilon-transitive epsilon-connected ordinal set

g is () set

(g) is set

(g) is set

(g) is set

(g) \/ (g) is set

(g) is Element of K53((g))

(g) is non empty set

K53((g)) is non empty set

{g} is non empty V25() 1 -element set

(g) \ {g} is Element of K53((g))

gR is set

gR is () set

(gR) is non empty set

g is () set

(g) is set

(g) is set

(g) is set

(g) \/ (g) is set

(g) is non empty set

(g) is Element of K53((g))

K53((g)) is non empty set

{g} is non empty V25() 1 -element set

(g) \ {g} is Element of K53((g))

g is () set

(g) is non empty set

gR is () set

(gR) is Element of K53((gR))

(gR) is non empty set

K53((gR)) is non empty set

{gR} is non empty V25() 1 -element set

(gR) \ {gR} is Element of K53((gR))

(g) is epsilon-transitive epsilon-connected ordinal set

(gR) is epsilon-transitive epsilon-connected ordinal set

g is () set

(g) is non empty set

gR is () set

(gR) is set

(gR) is set

(gR) is set

(gR) \/ (gR) is set

(gR) is Element of K53((gR))

(gR) is non empty set

K53((gR)) is non empty set

{gR} is non empty V25() 1 -element set

(gR) \ {gR} is Element of K53((gR))

({},()) is non empty Element of K53(({}))

K53(({})) is non empty set

g is () set

(g) is non empty set

gR is () set

(gR) is non empty set

(gR) is set

(gR) is set

(gR) is set

(gR) \/ (gR) is set

gR is set

gRL is () set

(gRL) is non empty set

g is () set

(g) is epsilon-transitive epsilon-connected ordinal set

(g) is Element of K53((g))

(g) is non empty set

K53((g)) is non empty set

{g} is non empty V25() 1 -element set

(g) \ {g} is Element of K53((g))

gR is () set

(gR) is epsilon-transitive epsilon-connected ordinal set

gR is () set

g is () set

(g) is non empty set

gR is Relation-like Function-like set

dom gR is set

gR is Relation-like Function-like set

dom gR is set

gRL is set

gR . gRL is set

gR . gRL is set

gRL is () set

gR . gRL is set

gR . gRL is set

(gRL) is Element of K53((gRL))

(gRL) is non empty set

K53((gRL)) is non empty set

{gRL} is non empty V25() 1 -element set

(gRL) \ {gRL} is Element of K53((gRL))

gR | (gRL) is Relation-like Function-like set

gR | (gRL) is Relation-like Function-like set

dom (gR | (gRL)) is set

dom (gR | (gRL)) is set

gR is set

gR . gR is set

gR . gR is set

(gR | (gRL)) . gR is set

(gR | (gRL)) . gR is set

F

F

g is set

gRL is () set

gR is set

gLR is Relation-like Function-like set

dom gLR is set

(gRL) is non empty set

g1 is () set

gR is set

gR is Relation-like Function-like set

dom gR is set

(g1) is non empty set

g is () set

(g) is non empty set

gR is Relation-like Function-like set

dom gR is set

gR | (g) is Relation-like Function-like set

dom (gR | (g)) is set

gR is () set

(gR | (g)) . gR is set

(gR) is Element of K53((gR))

(gR) is non empty set

K53((gR)) is non empty set

{gR} is non empty V25() 1 -element set

(gR) \ {gR} is Element of K53((gR))

(gR | (g)) | (gR) is Relation-like Function-like set

F

gR . gR is set

gR | (gR) is Relation-like Function-like set

F

g is () set

(g) is set

(g) is set

(g) is set

(g) \/ (g) is set

(g) is non empty set

gR is set

gR is set

gRL is set

gLR is () set

g1 is Relation-like Function-like set

dom g1 is set

(gLR) is non empty set

gR is Relation-like Function-like set

dom gR is set

gLR is set

g1 is () set

gR is Relation-like Function-like set

dom gR is set

(g1) is non empty set

gLR is () set

(gLR) is non empty set

gRL is Relation-like Function-like set

dom gRL is set

g1 is set

gR is () set

gRL is Relation-like Function-like set

dom gRL is set

(gR) is non empty set

g1 is () set

(g1) is non empty set

gR is set

(dom gR) /\ (dom gRL) is set

gR . gR is set

gRL . gR is set

gRL is () set

(gRL) is non empty set

gR | (gRL) is Relation-like Function-like set

dom (gR | (gRL)) is set

gRL | (gRL) is Relation-like Function-like set

dom (gRL | (gRL)) is set

s1 is () set

(gR | (gRL)) . s1 is set

(s1) is Element of K53((s1))

(s1) is non empty set

K53((s1)) is non empty set

{s1} is non empty V25() 1 -element set

(s1) \ {s1} is Element of K53((s1))

(gR | (gRL)) | (s1) is Relation-like Function-like set

F

gL is () set

(gRL | (gRL)) . gL is set

(gL) is Element of K53((gL))

(gL) is non empty set

K53((gL)) is non empty set

{gL} is non empty V25() 1 -element set

(gL) \ {gL} is Element of K53((gL))

(gRL | (gRL)) | (gL) is Relation-like Function-like set

F

gR . gRL is set

(gR | (gRL)) . gRL is set

gRL . gRL is set

(gRL | (gRL)) . gRL is set

gR is functional compatible set

union gR is Relation-like Function-like set

gRL is Relation-like Function-like set

dom gRL is set

(g) is Element of K53((g))

K53((g)) is non empty set

{g} is non empty V25() 1 -element set

(g) \ {g} is Element of K53((g))

gLR is set

g1 is () set

(g1) is non empty set

gR is Relation-like Function-like set

dom gR is set

gLR is set

gRL . gLR is set

[gLR,(gRL . gLR)] is set

{gLR,(gRL . gLR)} is non empty set

{gLR} is non empty V25() 1 -element set

{{gLR,(gRL . gLR)},{gLR}} is non empty set

g1 is set

g1 is Relation-like Function-like set

dom g1 is set

gR is set

gRL is () set

s0 is Relation-like Function-like set

dom s0 is set

(gRL) is non empty set

gR is () set

(gR) is non empty set

gLR is () set

gRL . gLR is set

(gLR) is Element of K53((gLR))

(gLR) is non empty set

K53((gLR)) is non empty set

{gLR} is non empty V25() 1 -element set

(gLR) \ {gLR} is Element of K53((gLR))

gRL | (gLR) is Relation-like Function-like set

F

[gLR,(gRL . gLR)] is set

{gLR,(gRL . gLR)} is non empty set

{{gLR,(gRL . gLR)},{gLR}} is non empty set

g1 is set

g1 is Relation-like Function-like set

dom g1 is set

gR is set

gRL is () set

s0 is Relation-like Function-like set

dom s0 is set

(gRL) is non empty set

gR is () set

(gR) is non empty set

g1 | (gLR) is Relation-like Function-like set

dom (g1 | (gLR)) is set

dom (gRL | (gLR)) is set

gRL is set

g1 . gRL is set

gRL . gRL is set

(g1 | (gLR)) . gRL is set

(gRL | (gLR)) . gRL is set

g1 . gLR is set

F

gRL | (g) is Relation-like Function-like set

F

[g,F

{g,F

{{g,F

{[g,F

dom {[g,F

{[g,F

gR is Relation-like Function-like set

g1 is Relation-like Function-like set

dom g1 is set

(dom gRL) \/ (dom {[g,F

(dom gRL) \/ {g} is non empty set

gR is set

{g} /\ (g) is set

({g} /\ (g)) \/ ((g) \ {g}) is set

gR is set

gR is () set

g1 . gR is set

(gR) is Element of K53((gR))

(gR) is non empty set

K53((gR)) is non empty set

{gR} is non empty V25() 1 -element set

(gR) \ {gR} is Element of K53((gR))

g1 | (gR) is Relation-like Function-like set

F

gRL | (gR) is Relation-like Function-like set

dom (gRL | (gR)) is set

dom (g1 | (gR)) is set

gRL . gR is set

gR is () set

gRL is Relation-like Function-like set

dom gRL is set

(gR) is non empty set

(g) \/ {g} is non empty set

gLR is () set

gRL . gLR is set

(gLR) is Element of K53((gLR))

(gLR) is non empty set

K53((gLR)) is non empty set

{gLR} is non empty V25() 1 -element set

(gLR) \ {gLR} is Element of K53((gLR))

gRL | (gLR) is Relation-like Function-like set

F

g is () set

(g) is non empty set

g is () set

(g) is set

(g) is Element of K53((g))

(g) is non empty set

K53((g)) is non empty set

{g} is non empty V25() 1 -element set

(g) \ {g} is Element of K53((g))

(g) is set

gR is Relation-like Function-like set

gR | (g) is Relation-like Function-like set

{ ((gR | (g)) . b

{ (gR . b

{ ((gR | (g)) . b

{ (gR . b

gR is () set

(gR | (g)) . gR is set

gR . gR is set

(g) is set

(g) \/ (g) is set

gR is set

gRL is Element of (g)

(gR | (g)) . gRL is set

gR . gRL is set

gR is set

gRL is Element of (g)

gR . gRL is set

(gR | (g)) . gRL is set

gR is set

gRL is Element of (g)

(gR | (g)) . gRL is set

gR . gRL is set

gR is set

gRL is Element of (g)

gR . gRL is set

(gR | (g)) . gRL is set

g is () set

(g) is non empty set

{ (a

{ (a

( { (a

gR is Relation-like Function-like set

dom gR is set

gR . g is set

gR is set

gRL is () set

gR . gRL is set

(gRL) is set

{ (gR . b

(gRL) is set

{ (gR . b

( { (gR . b

(gRL) is Element of K53((gRL))

(gRL) is non empty set

K53((gRL)) is non empty set

{gRL} is non empty V25() 1 -element set

(gRL) \ {gRL} is Element of K53((gRL))

gR | (gRL) is Relation-like Function-like set

{ ((gR | (gRL)) . b

{ ((gR | (gRL)) . b

{ (a

{ (a

( { (a

gR is set

gR is set

gRL is Relation-like Function-like set

dom gRL is set

gRL . g is set

gRL is Relation-like Function-like set

dom gRL is set

gRL . g is set

gLR is Relation-like Function-like set

dom gLR is set

gLR . g is set

gLR is Relation-like Function-like set

dom gLR is set

gLR . g is set

g1 is () set

gRL . g1 is set

(g1) is Element of K53((g1))

(g1) is non empty set

K53((g1)) is non empty set

{g1} is non empty V25() 1 -element set

(g1) \ {g1} is Element of K53((g1))

gRL | (g1) is Relation-like Function-like set

(g1) is set

{ ((gRL | (g1)) . b

(g1) is set

{ ((gRL | (g1)) . b

( { ((gRL | (g1)) . b

{ (gRL . b

{ (gRL . b

g1 is () set

gLR . g1 is set

(g1) is Element of K53((g1))

(g1) is non empty set

K53((g1)) is non empty set

{g1} is non empty V25() 1 -element set

(g1) \ {g1} is Element of K53((g1))

gLR | (g1) is Relation-like Function-like set

(g1) is set

{ ((gLR | (g1)) . b

(g1) is set

{ ((gLR | (g1)) . b

( { ((gLR | (g1)) . b

{ (gLR . b

{ (gLR . b

g is () set

(g) is set

(g) is non empty set

gR is Relation-like Function-like set

dom gR is set

gR . g is set

gR is () set

(gR) is set

(gR) is set

(gR) is set

(gR) \/ (gR) is set

gR . gR is set

{ (gR . b

{ (gR . b

( { (gR . b

g1 is set

{ (gR . b

gR is Element of (gR)

gR . gR is set

gRL is () set

gR . gRL is set

gR is Element of (gR)

gR . gR is set

gRL is () set

gR . gRL is set

gR is () set

gR . gR is set

gR is () set

gR . gR is set

(gR) is non empty set

g is () set

(g) is non empty set

gR is Relation-like Function-like set

dom gR is set

gR is () set

gR . gR is set

(gR) is () set

(gR) is non empty set

gR | (gR) is Relation-like Function-like set

dom (gR | (gR)) is set

gLR is () set

(gLR) is set

{ (gR . b

{ ((gR | (gR)) . b

(gLR) is set

{ (gR . b

{ ((gR | (gR)) . b

gR . gLR is set

( { (gR . b

s1 is () set

(gR | (gR)) . s1 is set

gR . s1 is set

(gLR) is set

(gLR) \/ (gLR) is set

(gLR) is non empty set

s1 is set

gL is Element of (gLR)

gR . gL is set

(gR | (gR)) . gL is set

s1 is set

gL is Element of (gLR)

(gR | (gR)) . gL is set

gR . gL is set

s1 is set

gL is Element of (gLR)

gR . gL is set

(gR | (gR)) . gL is set

s1 is set

gL is Element of (gLR)

(gR | (gR)) . gL is set

gR . gL is set

(gR | (gR)) . gLR is set

( { ((gR | (gR)) . b

(gR | (gR)) . gR is set

g is () set

(g) is () set

((g)) is set

(g) is set

((g)) is set

(g) is set

(g) is non empty set

gR is Relation-like Function-like set

dom gR is set

gR . g is set

gR is () set

gR . gR is set

(gR) is () set

(g) is set

(g) \/ (g) is set

{ (gR . b

{ (gR . b

( { (gR . b

gLR is set

g1 is Element of (g)

gR . g1 is set

gR is () set

gRL is () set

(gRL) is () set

g1 is () set

(g1) is () set

g1 is () set

(g1) is () set

gR . g1 is set

gLR is set

g1 is Element of (g)

gR . g1 is set

gR is () set

gRL is () set

(gRL) is () set

g1 is () set

(g1) is () set

g1 is () set

(g1) is () set

gR . g1 is set

g is () set

(g) is () set

((g)) is () set

gR is () set

(gR) is () set

((gR)) is () set

(gR) is set

(gR) is set

(gR) is set

(gR) \/ (gR) is set

gR is set

(((gR))) is set

((gR)) is set

gRL is () set

(gRL) is () set

gLR is () set

(gLR) is () set

gR is set

gRL is () set

(gRL) is () set

((gRL)) is () set

gR is set

(((gR))) is set

((gR)) is set

gRL is () set

(gRL) is () set

gLR is () set

(gLR) is () set

gR is set

gRL is () set

(gRL) is () set

((gRL)) is () set

g is () set

(g) is () set

gR is () set

(gR) is () set

((gR)) is set

(gR) is set

(gR) is set

((gR)) is set

((gR)) is () set

((g)) is () set

g is () set

g is () set

g is () set

g is () set

g is () set

g is () set

g is () set

g is () set

g is () set

g is () set

(g) is set

gR is set

gR is epsilon-transitive epsilon-connected ordinal set

(gR) is non empty set

gR /\ (gR) is set

gRL is () set

(gRL) is set

gLR is () set

(gLR) is set

g1 is () set

gR is set

gR is () set

(gR) is set

gRL is () set

gLR is () set

g1 is () set

gR is () set

(g1) is set

(gR) is set

gR is epsilon-transitive epsilon-connected ordinal set

(gR) is non empty set

K53((gR)) is non empty set

{ b

union { b

gRL is set

gLR is () set

(gLR) is set

g1 is set

gR is Element of K53((gR))

gRL is () set

(gRL) is set

s0 is () set

gLR is set

g1 is Element of K53((gR))

{g} is non empty V25() 1 -element set

gRL \/ {g} is non empty set

gLR is Element of K53((gR))

g1 is () set

(g1) is set

gR is () set

(gR) is set

gRL is () set

gRL is () set

s0 is set

s0 /\ (gR) is set

s1 is Element of K53((gR))

gL is () set

c

(gL) is set

(c

gLR is () set

g1 is () set

(gLR) is set

(g1) is set

gR is set

g is () set

(g) is set

(g) is () set

gR is () set

(gR) is () set

((g)) is set

((gR)) is set

gR is () set

(gR) is () set

gRL is () set

((gR)) is () set

(((gR))) is set

(gRL) is () set

(gR) is set

gR is () set

(gR) is () set

((g)) is () set

(((g))) is set

((gR)) is set

gR is () set

(gR) is () set

gRL is () set

((gR)) is () set

(((gR))) is set

(gR) is set

g is () set

(g) is set

(g) is set

gR is () set

(gR) is set

(gR) is set

(gR) is set

(gR) \/ (gR) is set

gR is () set

(gR) is set

gRL is () set

(gR) is set

gLR is () set

g1 is () set

gLR is () set

gLR is () set

g1 is () set

gR is () set

gR is () set

(gR) is set

(gR) is set

gRL is () set

gLR is () set

gRL is () set

gLR is () set

gRL is () set

gLR is () set

gR is () set

(gR) is set

gRL is () set

(gR) is set

gLR is () set

g1 is () set

gLR is () set

gLR is () set

g1 is () set

gR is () set

gR is () set

(gR) is set

(gR) is set

gRL is () set

gLR is () set

gRL is () set

gLR is () set

gRL is () set

gLR is () set

gR is () set

gR is () set

g is () set

(g) is set

(g) is set

gR is () set

(gR) is set

gR is () set

gRL is () set

(gR) is set

gR is () set

(gR) is set

gR is () set

gRL is () set

(gR) is set

gR is () set

gR is () set

gR is () set

gR is () set

g is () set

(g) is set

(g) is set

gR is () set

gR is () set

g is () set

(g) is set

(g) is set

gR is () set

gR is () set

gR is () set

gR is () set

gR is () set

g is () set

(g) is set

(g) is set

gR is () set

gR is () set

gR is () set

gR is () set

gR is () set

g is () set

gR is () set

g is () set

g is () () () () Element of ({})

g is () () () () Element of ({})

g is () () () () Element of ({})

g is () () () () Element of ({})

g is () () () () Element of ({})

gR is () () () () Element of ({})

g is () () set

(g) is () set

g is () () set

(g) is () set

((g)) is () set

g is () () () () set

(g) is () () set

((g)) is () () set

(()) is () () () () set

g is () () () () set

(g) is () () set

((g)) is () () set

g is () () () () set

(g) is () set

((g)) is () set