STACKS_1

:: STACKS_1 semantic presentation

REAL is set
NAT is non empty V39() V40() V41() V46() V51() V52() Element of bool REAL
bool REAL is non empty set
NAT is non empty V39() V40() V41() V46() V51() V52() set
bool NAT is non empty V46() set
bool NAT is non empty V46() set
1 is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
2 is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
{} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty ext-real non positive non negative irreflexive V39() V40() V41() V43() V44() V45() V46() V51() V53( {} ) FinSequence-like FinSubsequence-like FinSequence-membered co-well_founded weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V110() V246() set
the Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty ext-real non positive non negative irreflexive V39() V40() V41() V43() V44() V45() V46() V51() V53( {} ) FinSequence-like FinSubsequence-like FinSequence-membered co-well_founded weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V110() V246() set is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty ext-real non positive non negative irreflexive V39() V40() V41() V43() V44() V45() V46() V51() V53( {} ) FinSequence-like FinSubsequence-like FinSequence-membered co-well_founded weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V110() V246() set
{{},1} is non empty set
K439() is set
bool K439() is non empty set
K440() is Element of bool K439()
K480() is non empty V221() L22()
the carrier of K480() is non empty set
K443( the carrier of K480()) is non empty M32( the carrier of K480())
K479(K480()) is Element of bool K443( the carrier of K480())
bool K443( the carrier of K480()) is non empty set
[:K479(K480()),NAT:] is Relation-like set
bool [:K479(K480()),NAT:] is non empty set
[:NAT,K479(K480()):] is Relation-like set
bool [:NAT,K479(K480()):] is non empty set
K532() is set
bool K532() is non empty set
[:K532(),NAT:] is Relation-like set
bool [:K532(),NAT:] is non empty set
K534() is M16(K532())
K536() is set
K537() is set
K538() is set
K89(K536(),K537(),K538()) is non empty set
[:K534(),NAT:] is Relation-like set
K579() is non empty V204() V206() V207() V208() L21()
the carrier of K579() is non empty set
COMPLEX is set
RAT is set
INT is set
[:NAT,REAL:] is Relation-like set
bool [:NAT,REAL:] is non empty set
K278(1,NAT) is M16( NAT )
3 is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty ext-real non positive non negative irreflexive V39() V40() V41() V43() V44() V45() V46() V51() V53( {} ) FinSequence-like FinSubsequence-like FinSequence-membered co-well_founded weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V110() V246() Element of NAT
X is set
G is Relation-like NAT -defined X -valued Function-like V46() FinSequence-like FinSubsequence-like FinSequence of X
c₃ is Relation-like NAT -defined X -valued Function-like V46() FinSequence-like FinSubsequence-like FinSequence of X
G ^ c₃ is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like set
X * is functional non empty FinSequence-membered M16(X)
G ^ c₃ is Relation-like NAT -defined X -valued Function-like V46() FinSequence-like FinSubsequence-like FinSequence of X
X is set
G is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() set
c₃ is Relation-like NAT -defined X -valued Function-like V46() FinSequence-like FinSubsequence-like FinSequence of X
Del (c₃,G) is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like set
X * is functional non empty FinSequence-membered M16(X)
rng (Del (c₃,G)) is set
rng c₃ is Element of bool X
bool X is non empty set
X is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() set
Del ({},X) is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like set
dom (Del ({},X)) is Element of bool NAT
dom {} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty proper ext-real non positive non negative irreflexive V39() V40() V41() V43() V44() V45() V46() V51() V53( {} ) FinSequence-like FinSubsequence-like FinSequence-membered co-well_founded weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V110() V246() Element of bool NAT
F₁() is non empty set
<*> F₁() is Relation-like non-empty empty-yielding NAT -defined F₁() -valued Function-like one-to-one constant functional empty proper ext-real non positive non negative irreflexive V39() V40() V41() V43() V44() V45() V46() V51() V53( {} ) FinSequence-like FinSubsequence-like FinSequence-membered co-well_founded weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V110() V246() FinSequence of F₁()
[:NAT,F₁():] is Relation-like non empty V46() set
X is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() set
X + 1 is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
G is Relation-like NAT -defined F₁() -valued Function-like V46() FinSequence-like FinSubsequence-like FinSequence of F₁()
len G is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
X2 is Element of F₁()
<*X2*> is Relation-like NAT -defined F₁() -valued Function-like constant non empty trivial V46() V53(1) FinSequence-like FinSubsequence-like FinSequence of F₁()
[1,X2] is set
{1,X2} is non empty set
{1} is non empty trivial V53(1) set
{{1,X2},{1}} is non empty set
{[1,X2]} is Relation-like Function-like constant non empty trivial V53(1) set
c₃ is Relation-like NAT -defined F₁() -valued Function-like V46() FinSequence-like FinSubsequence-like FinSequence of F₁()
(F₁(),<*X2*>,c₃) is Relation-like NAT -defined F₁() -valued Function-like non empty V46() FinSequence-like FinSubsequence-like Element of F₁() *
F₁() * is functional non empty FinSequence-membered M16(F₁())
len c₃ is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
(len c₃) + 1 is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
X is Relation-like NAT -defined F₁() -valued Function-like V46() FinSequence-like FinSubsequence-like FinSequence of F₁()
len X is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
G is Relation-like NAT -defined F₁() -valued Function-like V46() FinSequence-like FinSubsequence-like FinSequence of F₁()
len G is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
X is non empty set
G is non empty set
[:X,G:] is Relation-like non empty set
[:[:X,G:],G:] is Relation-like non empty set
bool [:[:X,G:],G:] is non empty set
c₃ is Relation-like set
pr2 (X,G) is Relation-like [:X,G:] -defined G -valued Function-like non empty total quasi_total Element of bool [:[:X,G:],G:]
X2 is Relation-like [:X,G:] -defined G -valued Function-like non empty total quasi_total Element of bool [:[:X,G:],G:]
A is Element of X
s1 is Element of G
s2 is Element of G
[s1,s2] is Element of [:G,G:]
[:G,G:] is Relation-like non empty set
{s1,s2} is non empty set
{s1} is non empty trivial V53(1) set
{{s1,s2},{s1}} is non empty set
X2 . (A,s1) is Element of G
[A,s1] is set
{A,s1} is non empty set
{A} is non empty trivial V53(1) set
{{A,s1},{A}} is non empty set
X2 . [A,s1] is set
X2 . (A,s2) is Element of G
[A,s2] is set
{A,s2} is non empty set
{{A,s2},{A}} is non empty set
X2 . [A,s2] is set
[(X2 . (A,s1)),(X2 . (A,s2))] is Element of [:G,G:]
{(X2 . (A,s1)),(X2 . (A,s2))} is non empty set
{(X2 . (A,s1))} is non empty trivial V53(1) set
{{(X2 . (A,s1)),(X2 . (A,s2))},{(X2 . (A,s1))}} is non empty set
F₃() is non empty set
F₁() is non empty set
F₂() is non empty set
[:F₁(),F₂():] is Relation-like non empty set
[:[:F₁(),F₂():],F₃():] is Relation-like non empty set
bool [:[:F₁(),F₂():],F₃():] is non empty set
X is Relation-like [:F₁(),F₂():] -defined Function-like total set
dom X is Relation-like F₁() -defined F₂() -valued Element of bool [:F₁(),F₂():]
bool [:F₁(),F₂():] is non empty set
rng X is set
G is set
c₃ is set
X . c₃ is set
X2 is set
A is set
[X2,A] is set
{X2,A} is non empty set
{X2} is non empty trivial V53(1) set
{{X2,A},{X2}} is non empty set
X . (X2,A) is set
X . [X2,A] is set
F₄(X2,A) is Element of F₃()
G is Relation-like [:F₁(),F₂():] -defined F₃() -valued Function-like non empty total quasi_total Element of bool [:[:F₁(),F₂():],F₃():]
c₃ is Element of F₁()
X2 is Element of F₂()
G . (c₃,X2) is Element of F₃()
[c₃,X2] is set
{c₃,X2} is non empty set
{c₃} is non empty trivial V53(1) set
{{c₃,X2},{c₃}} is non empty set
G . [c₃,X2] is set
F₄(c₃,X2) is Element of F₃()
G is non empty set
[:G,G:] is Relation-like non empty set
bool [:G,G:] is non empty set
X is non empty set
[:X,G:] is Relation-like non empty set
[:[:X,G:],G:] is Relation-like non empty set
bool [:[:X,G:],G:] is non empty set
X2 is Relation-like [:X,G:] -defined G -valued Function-like non empty total quasi_total Element of bool [:[:X,G:],G:]
c₃ is Relation-like G -defined G -valued total quasi_total reflexive symmetric transitive Element of bool [:G,G:]
Class c₃ is non empty with_non-empty_elements a_partition of G
[:X,(Class c₃):] is Relation-like non empty set
[:[:X,(Class c₃):],(Class c₃):] is Relation-like non empty set
bool [:[:X,(Class c₃):],(Class c₃):] is non empty set
A is set
s1 is set
Class (c₃,s1) is Element of bool G
bool G is non empty set
{s1} is non empty trivial V53(1) set
c₃ .: {s1} is set
A is Relation-like Function-like set
dom A is set
rng A is set
s1 is set
s2 is set
A . s2 is set
bool G is non empty set
[:G,(Class c₃):] is Relation-like non empty set
bool [:G,(Class c₃):] is non empty set
s1 is Relation-like G -defined Class c₃ -valued Function-like non empty total quasi_total Element of bool [:G,(Class c₃):]
[:(Class c₃),G:] is Relation-like non empty set
bool [:(Class c₃),G:] is non empty set
s2 is Relation-like Class c₃ -defined G -valued Function-like non empty total quasi_total Element of bool [:(Class c₃),G:]
e1 is Relation-like [:X,(Class c₃):] -defined Class c₃ -valued Function-like non empty total quasi_total Element of bool [:[:X,(Class c₃):],(Class c₃):]
e2 is set
q2 is set
e1 is set
e1 . (e2,q2) is set
[e2,q2] is set
{e2,q2} is non empty set
{e2} is non empty trivial V53(1) set
{{e2,q2},{e2}} is non empty set
e1 . [e2,q2] is set
X2 . (e2,e1) is set
[e2,e1] is set
{e2,e1} is non empty set
{{e2,e1},{e2}} is non empty set
X2 . [e2,e1] is set
Class (c₃,(X2 . (e2,e1))) is Element of bool G
{(X2 . (e2,e1))} is non empty trivial V53(1) set
c₃ .: {(X2 . (e2,e1))} is set
e3 is Element of Class c₃
s2 . e3 is Element of G
a is Element of G
[(s2 . e3),a] is Element of [:G,G:]
{(s2 . e3),a} is non empty set
{(s2 . e3)} is non empty trivial V53(1) set
{{(s2 . e3),a},{(s2 . e3)}} is non empty set
v is set
Class (c₃,v) is Element of bool G
{v} is non empty trivial V53(1) set
c₃ .: {v} is set
e2 is Element of X
X2 . (e2,(s2 . e3)) is Element of G
[e2,(s2 . e3)] is set
{e2,(s2 . e3)} is non empty set
{e2} is non empty trivial V53(1) set
{{e2,(s2 . e3)},{e2}} is non empty set
X2 . [e2,(s2 . e3)] is set
X2 . (e2,a) is Element of G
[e2,a] is set
{e2,a} is non empty set
{{e2,a},{e2}} is non empty set
X2 . [e2,a] is set
[(X2 . (e2,(s2 . e3))),(X2 . (e2,a))] is Element of [:G,G:]
{(X2 . (e2,(s2 . e3))),(X2 . (e2,a))} is non empty set
{(X2 . (e2,(s2 . e3)))} is non empty trivial V53(1) set
{{(X2 . (e2,(s2 . e3))),(X2 . (e2,a))},{(X2 . (e2,(s2 . e3)))}} is non empty set
EqClass (c₃,(X2 . (e2,a))) is Element of Class c₃
{(X2 . (e2,a))} is non empty trivial V53(1) set
c₃ .: {(X2 . (e2,a))} is set
s1 . (X2 . (e2,(s2 . e3))) is Element of Class c₃
EqClass (c₃,(X2 . (e2,(s2 . e3)))) is Element of Class c₃
c₃ .: {(X2 . (e2,(s2 . e3)))} is set
e1 . (e2,e3) is Element of Class c₃
[e2,e3] is set
{e2,e3} is non empty set
{{e2,e3},{e2}} is non empty set
e1 . [e2,e3] is set
A is Relation-like [:X,(Class c₃):] -defined Class c₃ -valued Function-like non empty total quasi_total Element of bool [:[:X,(Class c₃):],(Class c₃):]
s1 is Relation-like [:X,(Class c₃):] -defined Class c₃ -valued Function-like non empty total quasi_total Element of bool [:[:X,(Class c₃):],(Class c₃):]
bool G is non empty set
e1 is Element of Class c₃
e2 is set
Class (c₃,e2) is Element of bool G
{e2} is non empty trivial V53(1) set
c₃ .: {e2} is set
s2 is Element of X
A . (s2,e1) is Element of Class c₃
[s2,e1] is set
{s2,e1} is non empty set
{s2} is non empty trivial V53(1) set
{{s2,e1},{s2}} is non empty set
A . [s2,e1] is set
X2 . (s2,e2) is set
[s2,e2] is set
{s2,e2} is non empty set
{{s2,e2},{s2}} is non empty set
X2 . [s2,e2] is set
Class (c₃,(X2 . (s2,e2))) is Element of bool G
{(X2 . (s2,e2))} is non empty trivial V53(1) set
c₃ .: {(X2 . (s2,e2))} is set
s1 . (s2,e1) is Element of Class c₃
s1 . [s2,e1] is set
X is non empty set
bool X is non empty set
G is non empty set
bool G is non empty set
[:X,G:] is Relation-like non empty set
bool [:X,G:] is non empty set
c₃ is Element of bool X
X2 is Element of bool G
[:c₃,X2:] is Relation-like set
bool [:c₃,X2:] is non empty set
A is Relation-like X -defined G -valued Function-like non empty total quasi_total Element of bool [:X,G:]
s1 is Relation-like c₃ -defined X2 -valued Function-like quasi_total Element of bool [:c₃,X2:]
A +* s1 is Relation-like Function-like non empty set
A +* {} is Relation-like Function-like non empty set
dom (A +* s1) is non empty set
dom A is non empty Element of bool X
dom s1 is Element of bool c₃
bool c₃ is non empty set
(dom A) \/ (dom s1) is non empty set
X \/ (dom s1) is non empty set
X \/ c₃ is non empty set
rng (A +* s1) is non empty set
rng A is non empty Element of bool G
rng s1 is Element of bool X2
bool X2 is non empty set
(rng A) \/ (rng s1) is non empty set
G \/ X2 is non empty set
G is set
bool G is non empty set
X is non empty set
[:X,G:] is Relation-like set
[:[:X,G:],G:] is Relation-like set
bool [:[:X,G:],G:] is non empty set
[:G,G:] is Relation-like set
bool [:G,G:] is non empty set
[:G,X:] is Relation-like set
bool [:G,X:] is non empty set
c₃ is Element of bool G
X2 is Relation-like [:X,G:] -defined G -valued Function-like quasi_total Element of bool [:[:X,G:],G:]
A is Relation-like G -defined G -valued Function-like total quasi_total Element of bool [:G,G:]
s1 is Relation-like G -defined X -valued Function-like total quasi_total Element of bool [:G,X:]
(X,G,c₃,X2,A,s1) is () ()
G is non empty set
bool G is non empty set
X is set
[:X,G:] is Relation-like set
[:[:X,G:],G:] is Relation-like set
bool [:[:X,G:],G:] is non empty set
[:G,G:] is Relation-like non empty set
bool [:G,G:] is non empty set
[:G,X:] is Relation-like set
bool [:G,X:] is non empty set
c₃ is Element of bool G
X2 is Relation-like [:X,G:] -defined G -valued Function-like total quasi_total Element of bool [:[:X,G:],G:]
A is Relation-like G -defined G -valued Function-like non empty total quasi_total Element of bool [:G,G:]
s1 is Relation-like G -defined X -valued Function-like quasi_total Element of bool [:G,X:]
(X,G,c₃,X2,A,s1) is () ()
the non empty set is non empty set
bool the non empty set is non empty set
the Element of bool the non empty set is Element of bool the non empty set
[: the non empty set , the non empty set :] is Relation-like non empty set
[:[: the non empty set , the non empty set :], the non empty set :] is Relation-like non empty set
bool [:[: the non empty set , the non empty set :], the non empty set :] is non empty set
the Relation-like [: the non empty set , the non empty set :] -defined the non empty set -valued Function-like non empty total quasi_total Element of bool [:[: the non empty set , the non empty set :], the non empty set :] is Relation-like [: the non empty set , the non empty set :] -defined the non empty set -valued Function-like non empty total quasi_total Element of bool [:[: the non empty set , the non empty set :], the non empty set :]
bool [: the non empty set , the non empty set :] is non empty set
the Relation-like the non empty set -defined the non empty set -valued Function-like non empty total quasi_total Element of bool [: the non empty set , the non empty set :] is Relation-like the non empty set -defined the non empty set -valued Function-like non empty total quasi_total Element of bool [: the non empty set , the non empty set :]
( the non empty set , the non empty set , the Element of bool the non empty set , the Relation-like [: the non empty set , the non empty set :] -defined the non empty set -valued Function-like non empty total quasi_total Element of bool [:[: the non empty set , the non empty set :], the non empty set :], the Relation-like the non empty set -defined the non empty set -valued Function-like non empty total quasi_total Element of bool [: the non empty set , the non empty set :], the Relation-like the non empty set -defined the non empty set -valued Function-like non empty total quasi_total Element of bool [: the non empty set , the non empty set :]) is non empty non void V67() () ()
X is ()
the carrier' of X is set
X is non void ()
the carrier' of X is non empty set
the of X is Relation-like the carrier' of X -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X, the carrier' of X:]
[: the carrier' of X, the carrier' of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier' of X:] is non empty set
G is Element of the carrier' of X
the of X . G is Element of the carrier' of X
the carrier of X is set
the of X is Relation-like the carrier' of X -defined the carrier of X -valued Function-like quasi_total Element of bool [: the carrier' of X, the carrier of X:]
[: the carrier' of X, the carrier of X:] is Relation-like set
bool [: the carrier' of X, the carrier of X:] is non empty set
the of X . G is Element of the carrier of X
X is non empty non void V67() ()
the carrier' of X is non empty set
the carrier of X is non empty set
the of X is Relation-like [: the carrier of X, the carrier' of X:] -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of X, the carrier' of X:], the carrier' of X:]
[: the carrier of X, the carrier' of X:] is Relation-like non empty set
[:[: the carrier of X, the carrier' of X:], the carrier' of X:] is Relation-like non empty set
bool [:[: the carrier of X, the carrier' of X:], the carrier' of X:] is non empty set
c₃ is Element of the carrier of X
G is Element of the carrier' of X
the of X . (c₃,G) is Element of the carrier' of X
[c₃,G] is set
{c₃,G} is non empty set
{c₃} is non empty trivial V53(1) set
{{c₃,G},{c₃}} is non empty set
the of X . [c₃,G] is set
X is non empty set
X * is functional non empty FinSequence-membered M16(X)
<*> X is Relation-like non-empty empty-yielding NAT -defined X -valued Function-like one-to-one constant functional empty proper ext-real non positive non negative irreflexive V39() V40() V41() V43() V44() V45() V46() V51() V53( {} ) FinSequence-like FinSubsequence-like FinSequence-membered co-well_founded weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V110() V246() FinSequence of X
[:NAT,X:] is Relation-like non empty V46() set
G is Relation-like NAT -defined X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of X *
{G} is functional non empty trivial V53(1) FinSequence-membered Element of bool (X *)
bool (X *) is non empty set
the Element of X is Element of X
[:X,(X *):] is Relation-like non empty set
[:[:X,(X *):],(X *):] is Relation-like non empty set
bool [:[:X,(X *):],(X *):] is non empty set
X2 is Relation-like [:X,(X *):] -defined X * -valued Function-like non empty total quasi_total Element of bool [:[:X,(X *):],(X *):]
[:(X *),(X *):] is Relation-like non empty set
bool [:(X *),(X *):] is non empty set
A is Relation-like X * -defined X * -valued Function-like non empty total quasi_total Element of bool [:(X *),(X *):]
[:(X *),X:] is Relation-like non empty set
bool [:(X *),X:] is non empty set
s1 is Relation-like X * -defined X -valued Function-like non empty total quasi_total Element of bool [:(X *),X:]
(X,(X *),{G},X2,A,s1) is non empty non void V67() () ()
s2 is non empty non void V67() () ()
the carrier of s2 is non empty set
the carrier' of s2 is non empty set
the Element of the carrier of s2 is Element of the carrier of s2
e1 is Element of the carrier' of s2
(s2,e1) is Element of the carrier of s2
the of s2 is Relation-like the carrier' of s2 -defined the carrier of s2 -valued Function-like non empty total quasi_total Element of bool [: the carrier' of s2, the carrier of s2:]
[: the carrier' of s2, the carrier of s2:] is Relation-like non empty set
bool [: the carrier' of s2, the carrier of s2:] is non empty set
the of s2 . e1 is Element of the carrier of s2
(s2,e1) is Element of the carrier' of s2
the of s2 is Relation-like the carrier' of s2 -defined the carrier' of s2 -valued Function-like non empty total quasi_total Element of bool [: the carrier' of s2, the carrier' of s2:]
[: the carrier' of s2, the carrier' of s2:] is Relation-like non empty set
bool [: the carrier' of s2, the carrier' of s2:] is non empty set
the of s2 . e1 is Element of the carrier' of s2
e2 is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like set
e2 . 1 is set
Del (e2,1) is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like set
q2 is Relation-like NAT -defined X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of X *
dom q2 is Element of bool NAT
q2 /. 1 is Element of X
IFEQ (e1,{}, the Element of X,(q2 /. 1)) is Element of X
e1 is Element of the carrier of s2
(s2,e1,e1) is Element of the carrier' of s2
the of s2 is Relation-like [: the carrier of s2, the carrier' of s2:] -defined the carrier' of s2 -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of s2, the carrier' of s2:], the carrier' of s2:]
[: the carrier of s2, the carrier' of s2:] is Relation-like non empty set
[:[: the carrier of s2, the carrier' of s2:], the carrier' of s2:] is Relation-like non empty set
bool [:[: the carrier of s2, the carrier' of s2:], the carrier' of s2:] is non empty set
the of s2 . (e1,e1) is Element of the carrier' of s2
[e1,e1] is set
{e1,e1} is non empty set
{e1} is non empty trivial V53(1) set
{{e1,e1},{e1}} is non empty set
the of s2 . [e1,e1] is set
<*e1*> is Relation-like NAT -defined the carrier of s2 -valued Function-like constant non empty trivial V46() V53(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of s2
[1,e1] is set
{1,e1} is non empty set
{1} is non empty trivial V53(1) set
{{1,e1},{1}} is non empty set
{[1,e1]} is Relation-like Function-like constant non empty trivial V53(1) set
<*e1*> ^ e2 is Relation-like NAT -defined Function-like non empty V46() FinSequence-like FinSubsequence-like set
G is non empty non void V67() () ()
the carrier of G is non empty set
the carrier' of G is non empty set
the Element of the carrier of G is Element of the carrier of G
c₃ is non empty non void V67() () ()
the carrier of c₃ is non empty set
the carrier' of c₃ is non empty set
the Element of the carrier of c₃ is Element of the carrier of c₃
X2 is Element of X
s2 is Relation-like NAT -defined X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of X *
the of G is Relation-like [: the carrier of G, the carrier' of G:] -defined the carrier' of G -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of G, the carrier' of G:], the carrier' of G:]
[: the carrier of G, the carrier' of G:] is Relation-like non empty set
[:[: the carrier of G, the carrier' of G:], the carrier' of G:] is Relation-like non empty set
bool [:[: the carrier of G, the carrier' of G:], the carrier' of G:] is non empty set
the of G . (X2,s2) is set
[X2,s2] is set
{X2,s2} is non empty set
{X2} is non empty trivial V53(1) set
{{X2,s2},{X2}} is non empty set
the of G . [X2,s2] is set
e1 is Element of the carrier' of G
A is Element of the carrier of G
(G,e1,A) is Element of the carrier' of G
the of G . (A,e1) is Element of the carrier' of G
[A,e1] is set
{A,e1} is non empty set
{A} is non empty trivial V53(1) set
{{A,e1},{A}} is non empty set
the of G . [A,e1] is set
<*X2*> is Relation-like NAT -defined X -valued Function-like constant non empty trivial V46() V53(1) FinSequence-like FinSubsequence-like FinSequence of X
[1,X2] is set
{1,X2} is non empty set
{1} is non empty trivial V53(1) set
{{1,X2},{1}} is non empty set
{[1,X2]} is Relation-like Function-like constant non empty trivial V53(1) set
(X,<*X2*>,s2) is Relation-like NAT -defined X -valued Function-like non empty V46() FinSequence-like FinSubsequence-like Element of X *
e2 is Element of the carrier' of c₃
s1 is Element of the carrier of c₃
(c₃,e2,s1) is Element of the carrier' of c₃
the of c₃ is Relation-like [: the carrier of c₃, the carrier' of c₃:] -defined the carrier' of c₃ -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of c₃, the carrier' of c₃:], the carrier' of c₃:]
[: the carrier of c₃, the carrier' of c₃:] is Relation-like non empty set
[:[: the carrier of c₃, the carrier' of c₃:], the carrier' of c₃:] is Relation-like non empty set
bool [:[: the carrier of c₃, the carrier' of c₃:], the carrier' of c₃:] is non empty set
the of c₃ . (s1,e2) is Element of the carrier' of c₃
[s1,e2] is set
{s1,e2} is non empty set
{s1} is non empty trivial V53(1) set
{{s1,e2},{s1}} is non empty set
the of c₃ . [s1,e2] is set
the of c₃ . (X2,s2) is set
the of c₃ . [X2,s2] is set
X2 is Relation-like NAT -defined X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of X *
A is Element of the carrier' of G
s1 is Element of the carrier' of c₃
the of G is Relation-like the carrier' of G -defined the carrier' of G -valued Function-like non empty total quasi_total Element of bool [: the carrier' of G, the carrier' of G:]
[: the carrier' of G, the carrier' of G:] is Relation-like non empty set
bool [: the carrier' of G, the carrier' of G:] is non empty set
the of G . X2 is set
(G,A) is Element of the carrier' of G
the of G . A is Element of the carrier' of G
(X,1,X2) is Relation-like NAT -defined X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of X *
(c₃,s1) is Element of the carrier' of c₃
the of c₃ is Relation-like the carrier' of c₃ -defined the carrier' of c₃ -valued Function-like non empty total quasi_total Element of bool [: the carrier' of c₃, the carrier' of c₃:]
[: the carrier' of c₃, the carrier' of c₃:] is Relation-like non empty set
bool [: the carrier' of c₃, the carrier' of c₃:] is non empty set
the of c₃ . s1 is Element of the carrier' of c₃
the of c₃ . X2 is set
A is Element of the carrier' of G
s1 is Element of the carrier' of c₃
the of G is Relation-like the carrier' of G -defined the carrier' of G -valued Function-like non empty total quasi_total Element of bool [: the carrier' of G, the carrier' of G:]
[: the carrier' of G, the carrier' of G:] is Relation-like non empty set
bool [: the carrier' of G, the carrier' of G:] is non empty set
the of G . X2 is set
(G,A) is Element of the carrier' of G
the of G . A is Element of the carrier' of G
(c₃,s1) is Element of the carrier' of c₃
the of c₃ is Relation-like the carrier' of c₃ -defined the carrier' of c₃ -valued Function-like non empty total quasi_total Element of bool [: the carrier' of c₃, the carrier' of c₃:]
[: the carrier' of c₃, the carrier' of c₃:] is Relation-like non empty set
bool [: the carrier' of c₃, the carrier' of c₃:] is non empty set
the of c₃ . s1 is Element of the carrier' of c₃
the of c₃ . X2 is set
A is Element of the carrier' of G
the of G is Relation-like the carrier' of G -defined the carrier' of G -valued Function-like non empty total quasi_total Element of bool [: the carrier' of G, the carrier' of G:]
[: the carrier' of G, the carrier' of G:] is Relation-like non empty set
bool [: the carrier' of G, the carrier' of G:] is non empty set
the of c₃ is Relation-like the carrier' of c₃ -defined the carrier' of c₃ -valued Function-like non empty total quasi_total Element of bool [: the carrier' of c₃, the carrier' of c₃:]
[: the carrier' of c₃, the carrier' of c₃:] is Relation-like non empty set
bool [: the carrier' of c₃, the carrier' of c₃:] is non empty set
the of G is Relation-like the carrier' of G -defined the carrier' of G -valued Function-like non empty total quasi_total Element of bool [: the carrier' of G, the carrier' of G:]
[: the carrier' of G, the carrier' of G:] is Relation-like non empty set
bool [: the carrier' of G, the carrier' of G:] is non empty set
the of c₃ is Relation-like the carrier' of c₃ -defined the carrier' of c₃ -valued Function-like non empty total quasi_total Element of bool [: the carrier' of c₃, the carrier' of c₃:]
[: the carrier' of c₃, the carrier' of c₃:] is Relation-like non empty set
bool [: the carrier' of c₃, the carrier' of c₃:] is non empty set
X2 is Relation-like NAT -defined X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of X *
A is Element of the carrier' of G
s1 is Element of the carrier' of c₃
the of G is Relation-like the carrier' of G -defined the carrier of G -valued Function-like non empty total quasi_total Element of bool [: the carrier' of G, the carrier of G:]
[: the carrier' of G, the carrier of G:] is Relation-like non empty set
bool [: the carrier' of G, the carrier of G:] is non empty set
the of G . X2 is set
(G,A) is Element of the carrier of G
the of G . A is Element of the carrier of G
X2 . 1 is set
(c₃,s1) is Element of the carrier of c₃
the of c₃ is Relation-like the carrier' of c₃ -defined the carrier of c₃ -valued Function-like non empty total quasi_total Element of bool [: the carrier' of c₃, the carrier of c₃:]
[: the carrier' of c₃, the carrier of c₃:] is Relation-like non empty set
bool [: the carrier' of c₃, the carrier of c₃:] is non empty set
the of c₃ . s1 is Element of the carrier of c₃
the of c₃ . X2 is set
A is Element of the carrier' of G
s1 is Element of the carrier' of c₃
the of G is Relation-like the carrier' of G -defined the carrier of G -valued Function-like non empty total quasi_total Element of bool [: the carrier' of G, the carrier of G:]
[: the carrier' of G, the carrier of G:] is Relation-like non empty set
bool [: the carrier' of G, the carrier of G:] is non empty set
the of G . X2 is set
(G,A) is Element of the carrier of G
the of G . A is Element of the carrier of G
the Element of X is Element of X
(c₃,s1) is Element of the carrier of c₃
the of c₃ is Relation-like the carrier' of c₃ -defined the carrier of c₃ -valued Function-like non empty total quasi_total Element of bool [: the carrier' of c₃, the carrier of c₃:]
[: the carrier' of c₃, the carrier of c₃:] is Relation-like non empty set
bool [: the carrier' of c₃, the carrier of c₃:] is non empty set
the of c₃ . s1 is Element of the carrier of c₃
the of c₃ . X2 is set
A is Element of the carrier' of G
the of G is Relation-like the carrier' of G -defined the carrier of G -valued Function-like non empty total quasi_total Element of bool [: the carrier' of G, the carrier of G:]
[: the carrier' of G, the carrier of G:] is Relation-like non empty set
bool [: the carrier' of G, the carrier of G:] is non empty set
the of c₃ is Relation-like the carrier' of c₃ -defined the carrier of c₃ -valued Function-like non empty total quasi_total Element of bool [: the carrier' of c₃, the carrier of c₃:]
[: the carrier' of c₃, the carrier of c₃:] is Relation-like non empty set
bool [: the carrier' of c₃, the carrier of c₃:] is non empty set
the of G is Relation-like the carrier' of G -defined the carrier of G -valued Function-like non empty total quasi_total Element of bool [: the carrier' of G, the carrier of G:]
[: the carrier' of G, the carrier of G:] is Relation-like non empty set
bool [: the carrier' of G, the carrier of G:] is non empty set
the of c₃ is Relation-like the carrier' of c₃ -defined the carrier of c₃ -valued Function-like non empty total quasi_total Element of bool [: the carrier' of c₃, the carrier of c₃:]
[: the carrier' of c₃, the carrier of c₃:] is Relation-like non empty set
bool [: the carrier' of c₃, the carrier of c₃:] is non empty set
the of G is Element of bool the carrier' of G
bool the carrier' of G is non empty set
the of c₃ is Element of bool the carrier' of c₃
bool the carrier' of c₃ is non empty set
X2 is set
A is Element of the carrier' of G
s1 is Element of the carrier' of c₃
X2 is set
A is Element of the carrier' of c₃
s1 is Element of the carrier' of G
X is non empty set
(X) is non empty non void V67() () ()
the carrier' of (X) is non empty set
X * is functional non empty FinSequence-membered M16(X)
X is non empty set
(X) is non empty non void V67() () ()
the carrier' of (X) is functional non empty set
X * is functional non empty FinSequence-membered M16(X)
G is Relation-like Function-like Element of the carrier' of (X)
X is non empty set
(X) is non empty non void V67() () ()
the carrier' of (X) is functional non empty set
[:NAT, the carrier' of (X):] is Relation-like non empty V46() set
bool [:NAT, the carrier' of (X):] is non empty V46() set
c₃ is Relation-like NAT -defined the carrier' of (X) -valued Function-like non empty total quasi_total Element of bool [:NAT, the carrier' of (X):]
X * is functional non empty FinSequence-membered M16(X)
c₃ . 1 is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier' of (X)
X2 is Relation-like NAT -defined X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of X *
len X2 is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
A is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
s1 is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
c₃ . s1 is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier' of (X)
A is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() set
s1 is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() set
s1 + 1 is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
e1 is Relation-like NAT -defined X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of X *
s2 is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() set
c₃ . s2 is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier' of (X)
len e1 is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
e2 is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier' of (X)
((X),e2) is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier' of (X)
the of (X) is Relation-like the carrier' of (X) -defined the carrier' of (X) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (X), the carrier' of (X):]
[: the carrier' of (X), the carrier' of (X):] is Relation-like non empty set
bool [: the carrier' of (X), the carrier' of (X):] is non empty set
the of (X) . e2 is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier' of (X)
q2 is Relation-like NAT -defined X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of X *
len q2 is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
e1 is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
s2 + 1 is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
c₃ . (s2 + 1) is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier' of (X)
(X,1,e1) is Relation-like NAT -defined X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of X *
dom e1 is Element of bool NAT
s1 is Relation-like NAT -defined X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of X *
A is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() set
c₃ . A is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier' of (X)
len s1 is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
s1 is Relation-like NAT -defined X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of X *
A is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() set
c₃ . A is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier' of (X)
len s1 is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
s2 is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier' of (X)
the carrier' of (X) is functional non empty set
c₃ is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier' of (X)
((X),c₃) is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier' of (X)
the of (X) is Relation-like the carrier' of (X) -defined the carrier' of (X) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (X), the carrier' of (X):]
[: the carrier' of (X), the carrier' of (X):] is Relation-like non empty set
bool [: the carrier' of (X), the carrier' of (X):] is non empty set
the of (X) . c₃ is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier' of (X)
((X),c₃) is Element of the carrier of (X)
the carrier of (X) is non empty set
the of (X) is Relation-like the carrier' of (X) -defined the carrier of (X) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (X), the carrier of (X):]
[: the carrier' of (X), the carrier of (X):] is Relation-like non empty set
bool [: the carrier' of (X), the carrier of (X):] is non empty set
the of (X) . c₃ is Element of the carrier of (X)
((X),((X),c₃),((X),c₃)) is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier' of (X)
the of (X) is Relation-like [: the carrier of (X), the carrier' of (X):] -defined the carrier' of (X) -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of (X), the carrier' of (X):], the carrier' of (X):]
[: the carrier of (X), the carrier' of (X):] is Relation-like non empty set
[:[: the carrier of (X), the carrier' of (X):], the carrier' of (X):] is Relation-like non empty set
bool [:[: the carrier of (X), the carrier' of (X):], the carrier' of (X):] is non empty set
the of (X) . (((X),c₃),((X),c₃)) is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier' of (X)
[((X),c₃),((X),c₃)] is set
{((X),c₃),((X),c₃)} is non empty set
{((X),c₃)} is non empty trivial V53(1) set
{{((X),c₃),((X),c₃)},{((X),c₃)}} is non empty set
the of (X) . [((X),c₃),((X),c₃)] is Relation-like Function-like set
X * is functional non empty FinSequence-membered M16(X)
X2 is Relation-like NAT -defined X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of X *
X2 . 1 is set
<*(X2 . 1)*> is Relation-like NAT -defined Function-like constant non empty trivial V46() V53(1) FinSequence-like FinSubsequence-like set
[1,(X2 . 1)] is set
{1,(X2 . 1)} is non empty set
{1} is non empty trivial V53(1) set
{{1,(X2 . 1)},{1}} is non empty set
{[1,(X2 . 1)]} is Relation-like Function-like constant non empty trivial V53(1) set
(X,1,X2) is Relation-like NAT -defined X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of X *
<*(X2 . 1)*> ^ (X,1,X2) is Relation-like NAT -defined Function-like non empty V46() FinSequence-like FinSubsequence-like set
dom X2 is Element of bool NAT
A is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier' of (X)
s1 is Element of the carrier of (X)
((X),A,s1) is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier' of (X)
the of (X) . (s1,A) is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier' of (X)
[s1,A] is set
{s1,A} is non empty set
{s1} is non empty trivial V53(1) set
{{s1,A},{s1}} is non empty set
the of (X) . [s1,A] is Relation-like Function-like set
((X),A,((X),c₃)) is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier' of (X)
the of (X) . (((X),c₃),A) is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier' of (X)
[((X),c₃),A] is set
{((X),c₃),A} is non empty set
{{((X),c₃),A},{((X),c₃)}} is non empty set
the of (X) . [((X),c₃),A] is Relation-like Function-like set
the carrier' of (X) is functional non empty set
the carrier of (X) is non empty set
c₃ is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier' of (X)
X2 is Element of the carrier of (X)
((X),c₃,X2) is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier' of (X)
the of (X) is Relation-like [: the carrier of (X), the carrier' of (X):] -defined the carrier' of (X) -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of (X), the carrier' of (X):], the carrier' of (X):]
[: the carrier of (X), the carrier' of (X):] is Relation-like non empty set
[:[: the carrier of (X), the carrier' of (X):], the carrier' of (X):] is Relation-like non empty set
bool [:[: the carrier of (X), the carrier' of (X):], the carrier' of (X):] is non empty set
the of (X) . (X2,c₃) is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier' of (X)
[X2,c₃] is set
{X2,c₃} is non empty set
{X2} is non empty trivial V53(1) set
{{X2,c₃},{X2}} is non empty set
the of (X) . [X2,c₃] is Relation-like Function-like set
((X),((X),c₃,X2)) is Element of the carrier of (X)
the of (X) is Relation-like the carrier' of (X) -defined the carrier of (X) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (X), the carrier of (X):]
[: the carrier' of (X), the carrier of (X):] is Relation-like non empty set
bool [: the carrier' of (X), the carrier of (X):] is non empty set
the of (X) . ((X),c₃,X2) is Element of the carrier of (X)
X * is functional non empty FinSequence-membered M16(X)
s1 is Relation-like NAT -defined X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of X *
<*X2*> is Relation-like NAT -defined the carrier of (X) -valued Function-like constant non empty trivial V46() V53(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of (X)
[1,X2] is set
{1,X2} is non empty set
{1} is non empty trivial V53(1) set
{{1,X2},{1}} is non empty set
{[1,X2]} is Relation-like Function-like constant non empty trivial V53(1) set
A is Relation-like NAT -defined X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of X *
<*X2*> ^ A is Relation-like NAT -defined Function-like non empty V46() FinSequence-like FinSubsequence-like set
s1 . 1 is set
the carrier' of (X) is functional non empty set
the carrier of (X) is non empty set
c₃ is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier' of (X)
X2 is Element of the carrier of (X)
((X),c₃,X2) is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier' of (X)
the of (X) is Relation-like [: the carrier of (X), the carrier' of (X):] -defined the carrier' of (X) -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of (X), the carrier' of (X):], the carrier' of (X):]
[: the carrier of (X), the carrier' of (X):] is Relation-like non empty set
[:[: the carrier of (X), the carrier' of (X):], the carrier' of (X):] is Relation-like non empty set
bool [:[: the carrier of (X), the carrier' of (X):], the carrier' of (X):] is non empty set
the of (X) . (X2,c₃) is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier' of (X)
[X2,c₃] is set
{X2,c₃} is non empty set
{X2} is non empty trivial V53(1) set
{{X2,c₃},{X2}} is non empty set
the of (X) . [X2,c₃] is Relation-like Function-like set
((X),((X),c₃,X2)) is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier' of (X)
the of (X) is Relation-like the carrier' of (X) -defined the carrier' of (X) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (X), the carrier' of (X):]
[: the carrier' of (X), the carrier' of (X):] is Relation-like non empty set
bool [: the carrier' of (X), the carrier' of (X):] is non empty set
the of (X) . ((X),c₃,X2) is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier' of (X)
X * is functional non empty FinSequence-membered M16(X)
s1 is Relation-like NAT -defined X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of X *
<*X2*> is Relation-like NAT -defined the carrier of (X) -valued Function-like constant non empty trivial V46() V53(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of (X)
[1,X2] is set
{1,X2} is non empty set
{1} is non empty trivial V53(1) set
{{1,X2},{1}} is non empty set
{[1,X2]} is Relation-like Function-like constant non empty trivial V53(1) set
A is Relation-like NAT -defined X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of X *
<*X2*> ^ A is Relation-like NAT -defined Function-like non empty V46() FinSequence-like FinSubsequence-like set
Del ((<*X2*> ^ A),1) is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like set
the carrier' of (X) is functional non empty set
the carrier of (X) is non empty set
c₃ is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier' of (X)
X2 is Element of the carrier of (X)
((X),c₃,X2) is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier' of (X)
the of (X) is Relation-like [: the carrier of (X), the carrier' of (X):] -defined the carrier' of (X) -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of (X), the carrier' of (X):], the carrier' of (X):]
[: the carrier of (X), the carrier' of (X):] is Relation-like non empty set
[:[: the carrier of (X), the carrier' of (X):], the carrier' of (X):] is Relation-like non empty set
bool [:[: the carrier of (X), the carrier' of (X):], the carrier' of (X):] is non empty set
the of (X) . (X2,c₃) is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier' of (X)
[X2,c₃] is set
{X2,c₃} is non empty set
{X2} is non empty trivial V53(1) set
{{X2,c₃},{X2}} is non empty set
the of (X) . [X2,c₃] is Relation-like Function-like set
X * is functional non empty FinSequence-membered M16(X)
<*X2*> is Relation-like NAT -defined the carrier of (X) -valued Function-like constant non empty trivial V46() V53(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of (X)
[1,X2] is set
{1,X2} is non empty set
{1} is non empty trivial V53(1) set
{{1,X2},{1}} is non empty set
{[1,X2]} is Relation-like Function-like constant non empty trivial V53(1) set
A is Relation-like NAT -defined X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of X *
<*X2*> ^ A is Relation-like NAT -defined Function-like non empty V46() FinSequence-like FinSubsequence-like set
the non empty set is non empty set
( the non empty set ) is non empty non void V67() () () () () () () ()
X is non empty non void V67() ()
the carrier' of X is non empty set
the Element of the carrier' of X is Element of the carrier' of X
X2 is Element of the carrier' of X
(X,X2) is Element of the carrier' of X
the of X is Relation-like the carrier' of X -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X, the carrier' of X:]
[: the carrier' of X, the carrier' of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier' of X:] is non empty set
the of X . X2 is Element of the carrier' of X
[:NAT, the carrier' of X:] is Relation-like non empty V46() set
bool [:NAT, the carrier' of X:] is non empty V46() set
c₃ is Relation-like NAT -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [:NAT, the carrier' of X:]
c₃ . 0 is Element of the carrier' of X
X2 is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() set
c₃ . X2 is Element of the carrier' of X
A is Element of the carrier' of X
X2 + 1 is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
c₃ . (X2 + 1) is Element of the carrier' of X
(X,A) is Element of the carrier' of X
the of X is Relation-like the carrier' of X -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X, the carrier' of X:]
[: the carrier' of X, the carrier' of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier' of X:] is non empty set
the of X . A is Element of the carrier' of X
X is non empty non void V67() () ()
the of X is Element of bool the carrier' of X
the carrier' of X is non empty set
bool the carrier' of X is non empty set
G is Element of the carrier' of X
X is non empty non void V67() ()
the carrier' of X is non empty set
the carrier of X is non empty set
G is Element of the carrier' of X
c₃ is Element of the carrier' of X
X2 is Element of the carrier of X
(X,G,X2) is Element of the carrier' of X
the of X is Relation-like [: the carrier of X, the carrier' of X:] -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of X, the carrier' of X:], the carrier' of X:]
[: the carrier of X, the carrier' of X:] is Relation-like non empty set
[:[: the carrier of X, the carrier' of X:], the carrier' of X:] is Relation-like non empty set
bool [:[: the carrier of X, the carrier' of X:], the carrier' of X:] is non empty set
the of X . (X2,G) is Element of the carrier' of X
[X2,G] is set
{X2,G} is non empty set
{X2} is non empty trivial V53(1) set
{{X2,G},{X2}} is non empty set
the of X . [X2,G] is set
A is Element of the carrier of X
(X,c₃,A) is Element of the carrier' of X
the of X . (A,c₃) is Element of the carrier' of X
[A,c₃] is set
{A,c₃} is non empty set
{A} is non empty trivial V53(1) set
{{A,c₃},{A}} is non empty set
the of X . [A,c₃] is set
(X,(X,G,X2)) is Element of the carrier of X
the of X is Relation-like the carrier' of X -defined the carrier of X -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X, the carrier of X:]
[: the carrier' of X, the carrier of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier of X:] is non empty set
the of X . (X,G,X2) is Element of the carrier of X
(X,(X,c₃,A)) is Element of the carrier of X
the of X . (X,c₃,A) is Element of the carrier of X
(X,(X,G,X2)) is Element of the carrier' of X
the of X is Relation-like the carrier' of X -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X, the carrier' of X:]
[: the carrier' of X, the carrier' of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier' of X:] is non empty set
the of X . (X,G,X2) is Element of the carrier' of X
(X,(X,c₃,A)) is Element of the carrier' of X
the of X . (X,c₃,A) is Element of the carrier' of X
X is non empty non void V67() ()
the carrier' of X is non empty set
G is Element of the carrier' of X
(X,G) is Element of the carrier' of X
the of X is Relation-like the carrier' of X -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X, the carrier' of X:]
[: the carrier' of X, the carrier' of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier' of X:] is non empty set
the of X . G is Element of the carrier' of X
(X,G) is Element of the carrier of X
the carrier of X is non empty set
the of X is Relation-like the carrier' of X -defined the carrier of X -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X, the carrier of X:]
[: the carrier' of X, the carrier of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier of X:] is non empty set
the of X . G is Element of the carrier of X
c₃ is Element of the carrier' of X
(X,c₃) is Element of the carrier' of X
the of X . c₃ is Element of the carrier' of X
(X,c₃) is Element of the carrier of X
the of X . c₃ is Element of the carrier of X
(X,(X,G),(X,G)) is Element of the carrier' of X
the of X is Relation-like [: the carrier of X, the carrier' of X:] -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of X, the carrier' of X:], the carrier' of X:]
[: the carrier of X, the carrier' of X:] is Relation-like non empty set
[:[: the carrier of X, the carrier' of X:], the carrier' of X:] is Relation-like non empty set
bool [:[: the carrier of X, the carrier' of X:], the carrier' of X:] is non empty set
the of X . ((X,G),(X,G)) is Element of the carrier' of X
[(X,G),(X,G)] is set
{(X,G),(X,G)} is non empty set
{(X,G)} is non empty trivial V53(1) set
{{(X,G),(X,G)},{(X,G)}} is non empty set
the of X . [(X,G),(X,G)] is set
F₁() is non empty non void V67() () () () () () ()
the carrier' of F₁() is non empty set
the carrier of F₁() is non empty set
F₂() is Element of the carrier' of F₁()
G is Element of the carrier' of F₁()
(F₁(),G) is Element of the carrier' of F₁()
the of F₁() is Relation-like the carrier' of F₁() -defined the carrier' of F₁() -valued Function-like non empty total quasi_total Element of bool [: the carrier' of F₁(), the carrier' of F₁():]
[: the carrier' of F₁(), the carrier' of F₁():] is Relation-like non empty set
bool [: the carrier' of F₁(), the carrier' of F₁():] is non empty set
the of F₁() . G is Element of the carrier' of F₁()
[:NAT, the carrier' of F₁():] is Relation-like non empty V46() set
bool [:NAT, the carrier' of F₁():] is non empty V46() set
X is Relation-like NAT -defined the carrier' of F₁() -valued Function-like non empty total quasi_total Element of bool [:NAT, the carrier' of F₁():]
X . 0 is Element of the carrier' of F₁()
G is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() set
X . G is Element of the carrier' of F₁()
c₃ is Element of the carrier' of F₁()
G + 1 is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
X . (G + 1) is Element of the carrier' of F₁()
(F₁(),c₃) is Element of the carrier' of F₁()
the of F₁() is Relation-like the carrier' of F₁() -defined the carrier' of F₁() -valued Function-like non empty total quasi_total Element of bool [: the carrier' of F₁(), the carrier' of F₁():]
[: the carrier' of F₁(), the carrier' of F₁():] is Relation-like non empty set
bool [: the carrier' of F₁(), the carrier' of F₁():] is non empty set
the of F₁() . c₃ is Element of the carrier' of F₁()
G -' 0 is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
X . (G -' 0) is Element of the carrier' of F₁()
X2 is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() set
G -' X2 is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
X . (G -' X2) is Element of the carrier' of F₁()
X2 + 1 is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
G -' (X2 + 1) is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
(G -' X2) -' 1 is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
(G -' (X2 + 1)) + 1 is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
X . (G -' (X2 + 1)) is Element of the carrier' of F₁()
(F₁(),(X . (G -' (X2 + 1)))) is Element of the carrier' of F₁()
the of F₁() . (X . (G -' (X2 + 1))) is Element of the carrier' of F₁()
(F₁(),(X . (G -' (X2 + 1)))) is Element of the carrier of F₁()
the of F₁() is Relation-like the carrier' of F₁() -defined the carrier of F₁() -valued Function-like non empty total quasi_total Element of bool [: the carrier' of F₁(), the carrier of F₁():]
[: the carrier' of F₁(), the carrier of F₁():] is Relation-like non empty set
bool [: the carrier' of F₁(), the carrier of F₁():] is non empty set
the of F₁() . (X . (G -' (X2 + 1))) is Element of the carrier of F₁()
(F₁(),(X . (G -' X2)),(F₁(),(X . (G -' (X2 + 1))))) is Element of the carrier' of F₁()
the of F₁() is Relation-like [: the carrier of F₁(), the carrier' of F₁():] -defined the carrier' of F₁() -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of F₁(), the carrier' of F₁():], the carrier' of F₁():]
[: the carrier of F₁(), the carrier' of F₁():] is Relation-like non empty set
[:[: the carrier of F₁(), the carrier' of F₁():], the carrier' of F₁():] is Relation-like non empty set
bool [:[: the carrier of F₁(), the carrier' of F₁():], the carrier' of F₁():] is non empty set
the of F₁() . ((F₁(),(X . (G -' (X2 + 1)))),(X . (G -' X2))) is Element of the carrier' of F₁()
[(F₁(),(X . (G -' (X2 + 1)))),(X . (G -' X2))] is set
{(F₁(),(X . (G -' (X2 + 1)))),(X . (G -' X2))} is non empty set
{(F₁(),(X . (G -' (X2 + 1))))} is non empty trivial V53(1) set
{{(F₁(),(X . (G -' (X2 + 1)))),(X . (G -' X2))},{(F₁(),(X . (G -' (X2 + 1))))}} is non empty set
the of F₁() . [(F₁(),(X . (G -' (X2 + 1)))),(X . (G -' X2))] is set
0 + 1 is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
0 -' 1 is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
X . (G -' (X2 + 1)) is Element of the carrier' of F₁()
0 + 1 is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
G -' G is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
X . (G -' G) is Element of the carrier' of F₁()
F₁() is non empty non void V67() () () () () () ()
the carrier' of F₁() is non empty set
F₃() is non empty set
[: the carrier' of F₁(),F₃():] is Relation-like non empty set
bool [: the carrier' of F₁(),F₃():] is non empty set
F₂() is Element of the carrier' of F₁()
F₄() is Element of F₃()
the carrier of F₁() is non empty set
bool [: the carrier' of F₁(),F₃():] is non empty Element of bool (bool [: the carrier' of F₁(),F₃():])
bool (bool [: the carrier' of F₁(),F₃():]) is non empty set
X is set
G is Element of the carrier' of F₁()
[G,F₄()] is Element of [: the carrier' of F₁(),F₃():]
{G,F₄()} is non empty set
{G} is non empty trivial V53(1) set
{{G,F₄()},{G}} is non empty set
c₃ is Element of the carrier' of F₁()
A is Element of F₃()
[c₃,A] is Element of [: the carrier' of F₁(),F₃():]
{c₃,A} is non empty set
{c₃} is non empty trivial V53(1) set
{{c₃,A},{c₃}} is non empty set
X2 is Element of the carrier of F₁()
(F₁(),c₃,X2) is Element of the carrier' of F₁()
the of F₁() is Relation-like [: the carrier of F₁(), the carrier' of F₁():] -defined the carrier' of F₁() -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of F₁(), the carrier' of F₁():], the carrier' of F₁():]
[: the carrier of F₁(), the carrier' of F₁():] is Relation-like non empty set
[:[: the carrier of F₁(), the carrier' of F₁():], the carrier' of F₁():] is Relation-like non empty set
bool [:[: the carrier of F₁(), the carrier' of F₁():], the carrier' of F₁():] is non empty set
the of F₁() . (X2,c₃) is Element of the carrier' of F₁()
[X2,c₃] is set
{X2,c₃} is non empty set
{X2} is non empty trivial V53(1) set
{{X2,c₃},{X2}} is non empty set
the of F₁() . [X2,c₃] is set
F₅(X2,A) is Element of F₃()
[(F₁(),c₃,X2),F₅(X2,A)] is Element of [: the carrier' of F₁(),F₃():]
{(F₁(),c₃,X2),F₅(X2,A)} is non empty set
{(F₁(),c₃,X2)} is non empty trivial V53(1) set
{{(F₁(),c₃,X2),F₅(X2,A)},{(F₁(),c₃,X2)}} is non empty set
G is non empty set
meet G is set
X2 is Relation-like the carrier' of F₁() -defined F₃() -valued Element of bool [: the carrier' of F₁(),F₃():]
A is Element of the carrier' of F₁()
[A,F₄()] is Element of [: the carrier' of F₁(),F₃():]
{A,F₄()} is non empty set
{A} is non empty trivial V53(1) set
{{A,F₄()},{A}} is non empty set
s1 is set
A is Element of the carrier' of F₁()
s1 is Element of the carrier of F₁()
(F₁(),A,s1) is Element of the carrier' of F₁()
the of F₁() is Relation-like [: the carrier of F₁(), the carrier' of F₁():] -defined the carrier' of F₁() -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of F₁(), the carrier' of F₁():], the carrier' of F₁():]
[: the carrier of F₁(), the carrier' of F₁():] is Relation-like non empty set
[:[: the carrier of F₁(), the carrier' of F₁():], the carrier' of F₁():] is Relation-like non empty set
bool [:[: the carrier of F₁(), the carrier' of F₁():], the carrier' of F₁():] is non empty set
the of F₁() . (s1,A) is Element of the carrier' of F₁()
[s1,A] is set
{s1,A} is non empty set
{s1} is non empty trivial V53(1) set
{{s1,A},{s1}} is non empty set
the of F₁() . [s1,A] is set
s2 is Element of F₃()
[A,s2] is Element of [: the carrier' of F₁(),F₃():]
{A,s2} is non empty set
{A} is non empty trivial V53(1) set
{{A,s2},{A}} is non empty set
F₅(s1,s2) is Element of F₃()
[(F₁(),A,s1),F₅(s1,s2)] is Element of [: the carrier' of F₁(),F₃():]
{(F₁(),A,s1),F₅(s1,s2)} is non empty set
{(F₁(),A,s1)} is non empty trivial V53(1) set
{{(F₁(),A,s1),F₅(s1,s2)},{(F₁(),A,s1)}} is non empty set
e1 is set
e2 is Element of the carrier' of F₁()
[e2,F₄()] is Element of [: the carrier' of F₁(),F₃():]
{e2,F₄()} is non empty set
{e2} is non empty trivial V53(1) set
{{e2,F₄()},{e2}} is non empty set
q2 is Element of the carrier' of F₁()
e2 is Element of F₃()
[q2,e2] is Element of [: the carrier' of F₁(),F₃():]
{q2,e2} is non empty set
{q2} is non empty trivial V53(1) set
{{q2,e2},{q2}} is non empty set
e1 is Element of the carrier of F₁()
(F₁(),q2,e1) is Element of the carrier' of F₁()
the of F₁() . (e1,q2) is Element of the carrier' of F₁()
[e1,q2] is set
{e1,q2} is non empty set
{e1} is non empty trivial V53(1) set
{{e1,q2},{e1}} is non empty set
the of F₁() . [e1,q2] is set
F₅(e1,e2) is Element of F₃()
[(F₁(),q2,e1),F₅(e1,e2)] is Element of [: the carrier' of F₁(),F₃():]
{(F₁(),q2,e1),F₅(e1,e2)} is non empty set
{(F₁(),q2,e1)} is non empty trivial V53(1) set
{{(F₁(),q2,e1),F₅(e1,e2)},{(F₁(),q2,e1)}} is non empty set
A is Element of the carrier' of F₁()
s1 is Element of F₃()
[A,s1] is set
{A,s1} is non empty set
{A} is non empty trivial V53(1) set
{{A,s1},{A}} is non empty set
[A,F₄()] is Element of [: the carrier' of F₁(),F₃():]
{A,F₄()} is non empty set
{{A,F₄()},{A}} is non empty set
s2 is set
A is Element of the carrier' of F₁()
s1 is Element of the carrier of F₁()
(F₁(),A,s1) is Element of the carrier' of F₁()
the of F₁() is Relation-like [: the carrier of F₁(), the carrier' of F₁():] -defined the carrier' of F₁() -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of F₁(), the carrier' of F₁():], the carrier' of F₁():]
[: the carrier of F₁(), the carrier' of F₁():] is Relation-like non empty set
[:[: the carrier of F₁(), the carrier' of F₁():], the carrier' of F₁():] is Relation-like non empty set
bool [:[: the carrier of F₁(), the carrier' of F₁():], the carrier' of F₁():] is non empty set
the of F₁() . (s1,A) is Element of the carrier' of F₁()
[s1,A] is set
{s1,A} is non empty set
{s1} is non empty trivial V53(1) set
{{s1,A},{s1}} is non empty set
the of F₁() . [s1,A] is set
s2 is set
[A,s2] is set
{A,s2} is non empty set
{A} is non empty trivial V53(1) set
{{A,s2},{A}} is non empty set
e1 is Element of F₃()
F₅(s1,e1) is Element of F₃()
e2 is Element of F₃()
[(F₁(),A,s1),e2] is set
{(F₁(),A,s1),e2} is non empty set
{(F₁(),A,s1)} is non empty trivial V53(1) set
{{(F₁(),A,s1),e2},{(F₁(),A,s1)}} is non empty set
q2 is set
[A,e1] is Element of [: the carrier' of F₁(),F₃():]
{A,e1} is non empty set
{{A,e1},{A}} is non empty set
[(F₁(),A,s1),e2] is Element of [: the carrier' of F₁(),F₃():]
A is Element of the carrier' of F₁()
s1 is set
[A,s1] is set
{A,s1} is non empty set
{A} is non empty trivial V53(1) set
{{A,s1},{A}} is non empty set
s2 is set
[A,s2] is set
{A,s2} is non empty set
{{A,s2},{A}} is non empty set
{[A,s1]} is Relation-like Function-like constant non empty trivial V53(1) set
X2 \ {[A,s1]} is Relation-like the carrier' of F₁() -defined F₃() -valued Element of bool [: the carrier' of F₁(),F₃():]
{[A,s2]} is Relation-like Function-like constant non empty trivial V53(1) set
X2 \ {[A,s2]} is Relation-like the carrier' of F₁() -defined F₃() -valued Element of bool [: the carrier' of F₁(),F₃():]
q2 is Element of the carrier' of F₁()
[q2,F₄()] is Element of [: the carrier' of F₁(),F₃():]
{q2,F₄()} is non empty set
{q2} is non empty trivial V53(1) set
{{q2,F₄()},{q2}} is non empty set
q2 is Element of the carrier' of F₁()
e1 is Element of the carrier of F₁()
(F₁(),q2,e1) is Element of the carrier' of F₁()
the of F₁() is Relation-like [: the carrier of F₁(), the carrier' of F₁():] -defined the carrier' of F₁() -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of F₁(), the carrier' of F₁():], the carrier' of F₁():]
[: the carrier of F₁(), the carrier' of F₁():] is Relation-like non empty set
[:[: the carrier of F₁(), the carrier' of F₁():], the carrier' of F₁():] is Relation-like non empty set
bool [:[: the carrier of F₁(), the carrier' of F₁():], the carrier' of F₁():] is non empty set
the of F₁() . (e1,q2) is Element of the carrier' of F₁()
[e1,q2] is set
{e1,q2} is non empty set
{e1} is non empty trivial V53(1) set
{{e1,q2},{e1}} is non empty set
the of F₁() . [e1,q2] is set
e2 is Element of F₃()
[q2,e2] is Element of [: the carrier' of F₁(),F₃():]
{q2,e2} is non empty set
{q2} is non empty trivial V53(1) set
{{q2,e2},{q2}} is non empty set
F₅(e1,e2) is Element of F₃()
[(F₁(),q2,e1),F₅(e1,e2)] is Element of [: the carrier' of F₁(),F₃():]
{(F₁(),q2,e1),F₅(e1,e2)} is non empty set
{(F₁(),q2,e1)} is non empty trivial V53(1) set
{{(F₁(),q2,e1),F₅(e1,e2)},{(F₁(),q2,e1)}} is non empty set
q2 is Element of the carrier' of F₁()
[q2,F₄()] is Element of [: the carrier' of F₁(),F₃():]
{q2,F₄()} is non empty set
{q2} is non empty trivial V53(1) set
{{q2,F₄()},{q2}} is non empty set
q2 is Element of the carrier' of F₁()
e1 is Element of the carrier of F₁()
(F₁(),q2,e1) is Element of the carrier' of F₁()
the of F₁() is Relation-like [: the carrier of F₁(), the carrier' of F₁():] -defined the carrier' of F₁() -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of F₁(), the carrier' of F₁():], the carrier' of F₁():]
[: the carrier of F₁(), the carrier' of F₁():] is Relation-like non empty set
[:[: the carrier of F₁(), the carrier' of F₁():], the carrier' of F₁():] is Relation-like non empty set
bool [:[: the carrier of F₁(), the carrier' of F₁():], the carrier' of F₁():] is non empty set
the of F₁() . (e1,q2) is Element of the carrier' of F₁()
[e1,q2] is set
{e1,q2} is non empty set
{e1} is non empty trivial V53(1) set
{{e1,q2},{e1}} is non empty set
the of F₁() . [e1,q2] is set
e2 is Element of F₃()
[q2,e2] is Element of [: the carrier' of F₁(),F₃():]
{q2,e2} is non empty set
{q2} is non empty trivial V53(1) set
{{q2,e2},{q2}} is non empty set
F₅(e1,e2) is Element of F₃()
[(F₁(),q2,e1),F₅(e1,e2)] is Element of [: the carrier' of F₁(),F₃():]
{(F₁(),q2,e1),F₅(e1,e2)} is non empty set
{(F₁(),q2,e1)} is non empty trivial V53(1) set
{{(F₁(),q2,e1),F₅(e1,e2)},{(F₁(),q2,e1)}} is non empty set
A is Element of the carrier' of F₁()
s1 is Element of the carrier of F₁()
(F₁(),A,s1) is Element of the carrier' of F₁()
the of F₁() is Relation-like [: the carrier of F₁(), the carrier' of F₁():] -defined the carrier' of F₁() -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of F₁(), the carrier' of F₁():], the carrier' of F₁():]
[: the carrier of F₁(), the carrier' of F₁():] is Relation-like non empty set
[:[: the carrier of F₁(), the carrier' of F₁():], the carrier' of F₁():] is Relation-like non empty set
bool [:[: the carrier of F₁(), the carrier' of F₁():], the carrier' of F₁():] is non empty set
the of F₁() . (s1,A) is Element of the carrier' of F₁()
[s1,A] is set
{s1,A} is non empty set
{s1} is non empty trivial V53(1) set
{{s1,A},{s1}} is non empty set
the of F₁() . [s1,A] is set
s2 is set
[(F₁(),A,s1),s2] is set
{(F₁(),A,s1),s2} is non empty set
{(F₁(),A,s1)} is non empty trivial V53(1) set
{{(F₁(),A,s1),s2},{(F₁(),A,s1)}} is non empty set
e1 is set
[(F₁(),A,s1),e1] is set
{(F₁(),A,s1),e1} is non empty set
{{(F₁(),A,s1),e1},{(F₁(),A,s1)}} is non empty set
e2 is set
[A,e2] is set
{A,e2} is non empty set
{A} is non empty trivial V53(1) set
{{A,e2},{A}} is non empty set
e2 is set
[A,e2] is set
{A,e2} is non empty set
{A} is non empty trivial V53(1) set
{{A,e2},{A}} is non empty set
{[(F₁(),A,s1),s2]} is Relation-like Function-like constant non empty trivial V53(1) set
X2 \ {[(F₁(),A,s1),s2]} is Relation-like the carrier' of F₁() -defined F₃() -valued Element of bool [: the carrier' of F₁(),F₃():]
{[(F₁(),A,s1),e1]} is Relation-like Function-like constant non empty trivial V53(1) set
X2 \ {[(F₁(),A,s1),e1]} is Relation-like the carrier' of F₁() -defined F₃() -valued Element of bool [: the carrier' of F₁(),F₃():]
q2 is Element of F₃()
F₅(s1,q2) is Element of F₃()
e3 is Element of the carrier' of F₁()
[e3,F₄()] is Element of [: the carrier' of F₁(),F₃():]
{e3,F₄()} is non empty set
{e3} is non empty trivial V53(1) set
{{e3,F₄()},{e3}} is non empty set
e3 is Element of the carrier' of F₁()
a is Element of the carrier of F₁()
(F₁(),e3,a) is Element of the carrier' of F₁()
the of F₁() . (a,e3) is Element of the carrier' of F₁()
[a,e3] is set
{a,e3} is non empty set
{a} is non empty trivial V53(1) set
{{a,e3},{a}} is non empty set
the of F₁() . [a,e3] is set
v is Element of F₃()
[e3,v] is Element of [: the carrier' of F₁(),F₃():]
{e3,v} is non empty set
{e3} is non empty trivial V53(1) set
{{e3,v},{e3}} is non empty set
F₅(a,v) is Element of F₃()
[(F₁(),e3,a),F₅(a,v)] is Element of [: the carrier' of F₁(),F₃():]
{(F₁(),e3,a),F₅(a,v)} is non empty set
{(F₁(),e3,a)} is non empty trivial V53(1) set
{{(F₁(),e3,a),F₅(a,v)},{(F₁(),e3,a)}} is non empty set
e3 is Element of the carrier' of F₁()
[e3,F₄()] is Element of [: the carrier' of F₁(),F₃():]
{e3,F₄()} is non empty set
{e3} is non empty trivial V53(1) set
{{e3,F₄()},{e3}} is non empty set
e3 is Element of the carrier' of F₁()
a is Element of the carrier of F₁()
(F₁(),e3,a) is Element of the carrier' of F₁()
the of F₁() . (a,e3) is Element of the carrier' of F₁()
[a,e3] is set
{a,e3} is non empty set
{a} is non empty trivial V53(1) set
{{a,e3},{a}} is non empty set
the of F₁() . [a,e3] is set
v is Element of F₃()
[e3,v] is Element of [: the carrier' of F₁(),F₃():]
{e3,v} is non empty set
{e3} is non empty trivial V53(1) set
{{e3,v},{e3}} is non empty set
F₅(a,v) is Element of F₃()
[(F₁(),e3,a),F₅(a,v)] is Element of [: the carrier' of F₁(),F₃():]
{(F₁(),e3,a),F₅(a,v)} is non empty set
{(F₁(),e3,a)} is non empty trivial V53(1) set
{{(F₁(),e3,a),F₅(a,v)},{(F₁(),e3,a)}} is non empty set
A is set
s1 is set
[A,s1] is set
{A,s1} is non empty set
{A} is non empty trivial V53(1) set
{{A,s1},{A}} is non empty set
s2 is set
[A,s2] is set
{A,s2} is non empty set
{{A,s2},{A}} is non empty set
e1 is Element of the carrier' of F₁()
dom X2 is Element of bool the carrier' of F₁()
bool the carrier' of F₁() is non empty set
A is set
s1 is Element of the carrier' of F₁()
s2 is set
[s1,s2] is set
{s1,s2} is non empty set
{s1} is non empty trivial V53(1) set
{{s1,s2},{s1}} is non empty set
A is Relation-like the carrier' of F₁() -defined F₃() -valued Function-like non empty total quasi_total Element of bool [: the carrier' of F₁(),F₃():]
A . F₂() is Element of F₃()
s1 is Element of F₃()
s2 is Element of the carrier' of F₁()
[s2,F₄()] is Element of [: the carrier' of F₁(),F₃():]
{s2,F₄()} is non empty set
{s2} is non empty trivial V53(1) set
{{s2,F₄()},{s2}} is non empty set
A . s2 is Element of F₃()
s2 is Element of the carrier' of F₁()
A . s2 is Element of F₃()
e1 is Element of the carrier of F₁()
(F₁(),s2,e1) is Element of the carrier' of F₁()
the of F₁() is Relation-like [: the carrier of F₁(), the carrier' of F₁():] -defined the carrier' of F₁() -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of F₁(), the carrier' of F₁():], the carrier' of F₁():]
[: the carrier of F₁(), the carrier' of F₁():] is Relation-like non empty set
[:[: the carrier of F₁(), the carrier' of F₁():], the carrier' of F₁():] is Relation-like non empty set
bool [:[: the carrier of F₁(), the carrier' of F₁():], the carrier' of F₁():] is non empty set
the of F₁() . (e1,s2) is Element of the carrier' of F₁()
[e1,s2] is set
{e1,s2} is non empty set
{e1} is non empty trivial V53(1) set
{{e1,s2},{e1}} is non empty set
the of F₁() . [e1,s2] is set
A . (F₁(),s2,e1) is Element of F₃()
F₅(e1,(A . s2)) is Element of F₃()
dom A is non empty Element of bool the carrier' of F₁()
bool the carrier' of F₁() is non empty set
[s2,(A . s2)] is Element of [: the carrier' of F₁(),F₃():]
{s2,(A . s2)} is non empty set
{s2} is non empty trivial V53(1) set
{{s2,(A . s2)},{s2}} is non empty set
[(F₁(),s2,e1),F₅(e1,(A . s2))] is Element of [: the carrier' of F₁(),F₃():]
{(F₁(),s2,e1),F₅(e1,(A . s2))} is non empty set
{(F₁(),s2,e1)} is non empty trivial V53(1) set
{{(F₁(),s2,e1),F₅(e1,(A . s2))},{(F₁(),s2,e1)}} is non empty set
F₁() is non empty non void V67() () () () () () ()
the carrier' of F₁() is non empty set
F₃() is non empty set
[: the carrier' of F₁(),F₃():] is Relation-like non empty set
bool [: the carrier' of F₁(),F₃():] is non empty set
F₂() is Element of the carrier' of F₁()
F₄() is Element of F₃()
the carrier of F₁() is non empty set
X is Element of F₃()
G is Element of F₃()
c₃ is Relation-like the carrier' of F₁() -defined F₃() -valued Function-like non empty total quasi_total Element of bool [: the carrier' of F₁(),F₃():]
c₃ . F₂() is Element of F₃()
X2 is Relation-like the carrier' of F₁() -defined F₃() -valued Function-like non empty total quasi_total Element of bool [: the carrier' of F₁(),F₃():]
X2 . F₂() is Element of F₃()
A is Element of the carrier' of F₁()
c₃ . A is Element of F₃()
X2 . A is Element of F₃()
A is Element of the carrier' of F₁()
c₃ . A is Element of F₃()
X2 . A is Element of F₃()
s1 is Element of the carrier of F₁()
(F₁(),A,s1) is Element of the carrier' of F₁()
the of F₁() is Relation-like [: the carrier of F₁(), the carrier' of F₁():] -defined the carrier' of F₁() -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of F₁(), the carrier' of F₁():], the carrier' of F₁():]
[: the carrier of F₁(), the carrier' of F₁():] is Relation-like non empty set
[:[: the carrier of F₁(), the carrier' of F₁():], the carrier' of F₁():] is Relation-like non empty set
bool [:[: the carrier of F₁(), the carrier' of F₁():], the carrier' of F₁():] is non empty set
the of F₁() . (s1,A) is Element of the carrier' of F₁()
[s1,A] is set
{s1,A} is non empty set
{s1} is non empty trivial V53(1) set
{{s1,A},{s1}} is non empty set
the of F₁() . [s1,A] is set
c₃ . (F₁(),A,s1) is Element of F₃()
F₅(s1,(X2 . A)) is Element of F₃()
X2 . (F₁(),A,s1) is Element of F₃()
X is non empty non void V67() () () () () () ()
the carrier' of X is non empty set
the carrier of X is non empty set
the carrier of X * is functional non empty FinSequence-membered M16( the carrier of X)
[: the carrier' of X,( the carrier of X *):] is Relation-like non empty set
bool [: the carrier' of X,( the carrier of X *):] is non empty set
G is Element of the carrier' of X
<*> the carrier of X is Relation-like non-empty empty-yielding NAT -defined the carrier of X -valued Function-like one-to-one constant functional empty proper ext-real non positive non negative irreflexive V39() V40() V41() V43() V44() V45() V46() V51() V53( {} ) FinSequence-like FinSubsequence-like FinSequence-membered co-well_founded weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V110() V246() FinSequence of the carrier of X
[:NAT, the carrier of X:] is Relation-like non empty V46() set
c₃ is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
X2 is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
A is Relation-like the carrier' of X -defined the carrier of X * -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X,( the carrier of X *):]
A . G is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
<*> the carrier of X is Relation-like non-empty empty-yielding NAT -defined the carrier of X -valued Function-like one-to-one constant functional empty proper ext-real non positive non negative irreflexive V39() V40() V41() V43() V44() V45() V46() V51() V53( {} ) FinSequence-like FinSubsequence-like FinSequence-membered co-well_founded weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V110() V246() FinSequence of the carrier of X
[:NAT, the carrier of X:] is Relation-like non empty V46() set
c₃ is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
X2 is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
s1 is Relation-like the carrier' of X -defined the carrier of X * -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X,( the carrier of X *):]
s1 . G is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
A is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
s2 is Relation-like the carrier' of X -defined the carrier of X * -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X,( the carrier of X *):]
s2 . G is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
X is non empty non void V67() () () () () () ()
the carrier' of X is non empty set
G is Element of the carrier' of X
(X,G) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
the carrier of X is non empty set
the carrier of X * is functional non empty FinSequence-membered M16( the carrier of X)
[: the carrier' of X,( the carrier of X *):] is Relation-like non empty set
bool [: the carrier' of X,( the carrier of X *):] is non empty set
c₃ is Relation-like the carrier' of X -defined the carrier of X * -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X,( the carrier of X *):]
c₃ . G is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
X is non empty non void V67() () () () () () ()
the carrier' of X is non empty set
the carrier of X is non empty set
G is Element of the carrier' of X
(X,G) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
the carrier of X * is functional non empty FinSequence-membered M16( the carrier of X)
(X,G) is Element of the carrier of X
the of X is Relation-like the carrier' of X -defined the carrier of X -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X, the carrier of X:]
[: the carrier' of X, the carrier of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier of X:] is non empty set
the of X . G is Element of the carrier of X
<*(X,G)*> is Relation-like NAT -defined the carrier of X -valued Function-like constant non empty trivial V46() V53(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of X
[1,(X,G)] is set
{1,(X,G)} is non empty set
{1} is non empty trivial V53(1) set
{{1,(X,G)},{1}} is non empty set
{[1,(X,G)]} is Relation-like Function-like constant non empty trivial V53(1) set
(X,G) is Element of the carrier' of X
the of X is Relation-like the carrier' of X -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X, the carrier' of X:]
[: the carrier' of X, the carrier' of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier' of X:] is non empty set
the of X . G is Element of the carrier' of X
(X,(X,G)) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
( the carrier of X,<*(X,G)*>,(X,(X,G))) is Relation-like NAT -defined the carrier of X -valued Function-like non empty V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
[: the carrier' of X,( the carrier of X *):] is Relation-like non empty set
bool [: the carrier' of X,( the carrier of X *):] is non empty set
c₃ is Relation-like the carrier' of X -defined the carrier of X * -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X,( the carrier of X *):]
c₃ . G is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
c₃ . (X,G) is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
(X,(X,G),(X,G)) is Element of the carrier' of X
the of X is Relation-like [: the carrier of X, the carrier' of X:] -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of X, the carrier' of X:], the carrier' of X:]
[: the carrier of X, the carrier' of X:] is Relation-like non empty set
[:[: the carrier of X, the carrier' of X:], the carrier' of X:] is Relation-like non empty set
bool [:[: the carrier of X, the carrier' of X:], the carrier' of X:] is non empty set
the of X . ((X,G),(X,G)) is Element of the carrier' of X
[(X,G),(X,G)] is set
{(X,G),(X,G)} is non empty set
{(X,G)} is non empty trivial V53(1) set
{{(X,G),(X,G)},{(X,G)}} is non empty set
the of X . [(X,G),(X,G)] is set
X is non empty non void V67() () () () () () ()
the carrier' of X is non empty set
the carrier of X is non empty set
G is Element of the carrier' of X
(X,G) is Element of the carrier' of X
the of X is Relation-like the carrier' of X -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X, the carrier' of X:]
[: the carrier' of X, the carrier' of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier' of X:] is non empty set
the of X . G is Element of the carrier' of X
(X,(X,G)) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
the carrier of X * is functional non empty FinSequence-membered M16( the carrier of X)
(X,G) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
( the carrier of X,1,(X,G)) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
(X,G) is Element of the carrier of X
the of X is Relation-like the carrier' of X -defined the carrier of X -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X, the carrier of X:]
[: the carrier' of X, the carrier of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier of X:] is non empty set
the of X . G is Element of the carrier of X
<*(X,G)*> is Relation-like NAT -defined the carrier of X -valued Function-like constant non empty trivial V46() V53(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of X
[1,(X,G)] is set
{1,(X,G)} is non empty set
{1} is non empty trivial V53(1) set
{{1,(X,G)},{1}} is non empty set
{[1,(X,G)]} is Relation-like Function-like constant non empty trivial V53(1) set
( the carrier of X,<*(X,G)*>,(X,(X,G))) is Relation-like NAT -defined the carrier of X -valued Function-like non empty V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
X is non empty non void V67() () () () () () ()
the carrier' of X is non empty set
the carrier of X is non empty set
G is Element of the carrier' of X
(X,G) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
the carrier of X * is functional non empty FinSequence-membered M16( the carrier of X)
c₃ is Element of the carrier of X
(X,G,c₃) is Element of the carrier' of X
the of X is Relation-like [: the carrier of X, the carrier' of X:] -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of X, the carrier' of X:], the carrier' of X:]
[: the carrier of X, the carrier' of X:] is Relation-like non empty set
[:[: the carrier of X, the carrier' of X:], the carrier' of X:] is Relation-like non empty set
bool [:[: the carrier of X, the carrier' of X:], the carrier' of X:] is non empty set
the of X . (c₃,G) is Element of the carrier' of X
[c₃,G] is set
{c₃,G} is non empty set
{c₃} is non empty trivial V53(1) set
{{c₃,G},{c₃}} is non empty set
the of X . [c₃,G] is set
(X,(X,G,c₃)) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
<*c₃*> is Relation-like NAT -defined the carrier of X -valued Function-like constant non empty trivial V46() V53(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of X
[1,c₃] is set
{1,c₃} is non empty set
{1} is non empty trivial V53(1) set
{{1,c₃},{1}} is non empty set
{[1,c₃]} is Relation-like Function-like constant non empty trivial V53(1) set
( the carrier of X,<*c₃*>,(X,G)) is Relation-like NAT -defined the carrier of X -valued Function-like non empty V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
(X,(X,G,c₃)) is Element of the carrier of X
the of X is Relation-like the carrier' of X -defined the carrier of X -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X, the carrier of X:]
[: the carrier' of X, the carrier of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier of X:] is non empty set
the of X . (X,G,c₃) is Element of the carrier of X
<*(X,(X,G,c₃))*> is Relation-like NAT -defined the carrier of X -valued Function-like constant non empty trivial V46() V53(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of X
[1,(X,(X,G,c₃))] is set
{1,(X,(X,G,c₃))} is non empty set
{{1,(X,(X,G,c₃))},{1}} is non empty set
{[1,(X,(X,G,c₃))]} is Relation-like Function-like constant non empty trivial V53(1) set
(X,(X,G,c₃)) is Element of the carrier' of X
the of X is Relation-like the carrier' of X -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X, the carrier' of X:]
[: the carrier' of X, the carrier' of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier' of X:] is non empty set
the of X . (X,G,c₃) is Element of the carrier' of X
(X,(X,(X,G,c₃))) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
( the carrier of X,<*(X,(X,G,c₃))*>,(X,(X,(X,G,c₃)))) is Relation-like NAT -defined the carrier of X -valued Function-like non empty V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
( the carrier of X,<*c₃*>,(X,(X,(X,G,c₃)))) is Relation-like NAT -defined the carrier of X -valued Function-like non empty V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
X is non empty non void V67() () () () () () ()
the carrier' of X is non empty set
G is Element of the carrier' of X
(X,G) is Element of the carrier of X
the carrier of X is non empty set
the of X is Relation-like the carrier' of X -defined the carrier of X -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X, the carrier of X:]
[: the carrier' of X, the carrier of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier of X:] is non empty set
the of X . G is Element of the carrier of X
(X,G) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
the carrier of X * is functional non empty FinSequence-membered M16( the carrier of X)
(X,G) . 1 is set
<*(X,G)*> is Relation-like NAT -defined the carrier of X -valued Function-like constant non empty trivial V46() V53(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of X
[1,(X,G)] is set
{1,(X,G)} is non empty set
{1} is non empty trivial V53(1) set
{{1,(X,G)},{1}} is non empty set
{[1,(X,G)]} is Relation-like Function-like constant non empty trivial V53(1) set
(X,G) is Element of the carrier' of X
the of X is Relation-like the carrier' of X -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X, the carrier' of X:]
[: the carrier' of X, the carrier' of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier' of X:] is non empty set
the of X . G is Element of the carrier' of X
(X,(X,G)) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
( the carrier of X,<*(X,G)*>,(X,(X,G))) is Relation-like NAT -defined the carrier of X -valued Function-like non empty V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
X is non empty non void V67() () () () () () ()
the carrier' of X is non empty set
G is Element of the carrier' of X
(X,G) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
the carrier of X is non empty set
the carrier of X * is functional non empty FinSequence-membered M16( the carrier of X)
(X,G) is Element of the carrier of X
the of X is Relation-like the carrier' of X -defined the carrier of X -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X, the carrier of X:]
[: the carrier' of X, the carrier of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier of X:] is non empty set
the of X . G is Element of the carrier of X
<*(X,G)*> is Relation-like NAT -defined the carrier of X -valued Function-like constant non empty trivial V46() V53(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of X
[1,(X,G)] is set
{1,(X,G)} is non empty set
{1} is non empty trivial V53(1) set
{{1,(X,G)},{1}} is non empty set
{[1,(X,G)]} is Relation-like Function-like constant non empty trivial V53(1) set
(X,G) is Element of the carrier' of X
the of X is Relation-like the carrier' of X -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X, the carrier' of X:]
[: the carrier' of X, the carrier' of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier' of X:] is non empty set
the of X . G is Element of the carrier' of X
(X,(X,G)) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
( the carrier of X,<*(X,G)*>,(X,(X,G))) is Relation-like NAT -defined the carrier of X -valued Function-like non empty V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
X is non empty set
(X) is non empty non void V67() () () () () () () ()
the carrier' of (X) is functional non empty set
G is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier' of (X)
((X),G) is Relation-like NAT -defined the carrier of (X) -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of (X) *
the carrier of (X) is non empty set
the carrier of (X) * is functional non empty FinSequence-membered M16( the carrier of (X))
G is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier' of (X)
((X),G) is Relation-like NAT -defined the carrier of (X) -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of (X) *
c₃ is Element of the carrier of (X)
((X),G,c₃) is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier' of (X)
the of (X) is Relation-like [: the carrier of (X), the carrier' of (X):] -defined the carrier' of (X) -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of (X), the carrier' of (X):], the carrier' of (X):]
[: the carrier of (X), the carrier' of (X):] is Relation-like non empty set
[:[: the carrier of (X), the carrier' of (X):], the carrier' of (X):] is Relation-like non empty set
bool [:[: the carrier of (X), the carrier' of (X):], the carrier' of (X):] is non empty set
the of (X) . (c₃,G) is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier' of (X)
[c₃,G] is set
{c₃,G} is non empty set
{c₃} is non empty trivial V53(1) set
{{c₃,G},{c₃}} is non empty set
the of (X) . [c₃,G] is Relation-like Function-like set
((X),((X),G,c₃)) is Relation-like NAT -defined the carrier of (X) -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of (X) *
<*c₃*> is Relation-like NAT -defined the carrier of (X) -valued Function-like constant non empty trivial V46() V53(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of (X)
[1,c₃] is set
{1,c₃} is non empty set
{1} is non empty trivial V53(1) set
{{1,c₃},{1}} is non empty set
{[1,c₃]} is Relation-like Function-like constant non empty trivial V53(1) set
<*c₃*> ^ G is Relation-like NAT -defined Function-like non empty V46() FinSequence-like FinSubsequence-like set
G is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier' of (X)
((X),G) is Relation-like NAT -defined the carrier of (X) -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of (X) *
X is non empty non void V67() () () () () () ()
the carrier of X is non empty set
the carrier of X * is functional non empty FinSequence-membered M16( the carrier of X)
the carrier' of X is non empty set
<*> the carrier of X is Relation-like non-empty empty-yielding NAT -defined the carrier of X -valued Function-like one-to-one constant functional empty proper ext-real non positive non negative irreflexive V39() V40() V41() V43() V44() V45() V46() V51() V53( {} ) FinSequence-like FinSubsequence-like FinSequence-membered co-well_founded weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V110() V246() FinSequence of the carrier of X
[:NAT, the carrier of X:] is Relation-like non empty V46() set
c₃ is Element of the carrier' of X
(X,c₃) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
c₃ is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of X
X2 is Element of the carrier of X
<*X2*> is Relation-like NAT -defined the carrier of X -valued Function-like constant non empty trivial V46() V53(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of X
[1,X2] is set
{1,X2} is non empty set
{1} is non empty trivial V53(1) set
{{1,X2},{1}} is non empty set
{[1,X2]} is Relation-like Function-like constant non empty trivial V53(1) set
( the carrier of X,<*X2*>,c₃) is Relation-like NAT -defined the carrier of X -valued Function-like non empty V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
A is Element of the carrier' of X
(X,A) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
(X,A,X2) is Element of the carrier' of X
the of X is Relation-like [: the carrier of X, the carrier' of X:] -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of X, the carrier' of X:], the carrier' of X:]
[: the carrier of X, the carrier' of X:] is Relation-like non empty set
[:[: the carrier of X, the carrier' of X:], the carrier' of X:] is Relation-like non empty set
bool [:[: the carrier of X, the carrier' of X:], the carrier' of X:] is non empty set
the of X . (X2,A) is Element of the carrier' of X
[X2,A] is set
{X2,A} is non empty set
{X2} is non empty trivial V53(1) set
{{X2,A},{X2}} is non empty set
the of X . [X2,A] is set
s1 is Element of the carrier' of X
(X,s1) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
c₃ is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
X is non empty non void V67() () () () () () ()
the carrier' of X is non empty set
X2 is Element of the carrier' of X
(X,X2) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
the carrier of X is non empty set
the carrier of X * is functional non empty FinSequence-membered M16( the carrier of X)
X2 is Element of the carrier' of X
(X,X2) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
the carrier of X is non empty set
the carrier of X * is functional non empty FinSequence-membered M16( the carrier of X)
A is Element of the carrier' of X
(X,A) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
X is non empty non void V67() () () () () () ()
the carrier' of X is non empty set
G is Element of the carrier' of X
c₃ is Element of the carrier' of X
X2 is Element of the carrier' of X
(X,G) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
the carrier of X is non empty set
the carrier of X * is functional non empty FinSequence-membered M16( the carrier of X)
(X,c₃) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
(X,X2) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
X is non empty non void V67() () () () () () ()
the carrier' of X is non empty set
G is Element of the carrier' of X
c₃ is Element of the carrier' of X
(X,G) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
the carrier of X is non empty set
the carrier of X * is functional non empty FinSequence-membered M16( the carrier of X)
(X,c₃) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
(X,c₃) is Element of the carrier of X
the of X is Relation-like the carrier' of X -defined the carrier of X -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X, the carrier of X:]
[: the carrier' of X, the carrier of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier of X:] is non empty set
the of X . c₃ is Element of the carrier of X
<*(X,c₃)*> is Relation-like NAT -defined the carrier of X -valued Function-like constant non empty trivial V46() V53(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of X
[1,(X,c₃)] is set
{1,(X,c₃)} is non empty set
{1} is non empty trivial V53(1) set
{{1,(X,c₃)},{1}} is non empty set
{[1,(X,c₃)]} is Relation-like Function-like constant non empty trivial V53(1) set
(X,c₃) is Element of the carrier' of X
the of X is Relation-like the carrier' of X -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X, the carrier' of X:]
[: the carrier' of X, the carrier' of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier' of X:] is non empty set
the of X . c₃ is Element of the carrier' of X
(X,(X,c₃)) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
( the carrier of X,<*(X,c₃)*>,(X,(X,c₃))) is Relation-like NAT -defined the carrier of X -valued Function-like non empty V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
X is non empty non void V67() () () () () () ()
the carrier' of X is non empty set
G is Element of the carrier' of X
c₃ is Element of the carrier' of X
(X,G) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
the carrier of X is non empty set
the carrier of X * is functional non empty FinSequence-membered M16( the carrier of X)
(X,c₃) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
X is non empty non void V67() () () () () () ()
the carrier' of X is non empty set
the carrier of X is non empty set
G is Element of the carrier' of X
c₃ is Element of the carrier' of X
X2 is Element of the carrier of X
(X,G,X2) is Element of the carrier' of X
the of X is Relation-like [: the carrier of X, the carrier' of X:] -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of X, the carrier' of X:], the carrier' of X:]
[: the carrier of X, the carrier' of X:] is Relation-like non empty set
[:[: the carrier of X, the carrier' of X:], the carrier' of X:] is Relation-like non empty set
bool [:[: the carrier of X, the carrier' of X:], the carrier' of X:] is non empty set
the of X . (X2,G) is Element of the carrier' of X
[X2,G] is set
{X2,G} is non empty set
{X2} is non empty trivial V53(1) set
{{X2,G},{X2}} is non empty set
the of X . [X2,G] is set
(X,c₃,X2) is Element of the carrier' of X
the of X . (X2,c₃) is Element of the carrier' of X
[X2,c₃] is set
{X2,c₃} is non empty set
{{X2,c₃},{X2}} is non empty set
the of X . [X2,c₃] is set
(X,G) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
the carrier of X * is functional non empty FinSequence-membered M16( the carrier of X)
(X,c₃) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
(X,(X,G,X2)) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
<*X2*> is Relation-like NAT -defined the carrier of X -valued Function-like constant non empty trivial V46() V53(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of X
[1,X2] is set
{1,X2} is non empty set
{1} is non empty trivial V53(1) set
{{1,X2},{1}} is non empty set
{[1,X2]} is Relation-like Function-like constant non empty trivial V53(1) set
( the carrier of X,<*X2*>,(X,c₃)) is Relation-like NAT -defined the carrier of X -valued Function-like non empty V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
(X,(X,c₃,X2)) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
X is non empty non void V67() () () () () () ()
the carrier' of X is non empty set
G is Element of the carrier' of X
(X,G) is Element of the carrier' of X
the of X is Relation-like the carrier' of X -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X, the carrier' of X:]
[: the carrier' of X, the carrier' of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier' of X:] is non empty set
the of X . G is Element of the carrier' of X
c₃ is Element of the carrier' of X
(X,c₃) is Element of the carrier' of X
the of X . c₃ is Element of the carrier' of X
(X,G) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
the carrier of X is non empty set
the carrier of X * is functional non empty FinSequence-membered M16( the carrier of X)
(X,c₃) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
(X,(X,G)) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
( the carrier of X,1,(X,G)) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
(X,(X,c₃)) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
X is non empty non void V67() () () () () () ()
the carrier' of X is non empty set
G is Element of the carrier' of X
(X,G) is Element of the carrier of X
the carrier of X is non empty set
the of X is Relation-like the carrier' of X -defined the carrier of X -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X, the carrier of X:]
[: the carrier' of X, the carrier of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier of X:] is non empty set
the of X . G is Element of the carrier of X
c₃ is Element of the carrier' of X
(X,c₃) is Element of the carrier of X
the of X . c₃ is Element of the carrier of X
(X,G) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
the carrier of X * is functional non empty FinSequence-membered M16( the carrier of X)
(X,c₃) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
(X,G) . 1 is set
X is non empty set
(X) is non empty non void V67() () () () () () () ()
the carrier' of (X) is functional non empty set
c₃ is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier' of (X)
X2 is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier' of (X)
((X),c₃) is Relation-like NAT -defined the carrier of (X) -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of (X) *
the carrier of (X) is non empty set
the carrier of (X) * is functional non empty FinSequence-membered M16( the carrier of (X))
((X),X2) is Relation-like NAT -defined the carrier of (X) -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of (X) *
X is non empty non void V67() () () () () () ()
the carrier' of X is non empty set
[: the carrier' of X, the carrier' of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier' of X:] is non empty set
G is Relation-like the carrier' of X -defined the carrier' of X -valued Element of bool [: the carrier' of X, the carrier' of X:]
c₃ is Relation-like the carrier' of X -defined the carrier' of X -valued Element of bool [: the carrier' of X, the carrier' of X:]
X is non empty non void V67() () () () () () ()
the carrier' of X is non empty set
(X) is Relation-like the carrier' of X -defined the carrier' of X -valued Element of bool [: the carrier' of X, the carrier' of X:]
[: the carrier' of X, the carrier' of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier' of X:] is non empty set
dom (X) is Element of bool the carrier' of X
bool the carrier' of X is non empty set
c₃ is set
X2 is Element of the carrier' of X
[X2,X2] is Element of [: the carrier' of X, the carrier' of X:]
{X2,X2} is non empty set
{X2} is non empty trivial V53(1) set
{{X2,X2},{X2}} is non empty set
field (X) is set
dom (X) is set
rng (X) is set
(dom (X)) \/ (rng (X)) is set
rng (X) is Element of bool the carrier' of X
(dom (X)) \/ (rng (X)) is Element of bool the carrier' of X
c₃ is set
X2 is set
[c₃,X2] is set
{c₃,X2} is non empty set
{c₃} is non empty trivial V53(1) set
{{c₃,X2},{c₃}} is non empty set
[X2,c₃] is set
{X2,c₃} is non empty set
{X2} is non empty trivial V53(1) set
{{X2,c₃},{X2}} is non empty set
A is Element of the carrier' of X
s1 is Element of the carrier' of X
c₃ is set
X2 is set
A is set
[c₃,X2] is set
{c₃,X2} is non empty set
{c₃} is non empty trivial V53(1) set
{{c₃,X2},{c₃}} is non empty set
[X2,A] is set
{X2,A} is non empty set
{X2} is non empty trivial V53(1) set
{{X2,A},{X2}} is non empty set
[c₃,A] is set
{c₃,A} is non empty set
{{c₃,A},{c₃}} is non empty set
s1 is Element of the carrier' of X
s2 is Element of the carrier' of X
e1 is Element of the carrier' of X
X is non empty non void V67() () () () () () ()
the carrier' of X is non empty set
(X) is Relation-like the carrier' of X -defined the carrier' of X -valued total quasi_total reflexive symmetric transitive Element of bool [: the carrier' of X, the carrier' of X:]
[: the carrier' of X, the carrier' of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier' of X:] is non empty set
the of X is non empty Element of bool the carrier' of X
bool the carrier' of X is non empty set
G is Element of the carrier' of X
Class ((X),G) is Element of bool the carrier' of X
{G} is non empty trivial V53(1) set
(X) .: {G} is set
c₃ is set
X2 is Element of the carrier' of X
[G,X2] is Element of [: the carrier' of X, the carrier' of X:]
{G,X2} is non empty set
{{G,X2},{G}} is non empty set
c₃ is set
X2 is Element of the carrier' of X
[G,X2] is Element of [: the carrier' of X, the carrier' of X:]
{G,X2} is non empty set
{{G,X2},{G}} is non empty set
X is non empty non void V67() () () () () () ()
the carrier' of X is non empty set
bool the carrier' of X is non empty set
G is Element of the carrier' of X
the carrier of X is non empty set
bool the carrier' of X is non empty Element of bool (bool the carrier' of X)
bool (bool the carrier' of X) is non empty set
c₃ is set
s1 is Element of the carrier' of X
A is Element of the carrier of X
(X,s1,A) is Element of the carrier' of X
the of X is Relation-like [: the carrier of X, the carrier' of X:] -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of X, the carrier' of X:], the carrier' of X:]
[: the carrier of X, the carrier' of X:] is Relation-like non empty set
[:[: the carrier of X, the carrier' of X:], the carrier' of X:] is Relation-like non empty set
bool [:[: the carrier of X, the carrier' of X:], the carrier' of X:] is non empty set
the of X . (A,s1) is Element of the carrier' of X
[A,s1] is set
{A,s1} is non empty set
{A} is non empty trivial V53(1) set
{{A,s1},{A}} is non empty set
the of X . [A,s1] is set
(X,s1) is Element of the carrier' of X
the of X is Relation-like the carrier' of X -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X, the carrier' of X:]
[: the carrier' of X, the carrier' of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier' of X:] is non empty set
the of X . s1 is Element of the carrier' of X
A is non empty set
meet A is set
s1 is Element of bool the carrier' of X
s2 is set
e1 is Element of the carrier' of X
e2 is set
s2 is Element of the carrier of X
(X,e1,s2) is Element of the carrier' of X
the of X is Relation-like [: the carrier of X, the carrier' of X:] -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of X, the carrier' of X:], the carrier' of X:]
[: the carrier of X, the carrier' of X:] is Relation-like non empty set
[:[: the carrier of X, the carrier' of X:], the carrier' of X:] is Relation-like non empty set
bool [:[: the carrier of X, the carrier' of X:], the carrier' of X:] is non empty set
the of X . (s2,e1) is Element of the carrier' of X
[s2,e1] is set
{s2,e1} is non empty set
{s2} is non empty trivial V53(1) set
{{s2,e1},{s2}} is non empty set
the of X . [s2,e1] is set
e2 is set
(X,e1) is Element of the carrier' of X
the of X is Relation-like the carrier' of X -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X, the carrier' of X:]
[: the carrier' of X, the carrier' of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier' of X:] is non empty set
the of X . e1 is Element of the carrier' of X
s2 is Element of bool the carrier' of X
c₃ is Element of bool the carrier' of X
X2 is Element of bool the carrier' of X
X is non empty non void V67() () () () () () ()
the carrier' of X is non empty set
the carrier of X is non empty set
G is Element of the carrier' of X
(X,G) is Element of the carrier' of X
the of X is Relation-like the carrier' of X -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X, the carrier' of X:]
[: the carrier' of X, the carrier' of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier' of X:] is non empty set
the of X . G is Element of the carrier' of X
c₃ is Element of the carrier' of X
(X,c₃) is Element of bool the carrier' of X
bool the carrier' of X is non empty set
X2 is Element of the carrier of X
(X,G,X2) is Element of the carrier' of X
the of X is Relation-like [: the carrier of X, the carrier' of X:] -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of X, the carrier' of X:], the carrier' of X:]
[: the carrier of X, the carrier' of X:] is Relation-like non empty set
[:[: the carrier of X, the carrier' of X:], the carrier' of X:] is Relation-like non empty set
bool [:[: the carrier of X, the carrier' of X:], the carrier' of X:] is non empty set
the of X . (X2,G) is Element of the carrier' of X
[X2,G] is set
{X2,G} is non empty set
{X2} is non empty trivial V53(1) set
{{X2,G},{X2}} is non empty set
the of X . [X2,G] is set
(X,(X,G,X2)) is Element of the carrier' of X
the of X . (X,G,X2) is Element of the carrier' of X
(X,G) is Element of the carrier of X
the of X is Relation-like the carrier' of X -defined the carrier of X -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X, the carrier of X:]
[: the carrier' of X, the carrier of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier of X:] is non empty set
the of X . G is Element of the carrier of X
(X,(X,G),(X,G)) is Element of the carrier' of X
the of X . ((X,G),(X,G)) is Element of the carrier' of X
[(X,G),(X,G)] is set
{(X,G),(X,G)} is non empty set
{(X,G)} is non empty trivial V53(1) set
{{(X,G),(X,G)},{(X,G)}} is non empty set
the of X . [(X,G),(X,G)] is set
X is non empty non void V67() () () () () () ()
the carrier' of X is non empty set
the carrier of X is non empty set
G is Element of the carrier' of X
(X,G) is Element of the carrier' of X
the of X is Relation-like the carrier' of X -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X, the carrier' of X:]
[: the carrier' of X, the carrier' of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier' of X:] is non empty set
the of X . G is Element of the carrier' of X
(X,(X,G)) is Element of bool the carrier' of X
bool the carrier' of X is non empty set
c₃ is Element of the carrier of X
(X,G,c₃) is Element of the carrier' of X
the of X is Relation-like [: the carrier of X, the carrier' of X:] -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of X, the carrier' of X:], the carrier' of X:]
[: the carrier of X, the carrier' of X:] is Relation-like non empty set
[:[: the carrier of X, the carrier' of X:], the carrier' of X:] is Relation-like non empty set
bool [:[: the carrier of X, the carrier' of X:], the carrier' of X:] is non empty set
the of X . (c₃,G) is Element of the carrier' of X
[c₃,G] is set
{c₃,G} is non empty set
{c₃} is non empty trivial V53(1) set
{{c₃,G},{c₃}} is non empty set
the of X . [c₃,G] is set
(X,(X,G,c₃)) is Element of bool the carrier' of X
(X,(X,G,c₃)) is Element of the carrier' of X
the of X . (X,G,c₃) is Element of the carrier' of X
(X,G) is Element of the carrier of X
the of X is Relation-like the carrier' of X -defined the carrier of X -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X, the carrier of X:]
[: the carrier' of X, the carrier of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier of X:] is non empty set
the of X . G is Element of the carrier of X
(X,(X,G),(X,G)) is Element of the carrier' of X
the of X . ((X,G),(X,G)) is Element of the carrier' of X
[(X,G),(X,G)] is set
{(X,G),(X,G)} is non empty set
{(X,G)} is non empty trivial V53(1) set
{{(X,G),(X,G)},{(X,G)}} is non empty set
the of X . [(X,G),(X,G)] is set
X is non empty non void V67() () () () () () ()
the carrier' of X is non empty set
G is Element of the carrier' of X
(X,G) is Element of bool the carrier' of X
bool the carrier' of X is non empty set
the of X is non empty Element of bool the carrier' of X
X2 is Element of the carrier' of X
(X,X2) is Element of the carrier' of X
the of X is Relation-like the carrier' of X -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X, the carrier' of X:]
[: the carrier' of X, the carrier' of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier' of X:] is non empty set
the of X . X2 is Element of the carrier' of X
IFIN (X2, the of X,G,(X,X2)) is Element of the carrier' of X
[:NAT, the carrier' of X:] is Relation-like non empty V46() set
bool [:NAT, the carrier' of X:] is non empty V46() set
c₃ is Relation-like NAT -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [:NAT, the carrier' of X:]
c₃ . 0 is Element of the carrier' of X
X2 is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() set
c₃ . X2 is Element of the carrier' of X
X2 + 1 is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
c₃ . (X2 + 1) is Element of the carrier' of X
(X,(c₃ . X2)) is Element of the carrier' of X
the of X is Relation-like the carrier' of X -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X, the carrier' of X:]
[: the carrier' of X, the carrier' of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier' of X:] is non empty set
the of X . (c₃ . X2) is Element of the carrier' of X
IFIN ((c₃ . X2), the of X,G,(X,(c₃ . X2))) is Element of the carrier' of X
X2 is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() set
c₃ . X2 is Element of the carrier' of X
A is Element of the carrier' of X
X2 + 1 is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
c₃ . (X2 + 1) is Element of the carrier' of X
(X,A) is Element of the carrier' of X
the of X . A is Element of the carrier' of X
(X,(c₃ . X2)) is Element of the carrier' of X
the of X . (c₃ . X2) is Element of the carrier' of X
IFIN ((c₃ . X2), the of X,G,(X,(c₃ . X2))) is Element of the carrier' of X
X is non empty set
[:X,X:] is Relation-like non empty set
bool [:X,X:] is non empty set
G is Relation-like X -defined X -valued Element of bool [:X,X:]
the Element of X is Element of X
<* the Element of X*> is Relation-like NAT -defined X -valued Function-like constant non empty trivial V46() V53(1) FinSequence-like FinSubsequence-like FinSequence of X
[1, the Element of X] is set
{1, the Element of X} is non empty set
{1} is non empty trivial V53(1) set
{{1, the Element of X},{1}} is non empty set
{[1, the Element of X]} is Relation-like Function-like constant non empty trivial V53(1) set
X2 is Relation-like NAT -defined Function-like non empty V46() FinSequence-like FinSubsequence-like RedSequence of G
X is non empty non void V67() () () () () () ()
the carrier' of X is non empty set
[: the carrier' of X, the carrier' of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier' of X:] is non empty set
the carrier of X is non empty set
G is Relation-like the carrier' of X -defined the carrier' of X -valued Element of bool [: the carrier' of X, the carrier' of X:]
c₃ is Relation-like the carrier' of X -defined the carrier' of X -valued Element of bool [: the carrier' of X, the carrier' of X:]
X is non empty set
[:X,X:] is Relation-like non empty set
bool [:X,X:] is non empty set
G is Relation-like X -defined X -valued Element of bool [:X,X:]
c₃ is Relation-like NAT -defined Function-like non empty V46() FinSequence-like FinSubsequence-like RedSequence of G
c₃ . 1 is set
rng c₃ is non empty set
dom c₃ is non empty Element of bool NAT
c₃ . 0 is set
X2 is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() set
c₃ . X2 is set
X2 + 1 is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
c₃ . (X2 + 1) is set
0 + 1 is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
A is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() set
A + 1 is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
len c₃ is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
[(c₃ . X2),(c₃ . (X2 + 1))] is set
{(c₃ . X2),(c₃ . (X2 + 1))} is non empty set
{(c₃ . X2)} is non empty trivial V53(1) set
{{(c₃ . X2),(c₃ . (X2 + 1))},{(c₃ . X2)}} is non empty set
X2 is set
A is set
c₃ . A is set
F₁() is non empty set
[:F₁(),F₁():] is Relation-like non empty set
bool [:F₁(),F₁():] is non empty set
F₂() is Element of F₁()
F₄() is Relation-like F₁() -defined F₁() -valued Element of bool [:F₁(),F₁():]
F₃() is Element of F₁()
X is Relation-like NAT -defined Function-like non empty V46() FinSequence-like FinSubsequence-like RedSequence of F₄()
X . 1 is set
len X is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
X . (len X) is set
G is Relation-like NAT -defined F₁() -valued Function-like non empty V46() FinSequence-like FinSubsequence-like RedSequence of F₄()
dom G is non empty Element of bool NAT
G . 0 is set
c₃ is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() set
G . c₃ is set
c₃ + 1 is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
G . (c₃ + 1) is set
0 + 1 is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
X2 is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() set
X2 + 1 is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
len G is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
rng G is non empty Element of bool F₁()
bool F₁() is non empty set
G /. c₃ is Element of F₁()
G /. (c₃ + 1) is Element of F₁()
[(G /. c₃),(G /. (c₃ + 1))] is Element of [:F₁(),F₁():]
{(G /. c₃),(G /. (c₃ + 1))} is non empty set
{(G /. c₃)} is non empty trivial V53(1) set
{{(G /. c₃),(G /. (c₃ + 1))},{(G /. c₃)}} is non empty set
len G is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
X is non empty non void V67() () () () () () ()
the carrier' of X is non empty set
(X) is Relation-like the carrier' of X -defined the carrier' of X -valued Element of bool [: the carrier' of X, the carrier' of X:]
[: the carrier' of X, the carrier' of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier' of X:] is non empty set
G is Element of the carrier' of X
(X,G) is Element of bool the carrier' of X
bool the carrier' of X is non empty set
X2 is Relation-like NAT -defined Function-like non empty V46() FinSequence-like FinSubsequence-like RedSequence of (X)
X2 . 1 is set
rng X2 is non empty set
dom X2 is non empty Element of bool NAT
X2 . 0 is set
s1 is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() set
X2 . s1 is set
s1 + 1 is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
X2 . (s1 + 1) is set
0 + 1 is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
s2 is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() set
s2 + 1 is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
len X2 is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
A is Relation-like NAT -defined the carrier' of X -valued Function-like non empty V46() FinSequence-like FinSubsequence-like RedSequence of (X)
A /. s1 is Element of the carrier' of X
A /. (s1 + 1) is Element of the carrier' of X
[(A /. s1),(A /. (s1 + 1))] is Element of [: the carrier' of X, the carrier' of X:]
{(A /. s1),(A /. (s1 + 1))} is non empty set
{(A /. s1)} is non empty trivial V53(1) set
{{(A /. s1),(A /. (s1 + 1))},{(A /. s1)}} is non empty set
(X,(A /. s1)) is Element of the carrier' of X
the of X is Relation-like the carrier' of X -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X, the carrier' of X:]
the of X . (A /. s1) is Element of the carrier' of X
the carrier of X is non empty set
e1 is Element of the carrier of X
(X,(A /. s1),e1) is Element of the carrier' of X
the of X is Relation-like [: the carrier of X, the carrier' of X:] -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of X, the carrier' of X:], the carrier' of X:]
[: the carrier of X, the carrier' of X:] is Relation-like non empty set
[:[: the carrier of X, the carrier' of X:], the carrier' of X:] is Relation-like non empty set
bool [:[: the carrier of X, the carrier' of X:], the carrier' of X:] is non empty set
the of X . (e1,(A /. s1)) is Element of the carrier' of X
[e1,(A /. s1)] is set
{e1,(A /. s1)} is non empty set
{e1} is non empty trivial V53(1) set
{{e1,(A /. s1)},{e1}} is non empty set
the of X . [e1,(A /. s1)] is set
s1 is set
s2 is set
X2 . s2 is set
X is non empty non void V67() () () () () () ()
the carrier' of X is non empty set
(X) is Relation-like the carrier' of X -defined the carrier' of X -valued Element of bool [: the carrier' of X, the carrier' of X:]
[: the carrier' of X, the carrier' of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier' of X:] is non empty set
G is Element of the carrier' of X
(X,G) is Element of bool the carrier' of X
bool the carrier' of X is non empty set
{ b₁ where b₁ is Element of the carrier' of X : (X) reduces G,b₁ } is set
X2 is set
A is Element of the carrier' of X
the carrier of X is non empty set
A is Element of the carrier' of X
X2 is Element of the carrier of X
(X,A,X2) is Element of the carrier' of X
the of X is Relation-like [: the carrier of X, the carrier' of X:] -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of X, the carrier' of X:], the carrier' of X:]
[: the carrier of X, the carrier' of X:] is Relation-like non empty set
[:[: the carrier of X, the carrier' of X:], the carrier' of X:] is Relation-like non empty set
bool [:[: the carrier of X, the carrier' of X:], the carrier' of X:] is non empty set
the of X . (X2,A) is Element of the carrier' of X
[X2,A] is set
{X2,A} is non empty set
{X2} is non empty trivial V53(1) set
{{X2,A},{X2}} is non empty set
the of X . [X2,A] is set
[A,(X,A,X2)] is Element of [: the carrier' of X, the carrier' of X:]
{A,(X,A,X2)} is non empty set
{A} is non empty trivial V53(1) set
{{A,(X,A,X2)},{A}} is non empty set
s1 is Element of the carrier' of X
(X,A) is Element of the carrier' of X
the of X is Relation-like the carrier' of X -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X, the carrier' of X:]
the of X . A is Element of the carrier' of X
[A,(X,A)] is Element of [: the carrier' of X, the carrier' of X:]
{A,(X,A)} is non empty set
{{A,(X,A)},{A}} is non empty set
s1 is Element of the carrier' of X
X2 is set
A is Element of the carrier' of X
s1 is Relation-like NAT -defined Function-like non empty V46() FinSequence-like FinSubsequence-like RedSequence of (X)
s1 . 1 is set
len s1 is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
s1 . (len s1) is set
dom s1 is non empty Element of bool NAT
rng s1 is non empty set
X is non empty non void V67() () () () () () ()
the carrier' of X is non empty set
(X) is Relation-like the carrier' of X -defined the carrier' of X -valued Element of bool [: the carrier' of X, the carrier' of X:]
[: the carrier' of X, the carrier' of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier' of X:] is non empty set
G is Element of the carrier' of X
the of X is non empty Element of bool the carrier' of X
bool the carrier' of X is non empty set
A is Element of the carrier' of X
(X,A) is Element of the carrier' of X
the of X is Relation-like the carrier' of X -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X, the carrier' of X:]
the of X . A is Element of the carrier' of X
IFIN (A, the of X,G,(X,A)) is Element of the carrier' of X
[:NAT, the carrier' of X:] is Relation-like non empty V46() set
bool [:NAT, the carrier' of X:] is non empty V46() set
X2 is Relation-like NAT -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [:NAT, the carrier' of X:]
X2 . 0 is Element of the carrier' of X
A is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() set
X2 . A is Element of the carrier' of X
A + 1 is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
X2 . (A + 1) is Element of the carrier' of X
s1 is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like set
len s1 is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
dom s1 is Element of bool NAT
s2 is Element of the carrier' of X
(X,s2) is Element of the carrier' of X
the of X is Relation-like the carrier' of X -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X, the carrier' of X:]
the of X . s2 is Element of the carrier' of X
s2 is Element of the carrier' of X
(X,s2) is Element of the carrier' of X
the of X is Relation-like the carrier' of X -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X, the carrier' of X:]
the of X . s2 is Element of the carrier' of X
(X,(X2 . A)) is Element of the carrier' of X
the of X . (X2 . A) is Element of the carrier' of X
IFIN ((X2 . A), the of X,G,(X,(X2 . A))) is Element of the carrier' of X
e1 is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
e1 + 1 is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
s1 . e1 is set
s1 . (e1 + 1) is set
[(s1 . e1),(s1 . (e1 + 1))] is set
{(s1 . e1),(s1 . (e1 + 1))} is non empty set
{(s1 . e1)} is non empty trivial V53(1) set
{{(s1 . e1),(s1 . (e1 + 1))},{(s1 . e1)}} is non empty set
e1 -' 1 is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
(e1 -' 1) + 1 is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
(e1 + 1) -' 1 is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
X2 . (e1 -' 1) is Element of the carrier' of X
e2 is Element of the carrier' of X
(X,e2) is Element of the carrier' of X
the of X . e2 is Element of the carrier' of X
X2 . e1 is Element of the carrier' of X
(X,(X2 . (e1 -' 1))) is Element of the carrier' of X
the of X . (X2 . (e1 -' 1)) is Element of the carrier' of X
IFIN ((X2 . (e1 -' 1)), the of X,G,(X,(X2 . (e1 -' 1)))) is Element of the carrier' of X
s1 . 1 is set
1 -' 1 is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
X2 . (1 -' 1) is Element of the carrier' of X
e1 is Relation-like NAT -defined the carrier' of X -valued Function-like non empty V46() FinSequence-like FinSubsequence-like RedSequence of (X)
e1 . 1 is set
len e1 is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
e1 . (len e1) is set
dom e1 is non empty Element of bool NAT
(A + 1) -' 1 is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
X2 . ((A + 1) -' 1) is Element of the carrier' of X
e2 is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() set
e1 /. e2 is Element of the carrier' of X
e2 + 1 is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
e1 /. (e2 + 1) is Element of the carrier' of X
(X,(e1 /. e2)) is Element of the carrier' of X
the of X . (e1 /. e2) is Element of the carrier' of X
e1 . e2 is set
e2 -' 1 is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
X2 . (e2 -' 1) is Element of the carrier' of X
e1 . (e2 + 1) is set
(e2 + 1) -' 1 is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
X2 . ((e2 + 1) -' 1) is Element of the carrier' of X
(e2 -' 1) + 1 is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
q2 is Element of the carrier' of X
(X,q2) is Element of the carrier' of X
the of X . q2 is Element of the carrier' of X
X2 . e2 is Element of the carrier' of X
(X,(X2 . (e2 -' 1))) is Element of the carrier' of X
the of X . (X2 . (e2 -' 1)) is Element of the carrier' of X
IFIN ((X2 . (e2 -' 1)), the of X,G,(X,(X2 . (e2 -' 1)))) is Element of the carrier' of X
c₃ is Element of the carrier' of X
X2 is Element of the carrier' of X
A is Relation-like NAT -defined the carrier' of X -valued Function-like non empty V46() FinSequence-like FinSubsequence-like RedSequence of (X)
A . 1 is set
len A is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
A . (len A) is set
s1 is Relation-like NAT -defined the carrier' of X -valued Function-like non empty V46() FinSequence-like FinSubsequence-like RedSequence of (X)
s1 . 1 is set
len s1 is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
s1 . (len s1) is set
dom A is non empty Element of bool NAT
dom s1 is non empty Element of bool NAT
A . 0 is set
s1 . 0 is set
s2 is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() set
A . s2 is set
s1 . s2 is set
s2 + 1 is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
A . (s2 + 1) is set
s1 . (s2 + 1) is set
e1 is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() set
e1 + 1 is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
e1 is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() set
e1 + 1 is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
A /. s2 is Element of the carrier' of X
s1 /. s2 is Element of the carrier' of X
A /. (s2 + 1) is Element of the carrier' of X
(X,(A /. s2)) is Element of the carrier' of X
the of X is Relation-like the carrier' of X -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X, the carrier' of X:]
the of X . (A /. s2) is Element of the carrier' of X
s1 /. (s2 + 1) is Element of the carrier' of X
(X,(s1 /. s2)) is Element of the carrier' of X
the of X . (s1 /. s2) is Element of the carrier' of X
s2 is set
s2 is set
X is non empty non void V67() () () () () () ()
the carrier' of X is non empty set
G is Element of the carrier' of X
(X,G) is Element of the carrier' of X
(X) is Relation-like the carrier' of X -defined the carrier' of X -valued Element of bool [: the carrier' of X, the carrier' of X:]
[: the carrier' of X, the carrier' of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier' of X:] is non empty set
X2 is Relation-like NAT -defined the carrier' of X -valued Function-like non empty V46() FinSequence-like FinSubsequence-like RedSequence of (X)
X2 . 1 is set
len X2 is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
X2 . (len X2) is set
dom X2 is non empty Element of bool NAT
X2 /. 1 is Element of the carrier' of X
X is non empty non void V67() () () () () () ()
the carrier' of X is non empty set
the carrier of X is non empty set
G is Element of the carrier' of X
(X,G) is Element of the carrier' of X
c₃ is Element of the carrier of X
(X,G,c₃) is Element of the carrier' of X
the of X is Relation-like [: the carrier of X, the carrier' of X:] -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of X, the carrier' of X:], the carrier' of X:]
[: the carrier of X, the carrier' of X:] is Relation-like non empty set
[:[: the carrier of X, the carrier' of X:], the carrier' of X:] is Relation-like non empty set
bool [:[: the carrier of X, the carrier' of X:], the carrier' of X:] is non empty set
the of X . (c₃,G) is Element of the carrier' of X
[c₃,G] is set
{c₃,G} is non empty set
{c₃} is non empty trivial V53(1) set
{{c₃,G},{c₃}} is non empty set
the of X . [c₃,G] is set
(X,(X,G,c₃)) is Element of the carrier' of X
(X) is Relation-like the carrier' of X -defined the carrier' of X -valued Element of bool [: the carrier' of X, the carrier' of X:]
[: the carrier' of X, the carrier' of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier' of X:] is non empty set
s1 is Relation-like NAT -defined the carrier' of X -valued Function-like non empty V46() FinSequence-like FinSubsequence-like RedSequence of (X)
s1 . 1 is set
len s1 is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
s1 . (len s1) is set
(X,(X,G,c₃)) is Element of the carrier' of X
the of X is Relation-like the carrier' of X -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X, the carrier' of X:]
the of X . (X,G,c₃) is Element of the carrier' of X
[(X,G,c₃),G] is Element of [: the carrier' of X, the carrier' of X:]
{(X,G,c₃),G} is non empty set
{(X,G,c₃)} is non empty trivial V53(1) set
{{(X,G,c₃),G},{(X,G,c₃)}} is non empty set
<*(X,G,c₃),G*> is Relation-like NAT -defined Function-like non empty V46() V53(2) FinSequence-like FinSubsequence-like set
<*(X,G,c₃)*> is Relation-like NAT -defined Function-like constant non empty trivial V46() V53(1) FinSequence-like FinSubsequence-like set
[1,(X,G,c₃)] is set
{1,(X,G,c₃)} is non empty set
{1} is non empty trivial V53(1) set
{{1,(X,G,c₃)},{1}} is non empty set
{[1,(X,G,c₃)]} is Relation-like Function-like constant non empty trivial V53(1) set
<*G*> is Relation-like NAT -defined Function-like constant non empty trivial V46() V53(1) 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 trivial V53(1) set
<*(X,G,c₃)*> ^ <*G*> is Relation-like NAT -defined Function-like non empty V46() V53(1 + 1) FinSequence-like FinSubsequence-like set
1 + 1 is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
s2 is Relation-like NAT -defined Function-like non empty V46() FinSequence-like FinSubsequence-like RedSequence of (X)
s2 . 2 is set
len s2 is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
s2 $^ s1 is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like set
e1 is Relation-like NAT -defined Function-like non empty V46() FinSequence-like FinSubsequence-like RedSequence of (X)
<*(X,G,c₃)*> is Relation-like NAT -defined the carrier' of X -valued Function-like constant non empty trivial V46() V53(1) FinSequence-like FinSubsequence-like FinSequence of the carrier' of X
<*(X,G,c₃)*> ^ s1 is Relation-like NAT -defined Function-like non empty V46() FinSequence-like FinSubsequence-like set
e1 . 1 is set
len <*(X,G,c₃)*> is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
e2 is Relation-like NAT -defined the carrier' of X -valued Function-like non empty V46() FinSequence-like FinSubsequence-like RedSequence of (X)
len e2 is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
1 + (len s1) is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
dom s1 is non empty Element of bool NAT
e2 . (len e2) is set
q2 is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() set
dom e2 is non empty Element of bool NAT
q2 + 1 is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
e2 /. q2 is Element of the carrier' of X
e2 . q2 is set
e2 /. (q2 + 1) is Element of the carrier' of X
e2 . (q2 + 1) is set
e1 is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() set
1 + e1 is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
(X,(e2 /. q2)) is Element of the carrier' of X
the of X . (e2 /. q2) is Element of the carrier' of X
s1 . e1 is set
s1 /. e1 is Element of the carrier' of X
s1 . q2 is set
s1 /. q2 is Element of the carrier' of X
(X,(e2 /. q2)) is Element of the carrier' of X
the of X . (e2 /. q2) is Element of the carrier' of X
X is non empty non void V67() () () () () () ()
the carrier' of X is non empty set
G is Element of the carrier' of X
(X,G) is Element of the carrier' of X
the of X is Relation-like the carrier' of X -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X, the carrier' of X:]
[: the carrier' of X, the carrier' of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier' of X:] is non empty set
the of X . G is Element of the carrier' of X
(X,(X,G)) is Element of the carrier' of X
(X,G) is Element of the carrier' of X
(X) is Relation-like the carrier' of X -defined the carrier' of X -valued Element of bool [: the carrier' of X, the carrier' of X:]
A is Relation-like NAT -defined the carrier' of X -valued Function-like non empty V46() FinSequence-like FinSubsequence-like RedSequence of (X)
A . 1 is set
len A is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
A . (len A) is set
[G,(X,G)] is Element of [: the carrier' of X, the carrier' of X:]
{G,(X,G)} is non empty set
{G} is non empty trivial V53(1) set
{{G,(X,G)},{G}} is non empty set
<*G,(X,G)*> is Relation-like NAT -defined Function-like non empty V46() V53(2) FinSequence-like FinSubsequence-like set
<*G*> is Relation-like NAT -defined Function-like constant non empty trivial V46() V53(1) FinSequence-like FinSubsequence-like set
[1,G] is set
{1,G} is non empty set
{1} is non empty trivial V53(1) set
{{1,G},{1}} is non empty set
{[1,G]} is Relation-like Function-like constant non empty trivial V53(1) set
<*(X,G)*> is Relation-like NAT -defined Function-like constant non empty trivial V46() V53(1) FinSequence-like FinSubsequence-like set
[1,(X,G)] is set
{1,(X,G)} is non empty set
{{1,(X,G)},{1}} is non empty set
{[1,(X,G)]} is Relation-like Function-like constant non empty trivial V53(1) set
<*G*> ^ <*(X,G)*> is Relation-like NAT -defined Function-like non empty V46() V53(1 + 1) FinSequence-like FinSubsequence-like set
1 + 1 is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
s1 is Relation-like NAT -defined Function-like non empty V46() FinSequence-like FinSubsequence-like RedSequence of (X)
s1 . 2 is set
len s1 is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
s1 $^ A is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like set
s2 is Relation-like NAT -defined Function-like non empty V46() FinSequence-like FinSubsequence-like RedSequence of (X)
<*G*> is Relation-like NAT -defined the carrier' of X -valued Function-like constant non empty trivial V46() V53(1) FinSequence-like FinSubsequence-like FinSequence of the carrier' of X
<*G*> ^ A is Relation-like NAT -defined Function-like non empty V46() FinSequence-like FinSubsequence-like set
s2 . 1 is set
len <*G*> is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
e1 is Relation-like NAT -defined the carrier' of X -valued Function-like non empty V46() FinSequence-like FinSubsequence-like RedSequence of (X)
len e1 is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
1 + (len A) is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
dom A is non empty Element of bool NAT
e1 . (len e1) is set
e2 is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() set
dom e1 is non empty Element of bool NAT
e2 + 1 is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
e1 /. e2 is Element of the carrier' of X
e1 . e2 is set
e1 /. (e2 + 1) is Element of the carrier' of X
e1 . (e2 + 1) is set
q2 is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() set
1 + q2 is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
(X,(e1 /. e2)) is Element of the carrier' of X
the of X . (e1 /. e2) is Element of the carrier' of X
A . q2 is set
A /. q2 is Element of the carrier' of X
A . e2 is set
A /. e2 is Element of the carrier' of X
(X,(e1 /. e2)) is Element of the carrier' of X
the of X . (e1 /. e2) is Element of the carrier' of X
X is non empty non void V67() () () () () () ()
the carrier' of X is non empty set
G is Element of the carrier' of X
(X,G) is Element of the carrier' of X
(X,G) is Element of bool the carrier' of X
bool the carrier' of X is non empty set
(X) is Relation-like the carrier' of X -defined the carrier' of X -valued Element of bool [: the carrier' of X, the carrier' of X:]
[: the carrier' of X, the carrier' of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier' of X:] is non empty set
c₃ is Relation-like NAT -defined the carrier' of X -valued Function-like non empty V46() FinSequence-like FinSubsequence-like RedSequence of (X)
c₃ . 1 is set
len c₃ is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
c₃ . (len c₃) is set
{ b₁ where b₁ is Element of the carrier' of X : (X) reduces G,b₁ } is set
X is non empty non void V67() () () () () () ()
the carrier' of X is non empty set
the carrier of X is non empty set
the carrier of X * is functional non empty FinSequence-membered M16( the carrier of X)
G is Element of the carrier' of X
(X,G) is Element of bool the carrier' of X
bool the carrier' of X is non empty set
(X,G) is Element of the carrier' of X
(X,(X,G)) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
<*> the carrier of X is Relation-like non-empty empty-yielding NAT -defined the carrier of X -valued Function-like one-to-one constant functional empty proper ext-real non positive non negative irreflexive V39() V40() V41() V43() V44() V45() V46() V51() V53( {} ) FinSequence-like FinSubsequence-like FinSequence-membered co-well_founded weakly-normalizing strongly-normalizing with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete V110() V246() FinSequence of the carrier of X
[:NAT, the carrier of X:] is Relation-like non empty V46() set
X2 is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of X
s1 is Element of the carrier' of X
(X,s1) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
s1 is Element of the carrier' of X
(X,s1) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
A is Element of the carrier of X
<*A*> is Relation-like NAT -defined the carrier of X -valued Function-like constant non empty trivial V46() V53(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of X
[1,A] is set
{1,A} is non empty set
{1} is non empty trivial V53(1) set
{{1,A},{1}} is non empty set
{[1,A]} is Relation-like Function-like constant non empty trivial V53(1) set
( the carrier of X,<*A*>,X2) is Relation-like NAT -defined the carrier of X -valued Function-like non empty V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
(X,s1,A) is Element of the carrier' of X
the of X is Relation-like [: the carrier of X, the carrier' of X:] -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of X, the carrier' of X:], the carrier' of X:]
[: the carrier of X, the carrier' of X:] is Relation-like non empty set
[:[: the carrier of X, the carrier' of X:], the carrier' of X:] is Relation-like non empty set
bool [:[: the carrier of X, the carrier' of X:], the carrier' of X:] is non empty set
the of X . (A,s1) is Element of the carrier' of X
[A,s1] is set
{A,s1} is non empty set
{A} is non empty trivial V53(1) set
{{A,s1},{A}} is non empty set
the of X . [A,s1] is set
s2 is Element of the carrier' of X
(X,s2) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
X2 is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
X is non empty non void V67() () () () () () ()
the carrier' of X is non empty set
G is Element of the carrier' of X
(X,G) is Element of the carrier' of X
c₃ is Element of the carrier' of X
(X,c₃) is Element of bool the carrier' of X
bool the carrier' of X is non empty set
(X,c₃) is Element of the carrier' of X
(X) is Relation-like the carrier' of X -defined the carrier' of X -valued Element of bool [: the carrier' of X, the carrier' of X:]
[: the carrier' of X, the carrier' of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier' of X:] is non empty set
{ b₁ where b₁ is Element of the carrier' of X : (X) reduces c₃,b₁ } is set
A is Element of the carrier' of X
A is Element of the carrier' of X
s1 is Element of the carrier' of X
[A,s1] is Element of [: the carrier' of X, the carrier' of X:]
{A,s1} is non empty set
{A} is non empty trivial V53(1) set
{{A,s1},{A}} is non empty set
(X,A) is Element of the carrier' of X
(X,A) is Element of the carrier' of X
the of X is Relation-like the carrier' of X -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X, the carrier' of X:]
the of X . A is Element of the carrier' of X
the carrier of X is non empty set
(X,s1) is Element of the carrier' of X
s2 is Element of the carrier of X
(X,A,s2) is Element of the carrier' of X
the of X is Relation-like [: the carrier of X, the carrier' of X:] -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of X, the carrier' of X:], the carrier' of X:]
[: the carrier of X, the carrier' of X:] is Relation-like non empty set
[:[: the carrier of X, the carrier' of X:], the carrier' of X:] is Relation-like non empty set
bool [:[: the carrier of X, the carrier' of X:], the carrier' of X:] is non empty set
the of X . (s2,A) is Element of the carrier' of X
[s2,A] is set
{s2,A} is non empty set
{s2} is non empty trivial V53(1) set
{{s2,A},{s2}} is non empty set
the of X . [s2,A] is set
X is non empty non void V67() () () () () () ()
the carrier' of X is non empty set
G is Element of the carrier' of X
(X,G) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
the carrier of X is non empty set
the carrier of X * is functional non empty FinSequence-membered M16( the carrier of X)
c₃ is Element of the carrier' of X
(X,c₃) is Element of bool the carrier' of X
bool the carrier' of X is non empty set
X2 is Element of the carrier' of X
(X,X2) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
A is Element of the carrier' of X
(X,A) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
s1 is Element of the carrier' of X
(X,s1) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
(X,A) is Element of the carrier' of X
(X,c₃) is Element of the carrier' of X
(X,s1) is Element of the carrier' of X
A is Element of the carrier' of X
(X,A) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
s1 is Element of the carrier of X
(X,A,s1) is Element of the carrier' of X
the of X is Relation-like [: the carrier of X, the carrier' of X:] -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of X, the carrier' of X:], the carrier' of X:]
[: the carrier of X, the carrier' of X:] is Relation-like non empty set
[:[: the carrier of X, the carrier' of X:], the carrier' of X:] is Relation-like non empty set
bool [:[: the carrier of X, the carrier' of X:], the carrier' of X:] is non empty set
the of X . (s1,A) is Element of the carrier' of X
[s1,A] is set
{s1,A} is non empty set
{s1} is non empty trivial V53(1) set
{{s1,A},{s1}} is non empty set
the of X . [s1,A] is set
(X,(X,A,s1)) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
s2 is Element of the carrier' of X
(X,s2) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
<*s1*> is Relation-like NAT -defined the carrier of X -valued Function-like constant non empty trivial V46() V53(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of X
[1,s1] is set
{1,s1} is non empty set
{1} is non empty trivial V53(1) set
{{1,s1},{1}} is non empty set
{[1,s1]} is Relation-like Function-like constant non empty trivial V53(1) set
( the carrier of X,<*s1*>,(X,A)) is Relation-like NAT -defined the carrier of X -valued Function-like non empty V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
(X,s2) is Element of the carrier' of X
the of X is Relation-like the carrier' of X -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X, the carrier' of X:]
[: the carrier' of X, the carrier' of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier' of X:] is non empty set
the of X . s2 is Element of the carrier' of X
(X,s2) is Element of the carrier of X
the of X is Relation-like the carrier' of X -defined the carrier of X -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X, the carrier of X:]
[: the carrier' of X, the carrier of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier of X:] is non empty set
the of X . s2 is Element of the carrier of X
(X,(X,s2),(X,s2)) is Element of the carrier' of X
the of X . ((X,s2),(X,s2)) is Element of the carrier' of X
[(X,s2),(X,s2)] is set
{(X,s2),(X,s2)} is non empty set
{(X,s2)} is non empty trivial V53(1) set
{{(X,s2),(X,s2)},{(X,s2)}} is non empty set
the of X . [(X,s2),(X,s2)] is set
<*(X,s2)*> is Relation-like NAT -defined the carrier of X -valued Function-like constant non empty trivial V46() V53(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of X
[1,(X,s2)] is set
{1,(X,s2)} is non empty set
{{1,(X,s2)},{1}} is non empty set
{[1,(X,s2)]} is Relation-like Function-like constant non empty trivial V53(1) set
(X,(X,s2)) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
( the carrier of X,<*(X,s2)*>,(X,(X,s2))) is Relation-like NAT -defined the carrier of X -valued Function-like non empty V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
(X,s2) . 1 is set
X is non empty non void V67() () () () () () ()
the carrier' of X is non empty set
(X) is Relation-like the carrier' of X -defined the carrier' of X -valued total quasi_total reflexive symmetric transitive Element of bool [: the carrier' of X, the carrier' of X:]
[: the carrier' of X, the carrier' of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier' of X:] is non empty set
G is Element of the carrier' of X
(X,G) is Element of bool the carrier' of X
bool the carrier' of X is non empty set
c₃ is Element of the carrier' of X
Class ((X),c₃) is Element of bool the carrier' of X
{c₃} is non empty trivial V53(1) set
(X) .: {c₃} is set
(X,G) /\ (Class ((X),c₃)) is Element of bool the carrier' of X
(X,c₃) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
the carrier of X is non empty set
the carrier of X * is functional non empty FinSequence-membered M16( the carrier of X)
X2 is Element of the carrier' of X
(X,X2) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
{X2} is non empty trivial V53(1) Element of bool the carrier' of X
A is set
s1 is Element of the carrier' of X
[c₃,s1] is Element of [: the carrier' of X, the carrier' of X:]
{c₃,s1} is non empty set
{{c₃,s1},{c₃}} is non empty set
(X,s1) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
[c₃,X2] is Element of [: the carrier' of X, the carrier' of X:]
{c₃,X2} is non empty set
{{c₃,X2},{c₃}} is non empty set
X is non empty non void V67() () () () () () ()
the carrier of X is non empty set
the carrier' of X is non empty set
(X) is Relation-like the carrier' of X -defined the carrier' of X -valued total quasi_total reflexive symmetric transitive Element of bool [: the carrier' of X, the carrier' of X:]
[: the carrier' of X, the carrier' of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier' of X:] is non empty set
Class (X) is non empty with_non-empty_elements a_partition of the carrier' of X
bool the carrier' of X is non empty set
the of X is non empty Element of bool the carrier' of X
{ the of X} is non empty trivial V53(1) Element of bool (bool the carrier' of X)
bool (bool the carrier' of X) is non empty set
the of X is Relation-like [: the carrier of X, the carrier' of X:] -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of X, the carrier' of X:], the carrier' of X:]
[: the carrier of X, the carrier' of X:] is Relation-like non empty set
[:[: the carrier of X, the carrier' of X:], the carrier' of X:] is Relation-like non empty set
bool [:[: the carrier of X, the carrier' of X:], the carrier' of X:] is non empty set
( the carrier of X, the carrier' of X,(X), the of X) is Relation-like [: the carrier of X,(Class (X)):] -defined Class (X) -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of X,(Class (X)):],(Class (X)):]
[: the carrier of X,(Class (X)):] is Relation-like non empty set
[:[: the carrier of X,(Class (X)):],(Class (X)):] is Relation-like non empty set
bool [:[: the carrier of X,(Class (X)):],(Class (X)):] is non empty set
the of X is Relation-like the carrier' of X -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X, the carrier' of X:]
id the of X is Relation-like the of X -defined the of X -valued Function-like one-to-one non empty total quasi_total onto bijective reflexive symmetric antisymmetric transitive Element of bool [: the of X, the of X:]
[: the of X, the of X:] is Relation-like non empty set
bool [: the of X, the of X:] is non empty set
( the carrier' of X, the carrier' of X, the of X, the of X, the of X,(id the of X)) is Relation-like the carrier' of X -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X, the carrier' of X:]
( the carrier' of X, the carrier' of X, the of X, the of X, the of X,(id the of X)) /\/ (X) is Relation-like Class (X) -defined Class (X) -valued Function-like non empty total quasi_total Element of bool [:(Class (X)),(Class (X)):]
[:(Class (X)),(Class (X)):] is Relation-like non empty set
bool [:(Class (X)),(Class (X)):] is non empty set
union (Class (X)) is set
the of X is Relation-like the carrier' of X -defined the carrier of X -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X, the carrier of X:]
[: the carrier' of X, the carrier of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier of X:] is non empty set
the Element of the carrier of X is Element of the carrier of X
G is () ()
the carrier of G is set
the carrier' of G is set
the of G is Element of bool the carrier' of G
bool the carrier' of G is non empty set
the of G is Relation-like [: the carrier of G, the carrier' of G:] -defined the carrier' of G -valued Function-like quasi_total Element of bool [:[: the carrier of G, the carrier' of G:], the carrier' of G:]
[: the carrier of G, the carrier' of G:] is Relation-like set
[:[: the carrier of G, the carrier' of G:], the carrier' of G:] is Relation-like set
bool [:[: the carrier of G, the carrier' of G:], the carrier' of G:] is non empty set
the of G is Relation-like the carrier' of G -defined the carrier' of G -valued Function-like total quasi_total Element of bool [: the carrier' of G, the carrier' of G:]
[: the carrier' of G, the carrier' of G:] is Relation-like set
bool [: the carrier' of G, the carrier' of G:] is non empty set
the of G is Relation-like the carrier' of G -defined the carrier of G -valued Function-like quasi_total Element of bool [: the carrier' of G, the carrier of G:]
[: the carrier' of G, the carrier of G:] is Relation-like set
bool [: the carrier' of G, the carrier of G:] is non empty set
c₃ is () ()
the carrier of c₃ is set
the carrier' of c₃ is set
the of c₃ is Element of bool the carrier' of c₃
bool the carrier' of c₃ is non empty set
the of c₃ is Relation-like [: the carrier of c₃, the carrier' of c₃:] -defined the carrier' of c₃ -valued Function-like quasi_total Element of bool [:[: the carrier of c₃, the carrier' of c₃:], the carrier' of c₃:]
[: the carrier of c₃, the carrier' of c₃:] is Relation-like set
[:[: the carrier of c₃, the carrier' of c₃:], the carrier' of c₃:] is Relation-like set
bool [:[: the carrier of c₃, the carrier' of c₃:], the carrier' of c₃:] is non empty set
the of c₃ is Relation-like the carrier' of c₃ -defined the carrier' of c₃ -valued Function-like total quasi_total Element of bool [: the carrier' of c₃, the carrier' of c₃:]
[: the carrier' of c₃, the carrier' of c₃:] is Relation-like set
bool [: the carrier' of c₃, the carrier' of c₃:] is non empty set
the of c₃ is Relation-like the carrier' of c₃ -defined the carrier of c₃ -valued Function-like quasi_total Element of bool [: the carrier' of c₃, the carrier of c₃:]
[: the carrier' of c₃, the carrier of c₃:] is Relation-like set
bool [: the carrier' of c₃, the carrier of c₃:] is non empty set
the Relation-like Class (X) -defined union (Class (X)) -valued Function-like quasi_total Choice_Function of Class (X) is Relation-like Class (X) -defined union (Class (X)) -valued Function-like quasi_total Choice_Function of Class (X)
the of X * the Relation-like Class (X) -defined union (Class (X)) -valued Function-like quasi_total Choice_Function of Class (X) is Relation-like Class (X) -defined the carrier of X -valued Function-like Element of bool [:(Class (X)), the carrier of X:]
[:(Class (X)), the carrier of X:] is Relation-like non empty set
bool [:(Class (X)), the carrier of X:] is non empty set
( the of X * the Relation-like Class (X) -defined union (Class (X)) -valued Function-like quasi_total Choice_Function of Class (X)) +* ( the of X, the Element of the carrier of X) is Relation-like Function-like set
the Relation-like Class (X) -defined union (Class (X)) -valued Function-like quasi_total Choice_Function of Class (X) is Relation-like Class (X) -defined union (Class (X)) -valued Function-like quasi_total Choice_Function of Class (X)
union (Class (X)) is Element of bool the carrier' of X
[:(Class (X)), the carrier' of X:] is Relation-like non empty set
bool [:(Class (X)), the carrier' of X:] is non empty set
X2 is Element of the carrier' of X
Class ((X),X2) is Element of bool the carrier' of X
{X2} is non empty trivial V53(1) set
(X) .: {X2} is set
c₃ is Relation-like Class (X) -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [:(Class (X)), the carrier' of X:]
the of X * c₃ is Relation-like Class (X) -defined the carrier of X -valued Function-like non empty total quasi_total Element of bool [:(Class (X)), the carrier of X:]
[:(Class (X)), the carrier of X:] is Relation-like non empty set
bool [:(Class (X)), the carrier of X:] is non empty set
A is Element of Class (X)
{A} is non empty trivial V53(1) Element of bool (Class (X))
bool (Class (X)) is non empty set
( the of X * c₃) +* ( the of X, the Element of the carrier of X) is Relation-like Class (X) -defined the carrier of X -valued Function-like non empty total quasi_total Element of bool [:(Class (X)), the carrier of X:]
( the carrier of X,(Class (X)),{A},( the carrier of X, the carrier' of X,(X), the of X),(( the carrier' of X, the carrier' of X, the of X, the of X, the of X,(id the of X)) /\/ (X)),(( the of X * c₃) +* ( the of X, the Element of the carrier of X))) is non empty non void V67() () ()
s2 is non empty non void V67() () ()
the carrier of s2 is non empty set
the carrier' of s2 is non empty set
the of s2 is Element of bool the carrier' of s2
bool the carrier' of s2 is non empty set
the of s2 is Relation-like [: the carrier of s2, the carrier' of s2:] -defined the carrier' of s2 -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of s2, the carrier' of s2:], the carrier' of s2:]
[: the carrier of s2, the carrier' of s2:] is Relation-like non empty set
[:[: the carrier of s2, the carrier' of s2:], the carrier' of s2:] is Relation-like non empty set
bool [:[: the carrier of s2, the carrier' of s2:], the carrier' of s2:] is non empty set
the of s2 is Relation-like the carrier' of s2 -defined the carrier' of s2 -valued Function-like non empty total quasi_total Element of bool [: the carrier' of s2, the carrier' of s2:]
[: the carrier' of s2, the carrier' of s2:] is Relation-like non empty set
bool [: the carrier' of s2, the carrier' of s2:] is non empty set
the of s2 is Relation-like the carrier' of s2 -defined the carrier of s2 -valued Function-like non empty total quasi_total Element of bool [: the carrier' of s2, the carrier of s2:]
[: the carrier' of s2, the carrier of s2:] is Relation-like non empty set
bool [: the carrier' of s2, the carrier of s2:] is non empty set
e1 is Relation-like Class (X) -defined union (Class (X)) -valued Function-like quasi_total Choice_Function of Class (X)
the of X * e1 is Relation-like Class (X) -defined the carrier of X -valued Function-like Element of bool [:(Class (X)), the carrier of X:]
( the of X * e1) +* ( the of X, the Element of the carrier of X) is Relation-like Function-like set
q2 is Element of Class (X)
e1 is Element of the carrier' of X
Class ((X),e1) is Element of bool the carrier' of X
{e1} is non empty trivial V53(1) set
(X) .: {e1} is set
dom ( the of X * c₃) is non empty Element of bool (Class (X))
e2 is Relation-like Class (X) -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [:(Class (X)), the carrier' of X:]
the of X * e2 is Relation-like Class (X) -defined the carrier of X -valued Function-like non empty total quasi_total Element of bool [:(Class (X)), the carrier of X:]
dom ( the of X * e2) is non empty Element of bool (Class (X))
(( the of X * c₃) +* ( the of X, the Element of the carrier of X)) . q2 is Element of the carrier of X
( the of X * e2) +* ( the of X, the Element of the carrier of X) is Relation-like Class (X) -defined the carrier of X -valued Function-like non empty total quasi_total Element of bool [:(Class (X)), the carrier of X:]
(( the of X * e2) +* ( the of X, the Element of the carrier of X)) . q2 is Element of the carrier of X
c₃ . q2 is Element of the carrier' of X
e1 . q2 is Element of union (Class (X))
[e1,(c₃ . q2)] is Element of [: the carrier' of X, the carrier' of X:]
{e1,(c₃ . q2)} is non empty set
{{e1,(c₃ . q2)},{e1}} is non empty set
[e1,(e1 . q2)] is set
{e1,(e1 . q2)} is non empty set
{{e1,(e1 . q2)},{e1}} is non empty set
e2 is Relation-like Class (X) -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [:(Class (X)), the carrier' of X:]
e2 . q2 is Element of the carrier' of X
(X,(c₃ . q2)) is Element of the carrier of X
the of X . (c₃ . q2) is Element of the carrier of X
(X,(e2 . q2)) is Element of the carrier of X
the of X . (e2 . q2) is Element of the carrier of X
( the of X * c₃) . q2 is Element of the carrier of X
the of X * e2 is Relation-like Class (X) -defined the carrier of X -valued Function-like non empty total quasi_total Element of bool [:(Class (X)), the carrier of X:]
( the of X * e2) . q2 is Element of the carrier of X
(( the of X * c₃) +* ( the of X, the Element of the carrier of X)) . q2 is Element of the carrier of X
( the of X * e2) +* ( the of X, the Element of the carrier of X) is Relation-like Class (X) -defined the carrier of X -valued Function-like non empty total quasi_total Element of bool [:(Class (X)), the carrier of X:]
(( the of X * e2) +* ( the of X, the Element of the carrier of X)) . q2 is Element of the carrier of X
e2 is Relation-like Class (X) -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [:(Class (X)), the carrier' of X:]
the of X * e2 is Relation-like Class (X) -defined the carrier of X -valued Function-like non empty total quasi_total Element of bool [:(Class (X)), the carrier of X:]
( the of X * e2) +* ( the of X, the Element of the carrier of X) is Relation-like Class (X) -defined the carrier of X -valued Function-like non empty total quasi_total Element of bool [:(Class (X)), the carrier of X:]
e2 is Relation-like Class (X) -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [:(Class (X)), the carrier' of X:]
the of X * e2 is Relation-like Class (X) -defined the carrier of X -valued Function-like non empty total quasi_total Element of bool [:(Class (X)), the carrier of X:]
( the of X * e2) +* ( the of X, the Element of the carrier of X) is Relation-like Class (X) -defined the carrier of X -valued Function-like non empty total quasi_total Element of bool [:(Class (X)), the carrier of X:]
X is non empty non void V67() () () () () () ()
(X) is () ()
the carrier of (X) is set
the carrier of X is non empty set
the carrier' of (X) is set
the carrier' of X is non empty set
(X) is Relation-like the carrier' of X -defined the carrier' of X -valued total quasi_total reflexive symmetric transitive Element of bool [: the carrier' of X, the carrier' of X:]
[: the carrier' of X, the carrier' of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier' of X:] is non empty set
Class (X) is non empty with_non-empty_elements a_partition of the carrier' of X
X is non empty non void V67() () () () () () ()
(X) is non empty non void V67() () ()
the carrier' of (X) is non empty set
the carrier' of X is non empty set
(X) is Relation-like the carrier' of X -defined the carrier' of X -valued total quasi_total reflexive symmetric transitive Element of bool [: the carrier' of X, the carrier' of X:]
[: the carrier' of X, the carrier' of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier' of X:] is non empty set
G is Element of the carrier' of (X)
Class (X) is non empty with_non-empty_elements a_partition of the carrier' of X
c₃ is set
Class ((X),c₃) is Element of bool the carrier' of X
bool the carrier' of X is non empty set
{c₃} is non empty trivial V53(1) set
(X) .: {c₃} is set
X is non empty non void V67() () () () () () ()
the carrier' of X is non empty set
(X) is Relation-like the carrier' of X -defined the carrier' of X -valued total quasi_total reflexive symmetric transitive Element of bool [: the carrier' of X, the carrier' of X:]
[: the carrier' of X, the carrier' of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier' of X:] is non empty set
(X) is non empty non void V67() () ()
the carrier' of (X) is non empty set
G is Element of the carrier' of X
Class ((X),G) is Element of bool the carrier' of X
bool the carrier' of X is non empty set
{G} is non empty trivial V53(1) set
(X) .: {G} is set
Class (X) is non empty with_non-empty_elements a_partition of the carrier' of X
X is non empty non void V67() () () () () () ()
the carrier' of X is non empty set
(X) is non empty non void V67() () ()
the carrier' of (X) is non empty set
(X) is Relation-like the carrier' of X -defined the carrier' of X -valued total quasi_total reflexive symmetric transitive Element of bool [: the carrier' of X, the carrier' of X:]
[: the carrier' of X, the carrier' of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier' of X:] is non empty set
G is Element of the carrier' of X
Class ((X),G) is Element of bool the carrier' of X
bool the carrier' of X is non empty set
{G} is non empty trivial V53(1) set
(X) .: {G} is set
c₃ is Element of the carrier' of (X)
X2 is Element of the carrier' of X
the of (X) is Element of bool the carrier' of (X)
bool the carrier' of (X) is non empty set
the of X is non empty Element of bool the carrier' of X
{ the of X} is non empty trivial V53(1) Element of bool (bool the carrier' of X)
bool (bool the carrier' of X) is non empty set
Class ((X),X2) is Element of bool the carrier' of X
{X2} is non empty trivial V53(1) set
(X) .: {X2} is set
[G,X2] is Element of [: the carrier' of X, the carrier' of X:]
{G,X2} is non empty set
{{G,X2},{G}} is non empty set
X is non empty non void V67() () () () () () ()
(X) is non empty non void V67() () ()
the carrier' of (X) is non empty set
the of X is non empty Element of bool the carrier' of X
the carrier' of X is non empty set
bool the carrier' of X is non empty set
G is Element of the carrier' of (X)
(X) is Relation-like the carrier' of X -defined the carrier' of X -valued total quasi_total reflexive symmetric transitive Element of bool [: the carrier' of X, the carrier' of X:]
[: the carrier' of X, the carrier' of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier' of X:] is non empty set
Class (X) is non empty with_non-empty_elements a_partition of the carrier' of X
c₃ is set
Class ((X),c₃) is Element of bool the carrier' of X
{c₃} is non empty trivial V53(1) set
(X) .: {c₃} is set
X2 is Element of the carrier' of X
X is non empty non void V67() () () () () () ()
the carrier' of X is non empty set
the carrier of X is non empty set
(X) is non empty non void V67() () ()
the carrier' of (X) is non empty set
the carrier of (X) is non empty set
(X) is Relation-like the carrier' of X -defined the carrier' of X -valued total quasi_total reflexive symmetric transitive Element of bool [: the carrier' of X, the carrier' of X:]
[: the carrier' of X, the carrier' of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier' of X:] is non empty set
G is Element of the carrier' of X
Class ((X),G) is Element of bool the carrier' of X
bool the carrier' of X is non empty set
{G} is non empty trivial V53(1) set
(X) .: {G} is set
c₃ is Element of the carrier of X
(X,G,c₃) is Element of the carrier' of X
the of X is Relation-like [: the carrier of X, the carrier' of X:] -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of X, the carrier' of X:], the carrier' of X:]
[: the carrier of X, the carrier' of X:] is Relation-like non empty set
[:[: the carrier of X, the carrier' of X:], the carrier' of X:] is Relation-like non empty set
bool [:[: the carrier of X, the carrier' of X:], the carrier' of X:] is non empty set
the of X . (c₃,G) is Element of the carrier' of X
[c₃,G] is set
{c₃,G} is non empty set
{c₃} is non empty trivial V53(1) set
{{c₃,G},{c₃}} is non empty set
the of X . [c₃,G] is set
Class ((X),(X,G,c₃)) is Element of bool the carrier' of X
{(X,G,c₃)} is non empty trivial V53(1) set
(X) .: {(X,G,c₃)} is set
X2 is Element of the carrier' of (X)
A is Element of the carrier of (X)
((X),X2,A) is Element of the carrier' of (X)
the of (X) is Relation-like [: the carrier of (X), the carrier' of (X):] -defined the carrier' of (X) -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of (X), the carrier' of (X):], the carrier' of (X):]
[: the carrier of (X), the carrier' of (X):] is Relation-like non empty set
[:[: the carrier of (X), the carrier' of (X):], the carrier' of (X):] is Relation-like non empty set
bool [:[: the carrier of (X), the carrier' of (X):], the carrier' of (X):] is non empty set
the of (X) . (A,X2) is Element of the carrier' of (X)
[A,X2] is set
{A,X2} is non empty set
{A} is non empty trivial V53(1) set
{{A,X2},{A}} is non empty set
the of (X) . [A,X2] is set
Class (X) is non empty with_non-empty_elements a_partition of the carrier' of X
s1 is Element of the carrier of X
s2 is Element of the carrier' of X
e1 is Element of the carrier' of X
[s2,e1] is Element of [: the carrier' of X, the carrier' of X:]
{s2,e1} is non empty set
{s2} is non empty trivial V53(1) set
{{s2,e1},{s2}} is non empty set
the of X . (s1,s2) is Element of the carrier' of X
[s1,s2] is set
{s1,s2} is non empty set
{s1} is non empty trivial V53(1) set
{{s1,s2},{s1}} is non empty set
the of X . [s1,s2] is set
the of X . (s1,e1) is Element of the carrier' of X
[s1,e1] is set
{s1,e1} is non empty set
{{s1,e1},{s1}} is non empty set
the of X . [s1,e1] is set
[( the of X . (s1,s2)),( the of X . (s1,e1))] is Element of [: the carrier' of X, the carrier' of X:]
{( the of X . (s1,s2)),( the of X . (s1,e1))} is non empty set
{( the of X . (s1,s2))} is non empty trivial V53(1) set
{{( the of X . (s1,s2)),( the of X . (s1,e1))},{( the of X . (s1,s2))}} is non empty set
(X,s2,s1) is Element of the carrier' of X
(X,e1,s1) is Element of the carrier' of X
( the carrier of X, the carrier' of X,(X), the of X) is Relation-like [: the carrier of X,(Class (X)):] -defined Class (X) -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of X,(Class (X)):],(Class (X)):]
[: the carrier of X,(Class (X)):] is Relation-like non empty set
[:[: the carrier of X,(Class (X)):],(Class (X)):] is Relation-like non empty set
bool [:[: the carrier of X,(Class (X)):],(Class (X)):] is non empty set
( the carrier of X, the carrier' of X,(X), the of X) . (A,X2) is set
( the carrier of X, the carrier' of X,(X), the of X) . [A,X2] is set
X is non empty non void V67() () () () () () ()
the carrier' of X is non empty set
(X) is non empty non void V67() () ()
the carrier' of (X) is non empty set
(X) is Relation-like the carrier' of X -defined the carrier' of X -valued total quasi_total reflexive symmetric transitive Element of bool [: the carrier' of X, the carrier' of X:]
[: the carrier' of X, the carrier' of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier' of X:] is non empty set
G is Element of the carrier' of X
Class ((X),G) is Element of bool the carrier' of X
bool the carrier' of X is non empty set
{G} is non empty trivial V53(1) set
(X) .: {G} is set
(X,G) is Element of the carrier' of X
the of X is Relation-like the carrier' of X -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X, the carrier' of X:]
the of X . G is Element of the carrier' of X
Class ((X),(X,G)) is Element of bool the carrier' of X
{(X,G)} is non empty trivial V53(1) set
(X) .: {(X,G)} is set
the of X is non empty Element of bool the carrier' of X
id the of X is Relation-like the of X -defined the of X -valued Function-like one-to-one non empty total quasi_total onto bijective reflexive symmetric antisymmetric transitive Element of bool [: the of X, the of X:]
[: the of X, the of X:] is Relation-like non empty set
bool [: the of X, the of X:] is non empty set
A is Element of the carrier' of (X)
((X),A) is Element of the carrier' of (X)
the of (X) is Relation-like the carrier' of (X) -defined the carrier' of (X) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (X), the carrier' of (X):]
[: the carrier' of (X), the carrier' of (X):] is Relation-like non empty set
bool [: the carrier' of (X), the carrier' of (X):] is non empty set
the of (X) . A is Element of the carrier' of (X)
Class (X) is non empty with_non-empty_elements a_partition of the carrier' of X
dom (id the of X) is non empty Element of bool the of X
bool the of X is non empty set
( the carrier' of X, the carrier' of X, the of X, the of X, the of X,(id the of X)) is Relation-like the carrier' of X -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X, the carrier' of X:]
s1 is Element of the carrier' of X
s2 is Element of the carrier' of X
[s1,s2] is Element of [: the carrier' of X, the carrier' of X:]
{s1,s2} is non empty set
{s1} is non empty trivial V53(1) set
{{s1,s2},{s1}} is non empty set
( the carrier' of X, the carrier' of X, the of X, the of X, the of X,(id the of X)) . s1 is Element of the carrier' of X
( the carrier' of X, the carrier' of X, the of X, the of X, the of X,(id the of X)) . s2 is Element of the carrier' of X
[(( the carrier' of X, the carrier' of X, the of X, the of X, the of X,(id the of X)) . s1),(( the carrier' of X, the carrier' of X, the of X, the of X, the of X,(id the of X)) . s2)] is Element of [: the carrier' of X, the carrier' of X:]
{(( the carrier' of X, the carrier' of X, the of X, the of X, the of X,(id the of X)) . s1),(( the carrier' of X, the carrier' of X, the of X, the of X, the of X,(id the of X)) . s2)} is non empty set
{(( the carrier' of X, the carrier' of X, the of X, the of X, the of X,(id the of X)) . s1)} is non empty trivial V53(1) set
{{(( the carrier' of X, the carrier' of X, the of X, the of X, the of X,(id the of X)) . s1),(( the carrier' of X, the carrier' of X, the of X, the of X, the of X,(id the of X)) . s2)},{(( the carrier' of X, the carrier' of X, the of X, the of X, the of X,(id the of X)) . s1)}} is non empty set
the of X . s1 is Element of the carrier' of X
the of X . s2 is Element of the carrier' of X
(X,s1) is Element of the carrier' of X
(X,s2) is Element of the carrier' of X
(id the of X) . s1 is set
(id the of X) . s2 is set
( the carrier' of X, the carrier' of X, the of X, the of X, the of X,(id the of X)) /\/ (X) is Relation-like Class (X) -defined Class (X) -valued Function-like non empty total quasi_total Element of bool [:(Class (X)),(Class (X)):]
[:(Class (X)),(Class (X)):] is Relation-like non empty set
bool [:(Class (X)),(Class (X)):] is non empty set
(( the carrier' of X, the carrier' of X, the of X, the of X, the of X,(id the of X)) /\/ (X)) . A is set
( the carrier' of X, the carrier' of X, the of X, the of X, the of X,(id the of X)) . G is Element of the carrier' of X
Class ((X),(( the carrier' of X, the carrier' of X, the of X, the of X, the of X,(id the of X)) . G)) is Element of bool the carrier' of X
{(( the carrier' of X, the carrier' of X, the of X, the of X, the of X,(id the of X)) . G)} is non empty trivial V53(1) set
(X) .: {(( the carrier' of X, the carrier' of X, the of X, the of X, the of X,(id the of X)) . G)} is set
X is non empty non void V67() () () () () () ()
the carrier' of X is non empty set
(X) is non empty non void V67() () ()
the carrier' of (X) is non empty set
(X) is Relation-like the carrier' of X -defined the carrier' of X -valued total quasi_total reflexive symmetric transitive Element of bool [: the carrier' of X, the carrier' of X:]
[: the carrier' of X, the carrier' of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier' of X:] is non empty set
G is Element of the carrier' of X
Class ((X),G) is Element of bool the carrier' of X
bool the carrier' of X is non empty set
{G} is non empty trivial V53(1) set
(X) .: {G} is set
(X,G) is Element of the carrier of X
the carrier of X is non empty set
the of X is Relation-like the carrier' of X -defined the carrier of X -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X, the carrier of X:]
[: the carrier' of X, the carrier of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier of X:] is non empty set
the of X . G is Element of the carrier of X
the of X is non empty Element of bool the carrier' of X
the Element of the carrier of X is Element of the carrier of X
s1 is Element of the carrier' of (X)
((X),s1) is Element of the carrier of (X)
the carrier of (X) is non empty set
the of (X) is Relation-like the carrier' of (X) -defined the carrier of (X) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (X), the carrier of (X):]
[: the carrier' of (X), the carrier of (X):] is Relation-like non empty set
bool [: the carrier' of (X), the carrier of (X):] is non empty set
the of (X) . s1 is Element of the carrier of (X)
Class (X) is non empty with_non-empty_elements a_partition of the carrier' of X
union (Class (X)) is set
the Relation-like Class (X) -defined union (Class (X)) -valued Function-like quasi_total Choice_Function of Class (X) is Relation-like Class (X) -defined union (Class (X)) -valued Function-like quasi_total Choice_Function of Class (X)
the Relation-like Class (X) -defined union (Class (X)) -valued Function-like quasi_total Choice_Function of Class (X) . s1 is set
e1 is Element of the carrier' of X
[G,e1] is Element of [: the carrier' of X, the carrier' of X:]
{G,e1} is non empty set
{{G,e1},{G}} is non empty set
dom the Relation-like Class (X) -defined union (Class (X)) -valued Function-like quasi_total Choice_Function of Class (X) is Element of bool (Class (X))
bool (Class (X)) is non empty set
the of X * the Relation-like Class (X) -defined union (Class (X)) -valued Function-like quasi_total Choice_Function of Class (X) is Relation-like Class (X) -defined the carrier of X -valued Function-like Element of bool [:(Class (X)), the carrier of X:]
[:(Class (X)), the carrier of X:] is Relation-like non empty set
bool [:(Class (X)), the carrier of X:] is non empty set
( the of X * the Relation-like Class (X) -defined union (Class (X)) -valued Function-like quasi_total Choice_Function of Class (X)) +* ( the of X, the Element of the carrier of X) is Relation-like Function-like set
( the of X * the Relation-like Class (X) -defined union (Class (X)) -valued Function-like quasi_total Choice_Function of Class (X)) . s1 is set
(X,e1) is Element of the carrier of X
the of X . e1 is Element of the carrier of X
X is non empty non void V67() () () () () () ()
(X) is non empty non void V67() () ()
the carrier' of (X) is non empty set
[:NAT, the carrier' of (X):] is Relation-like non empty V46() set
bool [:NAT, the carrier' of (X):] is non empty V46() set
G is Relation-like NAT -defined the carrier' of (X) -valued Function-like non empty total quasi_total Element of bool [:NAT, the carrier' of (X):]
the carrier' of X is non empty set
the Element of the carrier' of X is Element of the carrier' of X
(X, the Element of the carrier' of X) is Element of bool the carrier' of X
bool the carrier' of X is non empty set
(X) is Relation-like the carrier' of X -defined the carrier' of X -valued total quasi_total reflexive symmetric transitive Element of bool [: the carrier' of X, the carrier' of X:]
[: the carrier' of X, the carrier' of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier' of X:] is non empty set
Class (X) is non empty with_non-empty_elements a_partition of the carrier' of X
X2 is set
(X, the Element of the carrier' of X) /\ X2 is Element of bool the carrier' of X
A is Element of the carrier' of X
Class ((X),A) is Element of bool the carrier' of X
{A} is non empty trivial V53(1) set
(X) .: {A} is set
(X, the Element of the carrier' of X) /\ (Class ((X),A)) is Element of bool the carrier' of X
s1 is Element of the carrier' of X
{s1} is non empty trivial V53(1) Element of bool the carrier' of X
X2 is Relation-like Function-like set
dom X2 is set
rng X2 is set
[: the carrier' of (X), the carrier' of X:] is Relation-like non empty set
bool [: the carrier' of (X), the carrier' of X:] is non empty set
A is Relation-like the carrier' of (X) -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (X), the carrier' of X:]
A * G is Relation-like NAT -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [:NAT, the carrier' of X:]
[:NAT, the carrier' of X:] is Relation-like non empty V46() set
bool [:NAT, the carrier' of X:] is non empty V46() set
s1 is ext-real non negative V39() V40() V41() V45() V46() V51() V110() V246() set
(A * G) . s1 is Element of the carrier' of X
s2 is Element of the carrier' of X
s1 + 1 is non empty ext-real positive non negative V39() V40() V41() V45() V46() V51() V110() V246() Element of NAT
(A * G) . (s1 + 1) is Element of the carrier' of X
(X,s2) is Element of the carrier' of X
the of X is Relation-like the carrier' of X -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X, the carrier' of X:]
the of X . s2 is Element of the carrier' of X
Class ((X),s2) is Element of bool the carrier' of X
{s2} is non empty trivial V53(1) set
(X) .: {s2} is set
G . s1 is Element of the carrier' of (X)
G . (s1 + 1) is Element of the carrier' of (X)
e1 is Element of the carrier' of (X)
((X),e1) is Element of the carrier' of (X)
the of (X) is Relation-like the carrier' of (X) -defined the carrier' of (X) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (X), the carrier' of (X):]
[: the carrier' of (X), the carrier' of (X):] is Relation-like non empty set
bool [: the carrier' of (X), the carrier' of (X):] is non empty set
the of (X) . e1 is Element of the carrier' of (X)
e2 is Element of the carrier' of X
Class ((X),e2) is Element of bool the carrier' of X
{e2} is non empty trivial V53(1) set
(X) .: {e2} is set
A . (G . s1) is Element of the carrier' of X
(X, the Element of the carrier' of X) /\ (G . s1) is Element of bool the carrier' of X
Class ((X),(X,s2)) is Element of bool the carrier' of X
{(X,s2)} is non empty trivial V53(1) set
(X) .: {(X,s2)} is set
A . (G . (s1 + 1)) is Element of the carrier' of X
(X, the Element of the carrier' of X) /\ (G . (s1 + 1)) is Element of bool the carrier' of X
e1 is Element of the carrier' of X
{e1} is non empty trivial V53(1) Element of bool the carrier' of X
the carrier' of (X) is non empty set
G is Element of the carrier' of (X)
((X),G) is Element of the carrier' of (X)
the of (X) is Relation-like the carrier' of (X) -defined the carrier' of (X) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (X), the carrier' of (X):]
[: the carrier' of (X), the carrier' of (X):] is Relation-like non empty set
bool [: the carrier' of (X), the carrier' of (X):] is non empty set
the of (X) . G is Element of the carrier' of (X)
((X),G) is Element of the carrier of (X)
the carrier of (X) is non empty set
the of (X) is Relation-like the carrier' of (X) -defined the carrier of (X) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (X), the carrier of (X):]
[: the carrier' of (X), the carrier of (X):] is Relation-like non empty set
bool [: the carrier' of (X), the carrier of (X):] is non empty set
the of (X) . G is Element of the carrier of (X)
((X),((X),G),((X),G)) is Element of the carrier' of (X)
the of (X) is Relation-like [: the carrier of (X), the carrier' of (X):] -defined the carrier' of (X) -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of (X), the carrier' of (X):], the carrier' of (X):]
[: the carrier of (X), the carrier' of (X):] is Relation-like non empty set
[:[: the carrier of (X), the carrier' of (X):], the carrier' of (X):] is Relation-like non empty set
bool [:[: the carrier of (X), the carrier' of (X):], the carrier' of (X):] is non empty set
the of (X) . (((X),G),((X),G)) is Element of the carrier' of (X)
[((X),G),((X),G)] is set
{((X),G),((X),G)} is non empty set
{((X),G)} is non empty trivial V53(1) set
{{((X),G),((X),G)},{((X),G)}} is non empty set
the of (X) . [((X),G),((X),G)] is set
the carrier' of X is non empty set
(X) is Relation-like the carrier' of X -defined the carrier' of X -valued total quasi_total reflexive symmetric transitive Element of bool [: the carrier' of X, the carrier' of X:]
[: the carrier' of X, the carrier' of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier' of X:] is non empty set
c₃ is Element of the carrier' of X
Class ((X),c₃) is Element of bool the carrier' of X
bool the carrier' of X is non empty set
{c₃} is non empty trivial V53(1) set
(X) .: {c₃} is set
(X,c₃) is Element of the carrier' of X
the of X is Relation-like the carrier' of X -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X, the carrier' of X:]
the of X . c₃ is Element of the carrier' of X
Class ((X),(X,c₃)) is Element of bool the carrier' of X
{(X,c₃)} is non empty trivial V53(1) set
(X) .: {(X,c₃)} is set
(X,c₃) is Element of the carrier of X
the carrier of X is non empty set
the of X is Relation-like the carrier' of X -defined the carrier of X -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X, the carrier of X:]
[: the carrier' of X, the carrier of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier of X:] is non empty set
the of X . c₃ is Element of the carrier of X
(X,(X,c₃),(X,c₃)) is Element of the carrier' of X
the of X is Relation-like [: the carrier of X, the carrier' of X:] -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of X, the carrier' of X:], the carrier' of X:]
[: the carrier of X, the carrier' of X:] is Relation-like non empty set
[:[: the carrier of X, the carrier' of X:], the carrier' of X:] is Relation-like non empty set
bool [:[: the carrier of X, the carrier' of X:], the carrier' of X:] is non empty set
the of X . ((X,c₃),(X,c₃)) is Element of the carrier' of X
[(X,c₃),(X,c₃)] is set
{(X,c₃),(X,c₃)} is non empty set
{(X,c₃)} is non empty trivial V53(1) set
{{(X,c₃),(X,c₃)},{(X,c₃)}} is non empty set
the of X . [(X,c₃),(X,c₃)] is set
Class ((X),(X,(X,c₃),(X,c₃))) is Element of bool the carrier' of X
{(X,(X,c₃),(X,c₃))} is non empty trivial V53(1) set
(X) .: {(X,(X,c₃),(X,c₃))} is set
X2 is Element of the carrier' of (X)
A is Element of the carrier of (X)
((X),X2,A) is Element of the carrier' of (X)
the of (X) . (A,X2) is Element of the carrier' of (X)
[A,X2] is set
{A,X2} is non empty set
{A} is non empty trivial V53(1) set
{{A,X2},{A}} is non empty set
the of (X) . [A,X2] is set
((X),X2,((X),G)) is Element of the carrier' of (X)
the of (X) . (((X),G),X2) is Element of the carrier' of (X)
[((X),G),X2] is set
{((X),G),X2} is non empty set
{{((X),G),X2},{((X),G)}} is non empty set
the of (X) . [((X),G),X2] is set
the carrier' of (X) is non empty set
the carrier of (X) is non empty set
G is Element of the carrier' of (X)
c₃ is Element of the carrier of (X)
((X),G,c₃) is Element of the carrier' of (X)
the of (X) is Relation-like [: the carrier of (X), the carrier' of (X):] -defined the carrier' of (X) -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of (X), the carrier' of (X):], the carrier' of (X):]
[: the carrier of (X), the carrier' of (X):] is Relation-like non empty set
[:[: the carrier of (X), the carrier' of (X):], the carrier' of (X):] is Relation-like non empty set
bool [:[: the carrier of (X), the carrier' of (X):], the carrier' of (X):] is non empty set
the of (X) . (c₃,G) is Element of the carrier' of (X)
[c₃,G] is set
{c₃,G} is non empty set
{c₃} is non empty trivial V53(1) set
{{c₃,G},{c₃}} is non empty set
the of (X) . [c₃,G] is set
((X),((X),G,c₃)) is Element of the carrier of (X)
the of (X) is Relation-like the carrier' of (X) -defined the carrier of (X) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (X), the carrier of (X):]
[: the carrier' of (X), the carrier of (X):] is Relation-like non empty set
bool [: the carrier' of (X), the carrier of (X):] is non empty set
the of (X) . ((X),G,c₃) is Element of the carrier of (X)
the carrier' of X is non empty set
(X) is Relation-like the carrier' of X -defined the carrier' of X -valued total quasi_total reflexive symmetric transitive Element of bool [: the carrier' of X, the carrier' of X:]
[: the carrier' of X, the carrier' of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier' of X:] is non empty set
X2 is Element of the carrier' of X
Class ((X),X2) is Element of bool the carrier' of X
bool the carrier' of X is non empty set
{X2} is non empty trivial V53(1) set
(X) .: {X2} is set
the carrier of X is non empty set
A is Element of the carrier of X
(X,X2,A) is Element of the carrier' of X
the of X is Relation-like [: the carrier of X, the carrier' of X:] -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of X, the carrier' of X:], the carrier' of X:]
[: the carrier of X, the carrier' of X:] is Relation-like non empty set
[:[: the carrier of X, the carrier' of X:], the carrier' of X:] is Relation-like non empty set
bool [:[: the carrier of X, the carrier' of X:], the carrier' of X:] is non empty set
the of X . (A,X2) is Element of the carrier' of X
[A,X2] is set
{A,X2} is non empty set
{A} is non empty trivial V53(1) set
{{A,X2},{A}} is non empty set
the of X . [A,X2] is set
Class ((X),(X,X2,A)) is Element of bool the carrier' of X
{(X,X2,A)} is non empty trivial V53(1) set
(X) .: {(X,X2,A)} is set
(X,(X,X2,A)) is Element of the carrier of X
the of X is Relation-like the carrier' of X -defined the carrier of X -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X, the carrier of X:]
[: the carrier' of X, the carrier of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier of X:] is non empty set
the of X . (X,X2,A) is Element of the carrier of X
s1 is Element of the carrier' of (X)
((X),s1) is Element of the carrier of (X)
the of (X) . s1 is Element of the carrier of (X)
the carrier' of (X) is non empty set
the carrier of (X) is non empty set
G is Element of the carrier' of (X)
c₃ is Element of the carrier of (X)
((X),G,c₃) is Element of the carrier' of (X)
the of (X) is Relation-like [: the carrier of (X), the carrier' of (X):] -defined the carrier' of (X) -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of (X), the carrier' of (X):], the carrier' of (X):]
[: the carrier of (X), the carrier' of (X):] is Relation-like non empty set
[:[: the carrier of (X), the carrier' of (X):], the carrier' of (X):] is Relation-like non empty set
bool [:[: the carrier of (X), the carrier' of (X):], the carrier' of (X):] is non empty set
the of (X) . (c₃,G) is Element of the carrier' of (X)
[c₃,G] is set
{c₃,G} is non empty set
{c₃} is non empty trivial V53(1) set
{{c₃,G},{c₃}} is non empty set
the of (X) . [c₃,G] is set
((X),((X),G,c₃)) is Element of the carrier' of (X)
the of (X) is Relation-like the carrier' of (X) -defined the carrier' of (X) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of (X), the carrier' of (X):]
[: the carrier' of (X), the carrier' of (X):] is Relation-like non empty set
bool [: the carrier' of (X), the carrier' of (X):] is non empty set
the of (X) . ((X),G,c₃) is Element of the carrier' of (X)
the carrier' of X is non empty set
(X) is Relation-like the carrier' of X -defined the carrier' of X -valued total quasi_total reflexive symmetric transitive Element of bool [: the carrier' of X, the carrier' of X:]
[: the carrier' of X, the carrier' of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier' of X:] is non empty set
X2 is Element of the carrier' of X
Class ((X),X2) is Element of bool the carrier' of X
bool the carrier' of X is non empty set
{X2} is non empty trivial V53(1) set
(X) .: {X2} is set
the carrier of X is non empty set
A is Element of the carrier of X
(X,X2,A) is Element of the carrier' of X
the of X is Relation-like [: the carrier of X, the carrier' of X:] -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of X, the carrier' of X:], the carrier' of X:]
[: the carrier of X, the carrier' of X:] is Relation-like non empty set
[:[: the carrier of X, the carrier' of X:], the carrier' of X:] is Relation-like non empty set
bool [:[: the carrier of X, the carrier' of X:], the carrier' of X:] is non empty set
the of X . (A,X2) is Element of the carrier' of X
[A,X2] is set
{A,X2} is non empty set
{A} is non empty trivial V53(1) set
{{A,X2},{A}} is non empty set
the of X . [A,X2] is set
Class ((X),(X,X2,A)) is Element of bool the carrier' of X
{(X,X2,A)} is non empty trivial V53(1) set
(X) .: {(X,X2,A)} is set
(X,(X,X2,A)) is Element of the carrier' of X
the of X is Relation-like the carrier' of X -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X, the carrier' of X:]
the of X . (X,X2,A) is Element of the carrier' of X
Class ((X),(X,(X,X2,A))) is Element of bool the carrier' of X
{(X,(X,X2,A))} is non empty trivial V53(1) set
(X) .: {(X,(X,X2,A))} is set
s1 is Element of the carrier' of (X)
((X),s1) is Element of the carrier' of (X)
the of (X) . s1 is Element of the carrier' of (X)
the carrier' of (X) is non empty set
the carrier of (X) is non empty set
G is Element of the carrier' of (X)
c₃ is Element of the carrier of (X)
((X),G,c₃) is Element of the carrier' of (X)
the of (X) is Relation-like [: the carrier of (X), the carrier' of (X):] -defined the carrier' of (X) -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of (X), the carrier' of (X):], the carrier' of (X):]
[: the carrier of (X), the carrier' of (X):] is Relation-like non empty set
[:[: the carrier of (X), the carrier' of (X):], the carrier' of (X):] is Relation-like non empty set
bool [:[: the carrier of (X), the carrier' of (X):], the carrier' of (X):] is non empty set
the of (X) . (c₃,G) is Element of the carrier' of (X)
[c₃,G] is set
{c₃,G} is non empty set
{c₃} is non empty trivial V53(1) set
{{c₃,G},{c₃}} is non empty set
the of (X) . [c₃,G] is set
the carrier' of X is non empty set
(X) is Relation-like the carrier' of X -defined the carrier' of X -valued total quasi_total reflexive symmetric transitive Element of bool [: the carrier' of X, the carrier' of X:]
[: the carrier' of X, the carrier' of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier' of X:] is non empty set
X2 is Element of the carrier' of X
Class ((X),X2) is Element of bool the carrier' of X
bool the carrier' of X is non empty set
{X2} is non empty trivial V53(1) set
(X) .: {X2} is set
the carrier of X is non empty set
A is Element of the carrier of X
(X,X2,A) is Element of the carrier' of X
the of X is Relation-like [: the carrier of X, the carrier' of X:] -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of X, the carrier' of X:], the carrier' of X:]
[: the carrier of X, the carrier' of X:] is Relation-like non empty set
[:[: the carrier of X, the carrier' of X:], the carrier' of X:] is Relation-like non empty set
bool [:[: the carrier of X, the carrier' of X:], the carrier' of X:] is non empty set
the of X . (A,X2) is Element of the carrier' of X
[A,X2] is set
{A,X2} is non empty set
{A} is non empty trivial V53(1) set
{{A,X2},{A}} is non empty set
the of X . [A,X2] is set
Class ((X),(X,X2,A)) is Element of bool the carrier' of X
{(X,X2,A)} is non empty trivial V53(1) set
(X) .: {(X,X2,A)} is set
s1 is Element of the carrier' of (X)
X is non empty non void V67() () () () () () ()
the carrier' of X is non empty set
(X) is non empty non void V67() () () () () () () ()
the carrier' of (X) is non empty set
(X) is Relation-like the carrier' of X -defined the carrier' of X -valued total quasi_total reflexive symmetric transitive Element of bool [: the carrier' of X, the carrier' of X:]
[: the carrier' of X, the carrier' of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier' of X:] is non empty set
G is Element of the carrier' of X
Class ((X),G) is Element of bool the carrier' of X
bool the carrier' of X is non empty set
{G} is non empty trivial V53(1) set
(X) .: {G} is set
(X,G) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
the carrier of X is non empty set
the carrier of X * is functional non empty FinSequence-membered M16( the carrier of X)
c₃ is Element of the carrier' of X
Class ((X),c₃) is Element of bool the carrier' of X
{c₃} is non empty trivial V53(1) set
(X) .: {c₃} is set
(X,c₃) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
X2 is Element of the carrier' of (X)
((X),X2) is Relation-like NAT -defined the carrier of (X) -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of (X) *
the carrier of (X) is non empty set
the carrier of (X) * is functional non empty FinSequence-membered M16( the carrier of (X))
c₃ is Element of the carrier' of X
Class ((X),c₃) is Element of bool the carrier' of X
{c₃} is non empty trivial V53(1) set
(X) .: {c₃} is set
(X,c₃) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
X2 is Element of the carrier of X
(X,c₃,X2) is Element of the carrier' of X
the of X is Relation-like [: the carrier of X, the carrier' of X:] -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of X, the carrier' of X:], the carrier' of X:]
[: the carrier of X, the carrier' of X:] is Relation-like non empty set
[:[: the carrier of X, the carrier' of X:], the carrier' of X:] is Relation-like non empty set
bool [:[: the carrier of X, the carrier' of X:], the carrier' of X:] is non empty set
the of X . (X2,c₃) is Element of the carrier' of X
[X2,c₃] is set
{X2,c₃} is non empty set
{X2} is non empty trivial V53(1) set
{{X2,c₃},{X2}} is non empty set
the of X . [X2,c₃] is set
Class ((X),(X,c₃,X2)) is Element of bool the carrier' of X
{(X,c₃,X2)} is non empty trivial V53(1) set
(X) .: {(X,c₃,X2)} is set
(X,(X,c₃,X2)) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
the carrier of (X) is non empty set
s1 is Element of the carrier' of (X)
((X),s1) is Relation-like NAT -defined the carrier of (X) -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of (X) *
the carrier of (X) * is functional non empty FinSequence-membered M16( the carrier of (X))
s2 is Element of the carrier' of (X)
A is Element of the carrier of (X)
((X),s2,A) is Element of the carrier' of (X)
the of (X) is Relation-like [: the carrier of (X), the carrier' of (X):] -defined the carrier' of (X) -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of (X), the carrier' of (X):], the carrier' of (X):]
[: the carrier of (X), the carrier' of (X):] is Relation-like non empty set
[:[: the carrier of (X), the carrier' of (X):], the carrier' of (X):] is Relation-like non empty set
bool [:[: the carrier of (X), the carrier' of (X):], the carrier' of (X):] is non empty set
the of (X) . (A,s2) is Element of the carrier' of (X)
[A,s2] is set
{A,s2} is non empty set
{A} is non empty trivial V53(1) set
{{A,s2},{A}} is non empty set
the of (X) . [A,s2] is set
<*A*> is Relation-like NAT -defined the carrier of (X) -valued Function-like constant non empty trivial V46() V53(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of (X)
[1,A] is set
{1,A} is non empty set
{1} is non empty trivial V53(1) set
{{1,A},{1}} is non empty set
{[1,A]} is Relation-like Function-like constant non empty trivial V53(1) set
((X),s2) is Relation-like NAT -defined the carrier of (X) -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of (X) *
( the carrier of (X),<*A*>,((X),s2)) is Relation-like NAT -defined the carrier of (X) -valued Function-like non empty V46() FinSequence-like FinSubsequence-like Element of the carrier of (X) *
<*X2*> is Relation-like NAT -defined the carrier of X -valued Function-like constant non empty trivial V46() V53(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of X
[1,X2] is set
{1,X2} is non empty set
{{1,X2},{1}} is non empty set
{[1,X2]} is Relation-like Function-like constant non empty trivial V53(1) set
( the carrier of X,<*X2*>,(X,c₃)) is Relation-like NAT -defined the carrier of X -valued Function-like non empty V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
X is non empty non void V67() () () () () () ()
(X) is non empty non void V67() () () () () () () ()
the carrier' of (X) is non empty set
G is Element of the carrier' of (X)
c₃ is Element of the carrier' of (X)
the carrier' of X is non empty set
(X) is Relation-like the carrier' of X -defined the carrier' of X -valued total quasi_total reflexive symmetric transitive Element of bool [: the carrier' of X, the carrier' of X:]
[: the carrier' of X, the carrier' of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier' of X:] is non empty set
X2 is Element of the carrier' of X
Class ((X),X2) is Element of bool the carrier' of X
bool the carrier' of X is non empty set
{X2} is non empty trivial V53(1) set
(X) .: {X2} is set
A is Element of the carrier' of X
Class ((X),A) is Element of bool the carrier' of X
{A} is non empty trivial V53(1) set
(X) .: {A} is set
((X),G) is Relation-like NAT -defined the carrier of (X) -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of (X) *
the carrier of (X) is non empty set
the carrier of (X) * is functional non empty FinSequence-membered M16( the carrier of (X))
((X),c₃) is Relation-like NAT -defined the carrier of (X) -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of (X) *
(X,X2) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
the carrier of X is non empty set
the carrier of X * is functional non empty FinSequence-membered M16( the carrier of X)
(X,A) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
[X2,A] is Element of [: the carrier' of X, the carrier' of X:]
{X2,A} is non empty set
{{X2,A},{X2}} is non empty set
the non empty non void V67() () () () () () () is non empty non void V67() () () () () () ()
( the non empty non void V67() () () () () () ()) is non empty non void V67() () () () () () () () ()
X is non empty non void V67() () () () () () ()
the carrier of X is non empty set
id the carrier of X is Relation-like the carrier of X -defined the carrier of X -valued Function-like one-to-one non empty total quasi_total onto bijective reflexive symmetric antisymmetric transitive Element of bool [: the carrier of X, the carrier of X:]
[: the carrier of X, the carrier of X:] is Relation-like non empty set
bool [: the carrier of X, the carrier of X:] is non empty set
the carrier' of X is non empty set
id the carrier' of X is Relation-like the carrier' of X -defined the carrier' of X -valued Function-like one-to-one non empty total quasi_total onto bijective reflexive symmetric antisymmetric transitive Element of bool [: the carrier' of X, the carrier' of X:]
[: the carrier' of X, the carrier' of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier' of X:] is non empty set
dom (id the carrier of X) is non empty Element of bool the carrier of X
bool the carrier of X is non empty set
rng (id the carrier of X) is non empty Element of bool the carrier of X
dom (id the carrier' of X) is non empty set
rng (id the carrier' of X) is non empty set
dom (id the carrier' of X) is non empty Element of bool the carrier' of X
bool the carrier' of X is non empty set
rng (id the carrier' of X) is non empty Element of bool the carrier' of X
X2 is Element of the carrier' of X
(id the carrier' of X) . X2 is set
(X,X2) is Element of the carrier' of X
the of X is Relation-like the carrier' of X -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X, the carrier' of X:]
the of X . X2 is Element of the carrier' of X
(id the carrier' of X) . (X,X2) is set
(X,X2) is Element of the carrier of X
the of X is Relation-like the carrier' of X -defined the carrier of X -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X, the carrier of X:]
[: the carrier' of X, the carrier of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier of X:] is non empty set
the of X . X2 is Element of the carrier of X
(id the carrier of X) . (X,X2) is set
A is Element of the carrier' of X
(X,A) is Element of the carrier' of X
the of X . A is Element of the carrier' of X
(X,A) is Element of the carrier of X
the of X . A is Element of the carrier of X
(id the carrier' of X) . X2 is Element of the carrier' of X
(id the carrier' of X) . (X,X2) is Element of the carrier' of X
(id the carrier of X) . (X,X2) is Element of the carrier of X
s1 is Element of the carrier of X
(id the carrier of X) . s1 is set
(X,X2,s1) is Element of the carrier' of X
the of X is Relation-like [: the carrier of X, the carrier' of X:] -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of X, the carrier' of X:], the carrier' of X:]
[: the carrier of X, the carrier' of X:] is Relation-like non empty set
[:[: the carrier of X, the carrier' of X:], the carrier' of X:] is Relation-like non empty set
bool [:[: the carrier of X, the carrier' of X:], the carrier' of X:] is non empty set
the of X . (s1,X2) is Element of the carrier' of X
[s1,X2] is set
{s1,X2} is non empty set
{s1} is non empty trivial V53(1) set
{{s1,X2},{s1}} is non empty set
the of X . [s1,X2] is set
(id the carrier' of X) . (X,X2,s1) is set
s2 is Element of the carrier of X
(X,A,s2) is Element of the carrier' of X
the of X . (s2,A) is Element of the carrier' of X
[s2,A] is set
{s2,A} is non empty set
{s2} is non empty trivial V53(1) set
{{s2,A},{s2}} is non empty set
the of X . [s2,A] is set
(id the carrier of X) . s1 is Element of the carrier of X
(id the carrier' of X) . (X,X2,s1) is Element of the carrier' of X
X is non empty non void V67() () () () () () ()
G is non empty non void V67() () () () () () ()
c₃ is Relation-like Function-like set
c₃ " is Relation-like Function-like set
X2 is Relation-like Function-like set
X2 " is Relation-like Function-like set
dom c₃ is set
the carrier of X is non empty set
rng c₃ is set
the carrier of G is non empty set
dom X2 is set
the carrier' of X is non empty set
rng X2 is set
the carrier' of G is non empty set
dom (c₃ ") is set
rng (c₃ ") is set
dom (X2 ") is set
rng (X2 ") is set
A is Element of the carrier' of G
(X2 ") . A is set
(G,A) is Element of the carrier' of G
the of G is Relation-like the carrier' of G -defined the carrier' of G -valued Function-like non empty total quasi_total Element of bool [: the carrier' of G, the carrier' of G:]
[: the carrier' of G, the carrier' of G:] is Relation-like non empty set
bool [: the carrier' of G, the carrier' of G:] is non empty set
the of G . A is Element of the carrier' of G
(X2 ") . (G,A) is set
(G,A) is Element of the carrier of G
the of G is Relation-like the carrier' of G -defined the carrier of G -valued Function-like non empty total quasi_total Element of bool [: the carrier' of G, the carrier of G:]
[: the carrier' of G, the carrier of G:] is Relation-like non empty set
bool [: the carrier' of G, the carrier of G:] is non empty set
the of G . A is Element of the carrier of G
(c₃ ") . (G,A) is set
s1 is Element of the carrier' of X
(X,s1) is Element of the carrier' of X
the of X is Relation-like the carrier' of X -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X, the carrier' of X:]
[: the carrier' of X, the carrier' of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier' of X:] is non empty set
the of X . s1 is Element of the carrier' of X
(X,s1) is Element of the carrier of X
the of X is Relation-like the carrier' of X -defined the carrier of X -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X, the carrier of X:]
[: the carrier' of X, the carrier of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier of X:] is non empty set
the of X . s1 is Element of the carrier of X
X2 . s1 is set
X2 . (X,s1) is set
c₃ . (X,s1) is set
s2 is Element of the carrier of G
(c₃ ") . s2 is set
(G,A,s2) is Element of the carrier' of G
the of G is Relation-like [: the carrier of G, the carrier' of G:] -defined the carrier' of G -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of G, the carrier' of G:], the carrier' of G:]
[: the carrier of G, the carrier' of G:] is Relation-like non empty set
[:[: the carrier of G, the carrier' of G:], the carrier' of G:] is Relation-like non empty set
bool [:[: the carrier of G, the carrier' of G:], the carrier' of G:] is non empty set
the of G . (s2,A) is Element of the carrier' of G
[s2,A] is set
{s2,A} is non empty set
{s2} is non empty trivial V53(1) set
{{s2,A},{s2}} is non empty set
the of G . [s2,A] is set
(X2 ") . (G,A,s2) is set
e1 is Element of the carrier of X
(X,s1,e1) is Element of the carrier' of X
the of X is Relation-like [: the carrier of X, the carrier' of X:] -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of X, the carrier' of X:], the carrier' of X:]
[: the carrier of X, the carrier' of X:] is Relation-like non empty set
[:[: the carrier of X, the carrier' of X:], the carrier' of X:] is Relation-like non empty set
bool [:[: the carrier of X, the carrier' of X:], the carrier' of X:] is non empty set
the of X . (e1,s1) is Element of the carrier' of X
[e1,s1] is set
{e1,s1} is non empty set
{e1} is non empty trivial V53(1) set
{{e1,s1},{e1}} is non empty set
the of X . [e1,s1] is set
c₃ . e1 is set
X2 . (X,s1,e1) is set
X is non empty non void V67() () () () () () ()
G is non empty non void V67() () () () () () ()
c₃ is non empty non void V67() () () () () () ()
X2 is Relation-like Function-like set
A is Relation-like Function-like set
s1 is Relation-like Function-like set
X2 * s1 is Relation-like Function-like set
s2 is Relation-like Function-like set
A * s2 is Relation-like Function-like set
dom X2 is set
the carrier of X is non empty set
rng X2 is set
the carrier of G is non empty set
dom A is set
the carrier' of X is non empty set
rng A is set
the carrier' of G is non empty set
dom s1 is set
rng s1 is set
the carrier of c₃ is non empty set
dom s2 is set
rng s2 is set
the carrier' of c₃ is non empty set
dom (X2 * s1) is set
rng (X2 * s1) is set
dom (A * s2) is set
rng (A * s2) is set
e1 is Element of the carrier' of X
(A * s2) . e1 is set
(X,e1) is Element of the carrier' of X
the of X is Relation-like the carrier' of X -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X, the carrier' of X:]
[: the carrier' of X, the carrier' of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier' of X:] is non empty set
the of X . e1 is Element of the carrier' of X
(A * s2) . (X,e1) is set
(X,e1) is Element of the carrier of X
the of X is Relation-like the carrier' of X -defined the carrier of X -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X, the carrier of X:]
[: the carrier' of X, the carrier of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier of X:] is non empty set
the of X . e1 is Element of the carrier of X
(X2 * s1) . (X,e1) is set
e2 is Element of the carrier' of c₃
(c₃,e2) is Element of the carrier' of c₃
the of c₃ is Relation-like the carrier' of c₃ -defined the carrier' of c₃ -valued Function-like non empty total quasi_total Element of bool [: the carrier' of c₃, the carrier' of c₃:]
[: the carrier' of c₃, the carrier' of c₃:] is Relation-like non empty set
bool [: the carrier' of c₃, the carrier' of c₃:] is non empty set
the of c₃ . e2 is Element of the carrier' of c₃
(c₃,e2) is Element of the carrier of c₃
the of c₃ is Relation-like the carrier' of c₃ -defined the carrier of c₃ -valued Function-like non empty total quasi_total Element of bool [: the carrier' of c₃, the carrier of c₃:]
[: the carrier' of c₃, the carrier of c₃:] is Relation-like non empty set
bool [: the carrier' of c₃, the carrier of c₃:] is non empty set
the of c₃ . e2 is Element of the carrier of c₃
A . e1 is set
q2 is Element of the carrier' of G
s2 . q2 is set
(G,q2) is Element of the carrier' of G
the of G is Relation-like the carrier' of G -defined the carrier' of G -valued Function-like non empty total quasi_total Element of bool [: the carrier' of G, the carrier' of G:]
[: the carrier' of G, the carrier' of G:] is Relation-like non empty set
bool [: the carrier' of G, the carrier' of G:] is non empty set
the of G . q2 is Element of the carrier' of G
A . (X,e1) is set
(G,q2) is Element of the carrier of G
the of G is Relation-like the carrier' of G -defined the carrier of G -valued Function-like non empty total quasi_total Element of bool [: the carrier' of G, the carrier of G:]
[: the carrier' of G, the carrier of G:] is Relation-like non empty set
bool [: the carrier' of G, the carrier of G:] is non empty set
the of G . q2 is Element of the carrier of G
X2 . (X,e1) is set
s2 . (A . (X,e1)) is set
s1 . (X2 . (X,e1)) is set
e1 is Element of the carrier of X
(X2 * s1) . e1 is set
(X,e1,e1) is Element of the carrier' of X
the of X is Relation-like [: the carrier of X, the carrier' of X:] -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of X, the carrier' of X:], the carrier' of X:]
[: the carrier of X, the carrier' of X:] is Relation-like non empty set
[:[: the carrier of X, the carrier' of X:], the carrier' of X:] is Relation-like non empty set
bool [:[: the carrier of X, the carrier' of X:], the carrier' of X:] is non empty set
the of X . (e1,e1) is Element of the carrier' of X
[e1,e1] is set
{e1,e1} is non empty set
{e1} is non empty trivial V53(1) set
{{e1,e1},{e1}} is non empty set
the of X . [e1,e1] is set
(A * s2) . (X,e1,e1) is set
e2 is Element of the carrier of c₃
(c₃,e2,e2) is Element of the carrier' of c₃
the of c₃ is Relation-like [: the carrier of c₃, the carrier' of c₃:] -defined the carrier' of c₃ -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of c₃, the carrier' of c₃:], the carrier' of c₃:]
[: the carrier of c₃, the carrier' of c₃:] is Relation-like non empty set
[:[: the carrier of c₃, the carrier' of c₃:], the carrier' of c₃:] is Relation-like non empty set
bool [:[: the carrier of c₃, the carrier' of c₃:], the carrier' of c₃:] is non empty set
the of c₃ . (e2,e2) is Element of the carrier' of c₃
[e2,e2] is set
{e2,e2} is non empty set
{e2} is non empty trivial V53(1) set
{{e2,e2},{e2}} is non empty set
the of c₃ . [e2,e2] is set
X2 . e1 is set
e3 is Element of the carrier of G
s1 . e3 is set
(G,q2,e3) is Element of the carrier' of G
the of G is Relation-like [: the carrier of G, the carrier' of G:] -defined the carrier' of G -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of G, the carrier' of G:], the carrier' of G:]
[: the carrier of G, the carrier' of G:] is Relation-like non empty set
[:[: the carrier of G, the carrier' of G:], the carrier' of G:] is Relation-like non empty set
bool [:[: the carrier of G, the carrier' of G:], the carrier' of G:] is non empty set
the of G . (e3,q2) is Element of the carrier' of G
[e3,q2] is set
{e3,q2} is non empty set
{e3} is non empty trivial V53(1) set
{{e3,q2},{e3}} is non empty set
the of G . [e3,q2] is set
A . (X,e1,e1) is set
s2 . (A . (X,e1,e1)) is set
X is non empty non void V67() () () () () () ()
the carrier' of X is non empty set
G is non empty non void V67() () () () () () ()
the carrier' of G is non empty set
c₃ is Relation-like Function-like set
X2 is Relation-like Function-like set
dom c₃ is set
the carrier of X is non empty set
rng c₃ is set
the carrier of G is non empty set
dom X2 is set
rng X2 is set
[: the carrier of X, the carrier of G:] is Relation-like non empty set
bool [: the carrier of X, the carrier of G:] is non empty set
[: the carrier' of X, the carrier' of G:] is Relation-like non empty set
bool [: the carrier' of X, the carrier' of G:] is non empty set
s2 is Element of the carrier' of X
X2 . s2 is set
(X,s2) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
the carrier of X * is functional non empty FinSequence-membered M16( the carrier of X)
(X,s2) * c₃ is Relation-like NAT -defined Function-like set
e1 is Element of the carrier' of X
X2 . e1 is set
(X,e1) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
(X,e1) * c₃ is Relation-like NAT -defined Function-like set
e2 is Element of the carrier' of G
(G,e2) is Relation-like NAT -defined the carrier of G -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of G *
the carrier of G * is functional non empty FinSequence-membered M16( the carrier of G)
e1 is Element of the carrier' of X
X2 . e1 is set
(X,e1) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
(X,e1) * c₃ is Relation-like NAT -defined Function-like set
e2 is Element of the carrier of X
(X,e1,e2) is Element of the carrier' of X
the of X is Relation-like [: the carrier of X, the carrier' of X:] -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of X, the carrier' of X:], the carrier' of X:]
[: the carrier of X, the carrier' of X:] is Relation-like non empty set
[:[: the carrier of X, the carrier' of X:], the carrier' of X:] is Relation-like non empty set
bool [:[: the carrier of X, the carrier' of X:], the carrier' of X:] is non empty set
the of X . (e2,e1) is Element of the carrier' of X
[e2,e1] is set
{e2,e1} is non empty set
{e2} is non empty trivial V53(1) set
{{e2,e1},{e2}} is non empty set
the of X . [e2,e1] is set
X2 . (X,e1,e2) is set
(X,(X,e1,e2)) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
(X,(X,e1,e2)) * c₃ is Relation-like NAT -defined Function-like set
q2 is Element of the carrier' of G
(G,q2) is Relation-like NAT -defined the carrier of G -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of G *
the carrier of G * is functional non empty FinSequence-membered M16( the carrier of G)
s1 is Relation-like the carrier' of X -defined the carrier' of G -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X, the carrier' of G:]
s1 . e1 is Element of the carrier' of G
(G,(s1 . e1)) is Relation-like NAT -defined the carrier of G -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of G *
A is Relation-like the carrier of X -defined the carrier of G -valued Function-like non empty total quasi_total Element of bool [: the carrier of X, the carrier of G:]
A . e2 is Element of the carrier of G
<*(A . e2)*> is Relation-like NAT -defined the carrier of G -valued Function-like constant non empty trivial V46() V53(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of G
[1,(A . e2)] is set
{1,(A . e2)} is non empty set
{1} is non empty trivial V53(1) set
{{1,(A . e2)},{1}} is non empty set
{[1,(A . e2)]} is Relation-like Function-like constant non empty trivial V53(1) set
<*e2*> is Relation-like NAT -defined the carrier of X -valued Function-like constant non empty trivial V46() V53(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of X
[1,e2] is set
{1,e2} is non empty set
{{1,e2},{1}} is non empty set
{[1,e2]} is Relation-like Function-like constant non empty trivial V53(1) set
<*e2*> * c₃ is Relation-like NAT -defined Function-like set
(G,(s1 . e1),(A . e2)) is Element of the carrier' of G
the of G is Relation-like [: the carrier of G, the carrier' of G:] -defined the carrier' of G -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of G, the carrier' of G:], the carrier' of G:]
[: the carrier of G, the carrier' of G:] is Relation-like non empty set
[:[: the carrier of G, the carrier' of G:], the carrier' of G:] is Relation-like non empty set
bool [:[: the carrier of G, the carrier' of G:], the carrier' of G:] is non empty set
the of G . ((A . e2),(s1 . e1)) is Element of the carrier' of G
[(A . e2),(s1 . e1)] is set
{(A . e2),(s1 . e1)} is non empty set
{(A . e2)} is non empty trivial V53(1) set
{{(A . e2),(s1 . e1)},{(A . e2)}} is non empty set
the of G . [(A . e2),(s1 . e1)] is set
( the carrier of G,<*(A . e2)*>,(G,(s1 . e1))) is Relation-like NAT -defined the carrier of G -valued Function-like non empty V46() FinSequence-like FinSubsequence-like Element of the carrier of G *
( the carrier of X,<*e2*>,(X,e1)) is Relation-like NAT -defined the carrier of X -valued Function-like non empty V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
( the carrier of X,<*e2*>,(X,e1)) * c₃ is Relation-like NAT -defined Function-like set
c₃ is non empty non void V67() () () () () () ()
the carrier of c₃ is non empty set
[: the carrier of c₃, the carrier of c₃:] is Relation-like non empty set
bool [: the carrier of c₃, the carrier of c₃:] is non empty set
id the carrier of c₃ is Relation-like the carrier of c₃ -defined the carrier of c₃ -valued Function-like one-to-one non empty total quasi_total onto bijective reflexive symmetric antisymmetric transitive Element of bool [: the carrier of c₃, the carrier of c₃:]
X2 is Relation-like the carrier of c₃ -defined the carrier of c₃ -valued Function-like one-to-one non empty total quasi_total onto bijective reflexive symmetric antisymmetric transitive Element of bool [: the carrier of c₃, the carrier of c₃:]
the carrier' of c₃ is non empty set
[: the carrier' of c₃, the carrier' of c₃:] is Relation-like non empty set
bool [: the carrier' of c₃, the carrier' of c₃:] is non empty set
id the carrier' of c₃ is Relation-like the carrier' of c₃ -defined the carrier' of c₃ -valued Function-like one-to-one non empty total quasi_total onto bijective reflexive symmetric antisymmetric transitive Element of bool [: the carrier' of c₃, the carrier' of c₃:]
A is Relation-like the carrier' of c₃ -defined the carrier' of c₃ -valued Function-like one-to-one non empty total quasi_total onto bijective reflexive symmetric antisymmetric transitive Element of bool [: the carrier' of c₃, the carrier' of c₃:]
c₃ is non empty non void V67() () () () () () ()
X2 is non empty non void V67() () () () () () ()
A is Relation-like Function-like set
s1 is Relation-like Function-like set
A " is Relation-like Function-like set
s1 " is Relation-like Function-like set
X is non empty non void V67() () () () () () ()
G is non empty non void V67() () () () () () ()
c₃ is non empty non void V67() () () () () () ()
X2 is Relation-like Function-like set
A is Relation-like Function-like set
s1 is Relation-like Function-like set
s2 is Relation-like Function-like set
X2 * s1 is Relation-like Function-like set
A * s2 is Relation-like Function-like set
X is non empty non void V67() () () () () () ()
G is non empty non void V67() () () () () () ()
c₃ is Relation-like Function-like set
X2 is Relation-like Function-like set
the carrier' of G is non empty set
A is Element of the carrier' of G
s1 is Element of the carrier' of G
dom X2 is set
the carrier' of X is non empty set
rng X2 is set
s2 is set
X2 . s2 is set
e1 is set
X2 . e1 is set
dom c₃ is set
the carrier of X is non empty set
rng c₃ is set
the carrier of G is non empty set
e2 is Element of the carrier' of X
(X,e2) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
the carrier of X * is functional non empty FinSequence-membered M16( the carrier of X)
rng (X,e2) is Element of bool the carrier of X
bool the carrier of X is non empty set
q2 is Element of the carrier' of X
(X,q2) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
rng (X,q2) is Element of bool the carrier of X
(G,A) is Relation-like NAT -defined the carrier of G -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of G *
the carrier of G * is functional non empty FinSequence-membered M16( the carrier of G)
(G,s1) is Relation-like NAT -defined the carrier of G -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of G *
(X,e2) * c₃ is Relation-like NAT -defined Function-like set
(X,q2) * c₃ is Relation-like NAT -defined Function-like set
dom ((X,e2) * c₃) is Element of bool NAT
dom (X,e2) is Element of bool NAT
dom ((X,q2) * c₃) is Element of bool NAT
dom (X,q2) is Element of bool NAT
X is non empty non void V67() () () () () () () ()
the carrier' of X is non empty set
the carrier of X is non empty set
( the carrier of X) is non empty non void V67() () () () () () () () ()
id the carrier of X is Relation-like the carrier of X -defined the carrier of X -valued Function-like one-to-one non empty total quasi_total onto bijective reflexive symmetric antisymmetric transitive Element of bool [: the carrier of X, the carrier of X:]
[: the carrier of X, the carrier of X:] is Relation-like non empty set
bool [: the carrier of X, the carrier of X:] is non empty set
the carrier of X * is functional non empty FinSequence-membered M16( the carrier of X)
[: the carrier' of X,( the carrier of X *):] is Relation-like non empty set
bool [: the carrier' of X,( the carrier of X *):] is non empty set
G is Relation-like the carrier' of X -defined the carrier of X * -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X,( the carrier of X *):]
c₃ is Element of the carrier' of X
G . c₃ is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
(X,c₃) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
the carrier of ( the carrier of X) is non empty set
the carrier' of ( the carrier of X) is functional non empty set
the Element of the carrier of ( the carrier of X) is Element of the carrier of ( the carrier of X)
s1 is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier' of ( the carrier of X)
s2 is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier' of ( the carrier of X)
e2 is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like set
e1 is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier' of ( the carrier of X)
(( the carrier of X),e1) is Element of the carrier of ( the carrier of X)
the of ( the carrier of X) is Relation-like the carrier' of ( the carrier of X) -defined the carrier of ( the carrier of X) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of ( the carrier of X), the carrier of ( the carrier of X):]
[: the carrier' of ( the carrier of X), the carrier of ( the carrier of X):] is Relation-like non empty set
bool [: the carrier' of ( the carrier of X), the carrier of ( the carrier of X):] is non empty set
the of ( the carrier of X) . e1 is Element of the carrier of ( the carrier of X)
e2 . 1 is set
(( the carrier of X),e1) is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier' of ( the carrier of X)
the of ( the carrier of X) is Relation-like the carrier' of ( the carrier of X) -defined the carrier' of ( the carrier of X) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of ( the carrier of X), the carrier' of ( the carrier of X):]
[: the carrier' of ( the carrier of X), the carrier' of ( the carrier of X):] is Relation-like non empty set
bool [: the carrier' of ( the carrier of X), the carrier' of ( the carrier of X):] is non empty set
the of ( the carrier of X) . e1 is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier' of ( the carrier of X)
Del (e2,1) is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like set
q2 is Element of the carrier of ( the carrier of X)
(( the carrier of X),e1,q2) is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier' of ( the carrier of X)
the of ( the carrier of X) is Relation-like [: the carrier of ( the carrier of X), the carrier' of ( the carrier of X):] -defined the carrier' of ( the carrier of X) -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of ( the carrier of X), the carrier' of ( the carrier of X):], the carrier' of ( the carrier of X):]
[: the carrier of ( the carrier of X), the carrier' of ( the carrier of X):] is Relation-like non empty set
[:[: the carrier of ( the carrier of X), the carrier' of ( the carrier of X):], the carrier' of ( the carrier of X):] is Relation-like non empty set
bool [:[: the carrier of ( the carrier of X), the carrier' of ( the carrier of X):], the carrier' of ( the carrier of X):] is non empty set
the of ( the carrier of X) . (q2,e1) is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier' of ( the carrier of X)
[q2,e1] is set
{q2,e1} is non empty set
{q2} is non empty trivial V53(1) set
{{q2,e1},{q2}} is non empty set
the of ( the carrier of X) . [q2,e1] is Relation-like Function-like set
<*q2*> is Relation-like NAT -defined the carrier of ( the carrier of X) -valued Function-like constant non empty trivial V46() V53(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of ( the carrier of X)
[1,q2] is set
{1,q2} is non empty set
{1} is non empty trivial V53(1) set
{{1,q2},{1}} is non empty set
{[1,q2]} is Relation-like Function-like constant non empty trivial V53(1) set
<*q2*> ^ e2 is Relation-like NAT -defined Function-like non empty V46() FinSequence-like FinSubsequence-like set
dom (id the carrier of X) is non empty Element of bool the carrier of X
bool the carrier of X is non empty set
rng (id the carrier of X) is non empty Element of bool the carrier of X
dom G is non empty set
rng G is non empty set
dom G is non empty Element of bool the carrier' of X
bool the carrier' of X is non empty set
rng G is functional non empty FinSequence-membered Element of bool ( the carrier of X *)
bool ( the carrier of X *) is non empty set
s1 is set
s2 is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
e1 is Element of the carrier' of X
(X,e1) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
G . e1 is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
s1 is set
G . s1 is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like set
s2 is set
G . s2 is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like set
e1 is Element of the carrier' of X
(X,e1) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
e2 is Element of the carrier' of X
(X,e2) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
s1 is Element of the carrier' of X
G . s1 is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like set
(X,s1) is Element of the carrier' of X
the of X is Relation-like the carrier' of X -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X, the carrier' of X:]
[: the carrier' of X, the carrier' of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier' of X:] is non empty set
the of X . s1 is Element of the carrier' of X
G . (X,s1) is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like set
(X,s1) is Element of the carrier of X
the of X is Relation-like the carrier' of X -defined the carrier of X -valued Function-like non empty total quasi_total Element of bool [: the carrier' of X, the carrier of X:]
[: the carrier' of X, the carrier of X:] is Relation-like non empty set
bool [: the carrier' of X, the carrier of X:] is non empty set
the of X . s1 is Element of the carrier of X
(id the carrier of X) . (X,s1) is set
s2 is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier' of ( the carrier of X)
(( the carrier of X),s2) is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier' of ( the carrier of X)
the of ( the carrier of X) is Relation-like the carrier' of ( the carrier of X) -defined the carrier' of ( the carrier of X) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of ( the carrier of X), the carrier' of ( the carrier of X):]
[: the carrier' of ( the carrier of X), the carrier' of ( the carrier of X):] is Relation-like non empty set
bool [: the carrier' of ( the carrier of X), the carrier' of ( the carrier of X):] is non empty set
the of ( the carrier of X) . s2 is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier' of ( the carrier of X)
(( the carrier of X),s2) is Element of the carrier of ( the carrier of X)
the of ( the carrier of X) is Relation-like the carrier' of ( the carrier of X) -defined the carrier of ( the carrier of X) -valued Function-like non empty total quasi_total Element of bool [: the carrier' of ( the carrier of X), the carrier of ( the carrier of X):]
[: the carrier' of ( the carrier of X), the carrier of ( the carrier of X):] is Relation-like non empty set
bool [: the carrier' of ( the carrier of X), the carrier of ( the carrier of X):] is non empty set
the of ( the carrier of X) . s2 is Element of the carrier of ( the carrier of X)
G . s1 is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
(X,s1) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
Del (s2,1) is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like set
(X,(X,s1)) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
G . (X,s1) is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
s2 . 1 is set
(id the carrier of X) . (X,s1) is Element of the carrier of X
e1 is Element of the carrier of X
(id the carrier of X) . e1 is set
(X,s1,e1) is Element of the carrier' of X
the of X is Relation-like [: the carrier of X, the carrier' of X:] -defined the carrier' of X -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of X, the carrier' of X:], the carrier' of X:]
[: the carrier of X, the carrier' of X:] is Relation-like non empty set
[:[: the carrier of X, the carrier' of X:], the carrier' of X:] is Relation-like non empty set
bool [:[: the carrier of X, the carrier' of X:], the carrier' of X:] is non empty set
the of X . (e1,s1) is Element of the carrier' of X
[e1,s1] is set
{e1,s1} is non empty set
{e1} is non empty trivial V53(1) set
{{e1,s1},{e1}} is non empty set
the of X . [e1,s1] is set
G . (X,s1,e1) is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like set
e2 is Element of the carrier of ( the carrier of X)
(( the carrier of X),s2,e2) is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier' of ( the carrier of X)
the of ( the carrier of X) is Relation-like [: the carrier of ( the carrier of X), the carrier' of ( the carrier of X):] -defined the carrier' of ( the carrier of X) -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of ( the carrier of X), the carrier' of ( the carrier of X):], the carrier' of ( the carrier of X):]
[: the carrier of ( the carrier of X), the carrier' of ( the carrier of X):] is Relation-like non empty set
[:[: the carrier of ( the carrier of X), the carrier' of ( the carrier of X):], the carrier' of ( the carrier of X):] is Relation-like non empty set
bool [:[: the carrier of ( the carrier of X), the carrier' of ( the carrier of X):], the carrier' of ( the carrier of X):] is non empty set
the of ( the carrier of X) . (e2,s2) is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier' of ( the carrier of X)
[e2,s2] is set
{e2,s2} is non empty set
{e2} is non empty trivial V53(1) set
{{e2,s2},{e2}} is non empty set
the of ( the carrier of X) . [e2,s2] is Relation-like Function-like set
(id the carrier of X) . e1 is Element of the carrier of X
<*((id the carrier of X) . e1)*> is Relation-like NAT -defined the carrier of X -valued Function-like constant non empty trivial V46() V53(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of X
[1,((id the carrier of X) . e1)] is set
{1,((id the carrier of X) . e1)} is non empty set
{1} is non empty trivial V53(1) set
{{1,((id the carrier of X) . e1)},{1}} is non empty set
{[1,((id the carrier of X) . e1)]} is Relation-like Function-like constant non empty trivial V53(1) set
<*((id the carrier of X) . e1)*> ^ s2 is Relation-like NAT -defined Function-like non empty V46() FinSequence-like FinSubsequence-like set
<*e1*> is Relation-like NAT -defined the carrier of X -valued Function-like constant non empty trivial V46() V53(1) FinSequence-like FinSubsequence-like FinSequence of the carrier of X
[1,e1] is set
{1,e1} is non empty set
{{1,e1},{1}} is non empty set
{[1,e1]} is Relation-like Function-like constant non empty trivial V53(1) set
<*e1*> ^ s2 is Relation-like NAT -defined Function-like non empty V46() FinSequence-like FinSubsequence-like set
(X,(X,s1,e1)) is Relation-like NAT -defined the carrier of X -valued Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
G . (X,s1,e1) is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like Element of the carrier of X *
X is non empty non void V67() () () () () () () ()
the carrier of X is non empty set
( the carrier of X) is non empty non void V67() () () () () () () () ()
the carrier' of X is non empty set
id the carrier of X is Relation-like the carrier of X -defined the carrier of X -valued Function-like one-to-one non empty total quasi_total onto bijective reflexive symmetric antisymmetric transitive Element of bool [: the carrier of X, the carrier of X:]
[: the carrier of X, the carrier of X:] is Relation-like non empty set
bool [: the carrier of X, the carrier of X:] is non empty set
G is Relation-like Function-like set