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