:: 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₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative V39() cardinal Element of K104() : ( 1 <= b₁ & b₁ <= 1 ) } is set
{1} is non empty V25() 1 -element set
Seg 2 is non empty V39() 2 -element Element of K53(K104())
{ b₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative V39() cardinal Element of K104() : ( 1 <= b₁ & b₁ <= 2 ) } is set
{1,2} is non empty set
({},{}) is () ()
() is set
{ (b₁,b₂) where b₁, b₂ is Element of K53((union (rng a₁))) : verum } is set
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₁,b₂) where b₁, b₂ is Element of K53((union (rng ((g | gR) | gR)))) : verum } is set
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₁,b₂) where b₁, b₂ is Element of K53((union (rng (g | gR)))) : verum } is set
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₁,b₂) where b₁, b₂ is Element of K53((union (rng (gR | gR)))) : verum } is set
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₁,b₂) where b₁, b₂ is Element of K53((union (rng s0))) : verum } is set
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₁,b₂) where b₁, b₂ is Element of K53((union (rng s0))) : verum } is set
(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₁,b₂) where b₁, b₂ is Element of K53((union (rng (gR | gR)))) : verum } is set
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₁) where b₁ is Element of the of g \/ the of g : verum } is set
sup { (b₁) where b₁ is Element of the of g \/ the of g : verum } is epsilon-transitive epsilon-connected ordinal set
gRL is set
(gRL) is epsilon-transitive epsilon-connected ordinal set
On { (b₁) where b₁ is Element of the of g \/ the of g : verum } is set
gLR is epsilon-transitive epsilon-connected ordinal set
succ (sup { (b₁) where b₁ is Element of the of g \/ the of g : verum } ) is epsilon-transitive epsilon-connected ordinal non empty set
(gLR) is non empty set
((succ (sup { (b₁) where b₁ is Element of the of g \/ the of g : verum } ))) is non empty 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 () 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₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative V39() cardinal Element of K104() : ( 1 <= b₁ & b₁ <= gR ) } is set
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₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative V39() cardinal Element of K104() : ( 1 <= b₁ & b₁ <= gRL ) } is set
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₁ where b₁ is () Element of (gR) : ex b₂ being Relation-like K104() -defined Function-like non empty V39() FinSequence-like FinSubsequence-like () () set st
( b₂ . 1 = b₁ & b₂ . (len b₂) = g ) } is set
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₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative V39() cardinal Element of K104() : ( 1 <= b₁ & b₁ <= gR ) } is set
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₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative V39() cardinal Element of K104() : ( 1 <= b₁ & b₁ <= gLR ) } is set
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₁ where b₁ is epsilon-transitive epsilon-connected ordinal natural complex V32() ext-real non negative V39() cardinal Element of K104() : ( 1 <= b₁ & b₁ <= g1 ) } is set
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₁(gRL,(gR | (gRL))) is set
F₁(gRL,(gR | (gRL))) is set
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 | (g)) | (gR))) is set
gR . gR is set
gR | (gR) is Relation-like Function-like set
F₁(gR,(gR | (gR))) is set
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₁(s1,((gR | (gRL)) | (s1))) is set
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₁(gL,((gRL | (gRL)) | (gL))) is set
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 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₁(gLR,(g1 | (gLR))) is set
gRL | (g) is Relation-like Function-like set
F₁(g,(gRL | (g))) is set
[g,F₁(g,(gRL | (g)))] is set
{g,F₁(g,(gRL | (g)))} is non empty set
{{g,F₁(g,(gRL | (g)))},{g}} is non empty set
{[g,F₁(g,(gRL | (g)))]} is Relation-like Function-like constant non empty V25() 1 -element set
dom {[g,F₁(g,(gRL | (g)))]} is non empty V25() 1 -element set
{[g,F₁(g,(gRL | (g)))]} \/ gRL is Relation-like non empty set
gR is Relation-like Function-like set
g1 is Relation-like Function-like set
dom g1 is set
(dom gRL) \/ (dom {[g,F₁(g,(gRL | (g)))]}) is non empty set
(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₁(gR,(g1 | (gR))) is set
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₁(gLR,(gRL | (gLR))) is set
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₁) where b₁ is Element of (g) : not (g) = {} } is set
{ (gR . b₁) where b₁ is Element of (g) : not (g) = {} } is set
{ ((gR | (g)) . b₁) where b₁ is Element of (g) : not (g) = {} } is set
{ (gR . b₁) where b₁ is Element of (g) : not (g) = {} } is set
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₂ . b₁) where b₁ is Element of (a₁) : not (a₁) = {} } is set
{ (a₂ . b₁) where b₁ is Element of (a₁) : not (a₁) = {} } is set
( { (a₂ . b₁) where b₁ is Element of (a₁) : not (a₁) = {} } , { (a₂ . b₁) where b₁ is Element of (a₁) : not (a₁) = {} } ) is () ()
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₁) where b₁ is Element of (gRL) : not (gRL) = {} } is set
(gRL) is set
{ (gR . b₁) where b₁ is Element of (gRL) : not (gRL) = {} } is set
( { (gR . b₁) where b₁ is Element of (gRL) : not (gRL) = {} } , { (gR . b₁) where b₁ is Element of (gRL) : not (gRL) = {} } ) is () ()
(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₁) where b₁ is Element of (gRL) : not (gRL) = {} } is set
{ ((gR | (gRL)) . b₁) where b₁ is Element of (gRL) : not (gRL) = {} } is set
{ (a₂ . b₁) where b₁ is Element of (a₁) : not (a₁) = {} } is set
{ (a₂ . b₁) where b₁ is Element of (a₁) : not (a₁) = {} } is set
( { (a₂ . b₁) where b₁ is Element of (a₁) : not (a₁) = {} } , { (a₂ . b₁) where b₁ is Element of (a₁) : not (a₁) = {} } ) is () ()
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₁) where b₁ is Element of (g1) : not (g1) = {} } is set
(g1) is set
{ ((gRL | (g1)) . b₁) where b₁ is Element of (g1) : not (g1) = {} } is set
( { ((gRL | (g1)) . b₁) where b₁ is Element of (g1) : not (g1) = {} } , { ((gRL | (g1)) . b₁) where b₁ is Element of (g1) : not (g1) = {} } ) is () ()
{ (gRL . b₁) where b₁ is Element of (g1) : not (g1) = {} } is set
{ (gRL . b₁) where b₁ is Element of (g1) : not (g1) = {} } is set
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₁) where b₁ is Element of (g1) : not (g1) = {} } is set
(g1) is set
{ ((gLR | (g1)) . b₁) where b₁ is Element of (g1) : not (g1) = {} } is set
( { ((gLR | (g1)) . b₁) where b₁ is Element of (g1) : not (g1) = {} } , { ((gLR | (g1)) . b₁) where b₁ is Element of (g1) : not (g1) = {} } ) is () ()
{ (gLR . b₁) where b₁ is Element of (g1) : not (g1) = {} } is set
{ (gLR . b₁) where b₁ is Element of (g1) : not (g1) = {} } 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) is set
(gR) is set
(gR) is set
(gR) \/ (gR) is set
gR . gR is set
{ (gR . b₁) where b₁ is Element of (gR) : not (gR) = {} } is set
{ (gR . b₁) where b₁ is Element of (gR) : not (gR) = {} } is set
( { (gR . b₁) where b₁ is Element of (gR) : not (gR) = {} } , { (gR . b₁) where b₁ is Element of (gR) : not (gR) = {} } ) is () ()
g1 is set
{ (gR . b₁) where b₁ is Element of (gR) : not (gR) = {} } \/ { (gR . b₁) where b₁ is Element of (gR) : not (gR) = {} } is set
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₁) where b₁ is Element of (gLR) : not (gLR) = {} } is set
{ ((gR | (gR)) . b₁) where b₁ is Element of (gLR) : not (gLR) = {} } is set
(gLR) is set
{ (gR . b₁) where b₁ is Element of (gLR) : not (gLR) = {} } is set
{ ((gR | (gR)) . b₁) where b₁ is Element of (gLR) : not (gLR) = {} } is set
gR . gLR is set
( { (gR . b₁) where b₁ is Element of (gLR) : not (gLR) = {} } , { (gR . b₁) where b₁ is Element of (gLR) : not (gLR) = {} } ) is () ()
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₁) where b₁ is Element of (gLR) : not (gLR) = {} } , { ((gR | (gR)) . b₁) where b₁ is Element of (gLR) : not (gLR) = {} } ) is () ()
(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₁) where b₁ is Element of (g) : not (g) = {} } is set
{ (gR . b₁) where b₁ is Element of (g) : not (g) = {} } is set
( { (gR . b₁) where b₁ is Element of (g) : not (g) = {} } , { (gR . b₁) where b₁ is Element of (g) : not (g) = {} } ) is () ()
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₁ where b₁ is Element of K53((gR)) : S₂[b₁] } is set
union { b₁ where b₁ is Element of K53((gR)) : S₂[b₁] } is set
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₁₂ is () set
(gL) is set
(c₁₂) is set
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