:: HEYTING3 semantic presentation

REAL is V143() V144() V145() V149() V156() V157() V159() set
NAT is non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() Element of bool REAL
bool REAL is non empty cup-closed diff-closed preBoolean set
NAT is non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() set
bool NAT is non empty V107() cup-closed diff-closed preBoolean set
bool NAT is non empty V107() cup-closed diff-closed preBoolean set
COMPLEX is V143() V149() set
RAT is V143() V144() V145() V146() V149() set
INT is V143() V144() V145() V146() V147() V149() set
{} is Relation-like non-empty empty-yielding functional empty V35() V36() V37() V39() V40() V41() finite finite-yielding V48() FinSequence-like FinSequence-membered ext-real non positive non negative V143() V144() V145() V146() V147() V148() V149() V156() V157() V158() V159() set
the Relation-like non-empty empty-yielding functional empty V35() V36() V37() V39() V40() V41() finite finite-yielding V48() FinSequence-like FinSequence-membered ext-real non positive non negative V143() V144() V145() V146() V147() V148() V149() V156() V157() V158() V159() set is Relation-like non-empty empty-yielding functional empty V35() V36() V37() V39() V40() V41() finite finite-yielding V48() FinSequence-like FinSequence-membered ext-real non positive non negative V143() V144() V145() V146() V147() V148() V149() V156() V157() V158() V159() set
1 is non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
2 is non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
3 is non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
0 is Relation-like non-empty empty-yielding functional empty V35() V36() V37() V39() V40() V41() V42() V43() finite finite-yielding V48() FinSequence-like FinSequence-membered V128() V129() ext-real non positive non negative V143() V144() V145() V146() V147() V148() V149() V156() V157() V158() V159() Element of NAT
{{}} is non empty finite V48() V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
F₁() is 1-sorted
the carrier of F₁() is set
bool the carrier of F₁() is non empty cup-closed diff-closed preBoolean set
m is Element of bool the carrier of F₁()
K is Element of bool the carrier of F₁()
a is set
a is set
m is set
K is set
{K} is non empty finite set
[:m,{K}:] is Relation-like set
a9 is set
Mi is set
[a9,Mi] is V15() set
{a9,Mi} is non empty finite set
{a9} is non empty finite set
{{a9,Mi},{a9}} is non empty finite V48() set
Mi is set
[a9,Mi] is V15() set
{a9,Mi} is non empty finite set
{{a9,Mi},{a9}} is non empty finite V48() set
m is set
K is set
{K} is non empty finite set
[:m,{K}:] is Relation-like set
2 * 0 is V35() V36() V37() V41() V42() V43() even V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
0 + 1 is non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
{0} is non empty finite V48() V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() Element of bool NAT
m is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() Element of bool NAT
max m is V35() V36() V37() V41() V42() V43() V128() ext-real non negative set
K is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
Seg K is finite V51(K) V143() V144() V145() V146() V147() V148() V156() V157() V158() Element of bool NAT
(Seg K) \/ {0} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() Element of bool NAT
a is set
a9 is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
m is finite V143() V144() V145() V146() V147() V148() V156() V157() V158() Element of bool NAT
K is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
Seg K is finite V51(K) V143() V144() V145() V146() V147() V148() V156() V157() V158() Element of bool NAT
(Seg K) \/ {0} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() Element of bool NAT
2 * K is V35() V36() V37() V41() V42() V43() even V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
(2 * K) + 1 is non empty V35() V36() V37() V41() V42() V43() non even V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
1 * K is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
m is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
{m} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() Element of bool NAT
[:NAT,{m}:] is Relation-like REAL -defined NAT -valued Function-like non empty Element of bool [:REAL,NAT:]
[:REAL,NAT:] is Relation-like set
bool [:REAL,NAT:] is non empty cup-closed diff-closed preBoolean set
bool [:NAT,{m}:] is non empty V107() cup-closed diff-closed preBoolean set
K is Relation-like REAL -defined NAT -valued non empty finite Element of bool [:NAT,{m}:]
dom K is non empty finite set
a is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() Element of bool NAT
max a is V35() V36() V37() V41() V42() V43() V128() ext-real non negative set
a9 is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
a9 + 1 is non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
Mi is non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
Seg Mi is non empty finite V51(Mi) V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() Element of bool NAT
(Seg Mi) \/ {0} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() Element of bool NAT
[:((Seg Mi) \/ {0}),{m}:] is Relation-like NAT -defined NAT -valued Function-like non empty finite Element of bool [:NAT,NAT:]
[:NAT,NAT:] is Relation-like non empty set
bool [:NAT,NAT:] is non empty V107() cup-closed diff-closed preBoolean set
Mi is set
mX is set
Sum is set
[mX,Sum] is V15() set
{mX,Sum} is non empty finite set
{mX} is non empty finite set
{{mX,Sum},{mX}} is non empty finite V48() set
Mi `1 is set
[mX,Sum] `1 is set
b is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
m is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
{m} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() Element of bool NAT
[:NAT,{m}:] is Relation-like REAL -defined NAT -valued Function-like non empty Element of bool [:REAL,NAT:]
[:REAL,NAT:] is Relation-like set
bool [:REAL,NAT:] is non empty cup-closed diff-closed preBoolean set
bool [:NAT,{m}:] is non empty V107() cup-closed diff-closed preBoolean set
K is Relation-like REAL -defined NAT -valued non empty finite Element of bool [:NAT,{m}:]
a is non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
Seg a is non empty finite V51(a) V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() Element of bool NAT
(Seg a) \/ {0} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() Element of bool NAT
[:((Seg a) \/ {0}),{m}:] is Relation-like NAT -defined NAT -valued Function-like non empty finite Element of bool [:NAT,NAT:]
[:NAT,NAT:] is Relation-like non empty set
bool [:NAT,NAT:] is non empty V107() cup-closed diff-closed preBoolean set
2 * a is V35() V36() V37() V41() V42() V43() even V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
(2 * a) + 1 is non empty V35() V36() V37() V41() V42() V43() non even V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
[((2 * a) + 1),m] is V15() Element of [:NAT,NAT:]
{((2 * a) + 1),m} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{((2 * a) + 1)} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{{((2 * a) + 1),m},{((2 * a) + 1)}} is non empty finite V48() set
1 * a is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
m is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
{m} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() Element of bool NAT
[:NAT,{m}:] is Relation-like REAL -defined NAT -valued Function-like non empty Element of bool [:REAL,NAT:]
[:REAL,NAT:] is Relation-like set
bool [:REAL,NAT:] is non empty cup-closed diff-closed preBoolean set
bool [:NAT,{m}:] is non empty V107() cup-closed diff-closed preBoolean set
K is Relation-like REAL -defined NAT -valued finite Element of bool [:NAT,{m}:]
a is Relation-like REAL -defined NAT -valued non empty finite Element of bool [:NAT,{m}:]
a9 is non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
Seg a9 is non empty finite V51(a9) V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() Element of bool NAT
(Seg a9) \/ {0} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() Element of bool NAT
[:((Seg a9) \/ {0}),{m}:] is Relation-like NAT -defined NAT -valued Function-like non empty finite Element of bool [:NAT,NAT:]
[:NAT,NAT:] is Relation-like non empty set
bool [:NAT,NAT:] is non empty V107() cup-closed diff-closed preBoolean set
a9 + 1 is non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
Mi is non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
Mi is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
[Mi,m] is V15() Element of [:NAT,NAT:]
{Mi,m} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{Mi} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{{Mi,m},{Mi}} is non empty finite V48() set
a is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
[a,m] is V15() Element of [:NAT,NAT:]
[:NAT,NAT:] is Relation-like non empty set
{a,m} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{a} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{{a,m},{a}} is non empty finite V48() set
m is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded LattStr
Top m is Element of the carrier of m
the carrier of m is non empty set
LattPOSet m is non empty strict reflexive transitive antisymmetric with_suprema with_infima upper-bounded RelStr
K262(m) is Relation-like the carrier of m -defined the carrier of m -valued total V26() V29() V33() Element of bool [: the carrier of m, the carrier of m:]
[: the carrier of m, the carrier of m:] is Relation-like non empty set
bool [: the carrier of m, the carrier of m:] is non empty V107() cup-closed diff-closed preBoolean set
RelStr(# the carrier of m,K262(m) #) is strict RelStr
Top (LattPOSet m) is Element of the carrier of (LattPOSet m)
the carrier of (LattPOSet m) is non empty set
% (Top (LattPOSet m)) is Element of the carrier of m
a is Element of the carrier of m
a % is Element of the carrier of (LattPOSet m)
(% (Top (LattPOSet m))) % is Element of the carrier of (LattPOSet m)
(% (Top (LattPOSet m))) "\/" a is Element of the carrier of m
a "\/" (% (Top (LattPOSet m))) is Element of the carrier of m
m is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded LattStr
Bottom m is Element of the carrier of m
the carrier of m is non empty set
LattPOSet m is non empty strict reflexive transitive antisymmetric with_suprema with_infima lower-bounded RelStr
K262(m) is Relation-like the carrier of m -defined the carrier of m -valued total V26() V29() V33() Element of bool [: the carrier of m, the carrier of m:]
[: the carrier of m, the carrier of m:] is Relation-like non empty set
bool [: the carrier of m, the carrier of m:] is non empty V107() cup-closed diff-closed preBoolean set
RelStr(# the carrier of m,K262(m) #) is strict RelStr
Bottom (LattPOSet m) is Element of the carrier of (LattPOSet m)
the carrier of (LattPOSet m) is non empty set
% (Bottom (LattPOSet m)) is Element of the carrier of m
(% (Bottom (LattPOSet m))) % is Element of the carrier of (LattPOSet m)
a is Element of the carrier of m
a % is Element of the carrier of (LattPOSet m)
(% (Bottom (LattPOSet m))) "/\" a is Element of the carrier of m
a "/\" (% (Bottom (LattPOSet m))) is Element of the carrier of m
m is set
K is finite set
PFuncs (m,K) is functional non empty set
Fin (PFuncs (m,K)) is non empty cup-closed diff-closed preBoolean set
a is finite Element of Fin (PFuncs (m,K))
a9 is finite Element of Fin (PFuncs (m,K))
a9 =>> a is finite Element of Fin (PFuncs (m,K))
Mi is set
[:a9,a:] is Relation-like finite set
bool [:a9,a:] is non empty finite V48() cup-closed diff-closed preBoolean set
Mi is Relation-like a9 -defined a -valued Function-like finite Element of bool [:a9,a:]
{ ((Mi . b₁) \ b₁) where b₁ is Element of PFuncs (m,K) : b₁ in a9 } is set
union { ((Mi . b₁) \ b₁) where b₁ is Element of PFuncs (m,K) : b₁ in a9 } is set
dom Mi is finite set
m is set
K is set
a is set
a9 is set
SubstitutionSet (m,a) is non empty Element of bool (Fin (PFuncs (m,a)))
PFuncs (m,a) is functional non empty set
Fin (PFuncs (m,a)) is non empty cup-closed diff-closed preBoolean set
bool (Fin (PFuncs (m,a))) is non empty V107() cup-closed diff-closed preBoolean set
SubstitutionSet (K,a9) is non empty Element of bool (Fin (PFuncs (K,a9)))
PFuncs (K,a9) is functional non empty set
Fin (PFuncs (K,a9)) is non empty cup-closed diff-closed preBoolean set
bool (Fin (PFuncs (K,a9))) is non empty V107() cup-closed diff-closed preBoolean set
Mi is set
{ b₁ where b₁ is finite Element of Fin (PFuncs (m,a)) : ( ( for b₂ being set holds
( not b₂ in b₁ or b₂ is finite ) ) & ( for b₂, b₃ being Element of PFuncs (m,a) holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) ) ) } is set
Mi is finite Element of Fin (PFuncs (m,a))
mX is finite Element of Fin (PFuncs (K,a9))
Sum is Element of PFuncs (K,a9)
b is Element of PFuncs (K,a9)
{ b₁ where b₁ is finite Element of Fin (PFuncs (K,a9)) : ( ( for b₂ being set holds
( not b₂ in b₁ or b₂ is finite ) ) & ( for b₂, b₃ being Element of PFuncs (K,a9) holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) ) ) } is set
m is set
a is set
PFuncs (m,a) is functional non empty set
Fin (PFuncs (m,a)) is non empty cup-closed diff-closed preBoolean set
K is set
a9 is set
PFuncs (K,a9) is functional non empty set
Fin (PFuncs (K,a9)) is non empty cup-closed diff-closed preBoolean set
Mi is finite Element of Fin (PFuncs (m,a))
mi Mi is functional finite Element of SubstitutionSet (m,a)
SubstitutionSet (m,a) is non empty Element of bool (Fin (PFuncs (m,a)))
bool (Fin (PFuncs (m,a))) is non empty V107() cup-closed diff-closed preBoolean set
Mi is finite Element of Fin (PFuncs (K,a9))
mi Mi is functional finite Element of SubstitutionSet (K,a9)
SubstitutionSet (K,a9) is non empty Element of bool (Fin (PFuncs (K,a9)))
bool (Fin (PFuncs (K,a9))) is non empty V107() cup-closed diff-closed preBoolean set
mX is set
{ b₁ where b₁ is Element of PFuncs (m,a) : ( b₁ is finite & ( for b₂ being Element of PFuncs (m,a) holds
( ( not b₂ in Mi or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in Mi & b₂ c= b₁ ) ) ) ) ) } is set
Sum is Element of PFuncs (m,a)
b is Element of PFuncs (K,a9)
g is Element of PFuncs (K,a9)
P1 is Element of PFuncs (K,a9)
{ b₁ where b₁ is Element of PFuncs (K,a9) : ( b₁ is finite & ( for b₂ being Element of PFuncs (K,a9) holds
( ( not b₂ in Mi or not b₂ c= b₁ or b₂ = b₁ ) & ( not b₂ = b₁ or ( b₂ in Mi & b₂ c= b₁ ) ) ) ) ) } is set
mX is set
b is Element of PFuncs (K,a9)
Sum is finite set
b is finite set
m is set
K is set
a is set
a9 is set
SubstLatt (m,a) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V99() LattStr
the L_join of (SubstLatt (m,a)) is Relation-like [: the carrier of (SubstLatt (m,a)), the carrier of (SubstLatt (m,a)):] -defined the carrier of (SubstLatt (m,a)) -valued Function-like V18([: the carrier of (SubstLatt (m,a)), the carrier of (SubstLatt (m,a)):], the carrier of (SubstLatt (m,a))) Element of bool [:[: the carrier of (SubstLatt (m,a)), the carrier of (SubstLatt (m,a)):], the carrier of (SubstLatt (m,a)):]
the carrier of (SubstLatt (m,a)) is non empty set
[: the carrier of (SubstLatt (m,a)), the carrier of (SubstLatt (m,a)):] is Relation-like non empty set
[:[: the carrier of (SubstLatt (m,a)), the carrier of (SubstLatt (m,a)):], the carrier of (SubstLatt (m,a)):] is Relation-like non empty set
bool [:[: the carrier of (SubstLatt (m,a)), the carrier of (SubstLatt (m,a)):], the carrier of (SubstLatt (m,a)):] is non empty V107() cup-closed diff-closed preBoolean set
SubstLatt (K,a9) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V99() LattStr
the L_join of (SubstLatt (K,a9)) is Relation-like [: the carrier of (SubstLatt (K,a9)), the carrier of (SubstLatt (K,a9)):] -defined the carrier of (SubstLatt (K,a9)) -valued Function-like V18([: the carrier of (SubstLatt (K,a9)), the carrier of (SubstLatt (K,a9)):], the carrier of (SubstLatt (K,a9))) Element of bool [:[: the carrier of (SubstLatt (K,a9)), the carrier of (SubstLatt (K,a9)):], the carrier of (SubstLatt (K,a9)):]
the carrier of (SubstLatt (K,a9)) is non empty set
[: the carrier of (SubstLatt (K,a9)), the carrier of (SubstLatt (K,a9)):] is Relation-like non empty set
[:[: the carrier of (SubstLatt (K,a9)), the carrier of (SubstLatt (K,a9)):], the carrier of (SubstLatt (K,a9)):] is Relation-like non empty set
bool [:[: the carrier of (SubstLatt (K,a9)), the carrier of (SubstLatt (K,a9)):], the carrier of (SubstLatt (K,a9)):] is non empty V107() cup-closed diff-closed preBoolean set
the L_join of (SubstLatt (K,a9)) || the carrier of (SubstLatt (m,a)) is Relation-like Function-like set
the L_join of (SubstLatt (K,a9)) | [: the carrier of (SubstLatt (m,a)), the carrier of (SubstLatt (m,a)):] is Relation-like [: the carrier of (SubstLatt (m,a)), the carrier of (SubstLatt (m,a)):] -defined [: the carrier of (SubstLatt (K,a9)), the carrier of (SubstLatt (K,a9)):] -defined the carrier of (SubstLatt (K,a9)) -valued set
SubstitutionSet (m,a) is non empty Element of bool (Fin (PFuncs (m,a)))
PFuncs (m,a) is functional non empty set
Fin (PFuncs (m,a)) is non empty cup-closed diff-closed preBoolean set
bool (Fin (PFuncs (m,a))) is non empty V107() cup-closed diff-closed preBoolean set
dom the L_join of (SubstLatt (K,a9)) is Relation-like set
SubstitutionSet (K,a9) is non empty Element of bool (Fin (PFuncs (K,a9)))
PFuncs (K,a9) is functional non empty set
Fin (PFuncs (K,a9)) is non empty cup-closed diff-closed preBoolean set
bool (Fin (PFuncs (K,a9))) is non empty V107() cup-closed diff-closed preBoolean set
dom ( the L_join of (SubstLatt (K,a9)) || the carrier of (SubstLatt (m,a))) is set
rng ( the L_join of (SubstLatt (K,a9)) || the carrier of (SubstLatt (m,a))) is set
b is set
g is set
( the L_join of (SubstLatt (K,a9)) || the carrier of (SubstLatt (m,a))) . g is set
P1 is set
x is set
[P1,x] is V15() set
{P1,x} is non empty finite set
{P1} is non empty finite set
{{P1,x},{P1}} is non empty finite V48() set
the L_join of (SubstLatt (K,a9)) . (P1,x) is set
the L_join of (SubstLatt (K,a9)) . [P1,x] is set
y is functional finite Element of SubstitutionSet (K,a9)
a1 is functional finite Element of SubstitutionSet (K,a9)
y \/ a1 is finite Element of Fin (PFuncs (K,a9))
mi (y \/ a1) is functional finite Element of SubstitutionSet (K,a9)
b1 is functional finite Element of SubstitutionSet (m,a)
y22 is functional finite Element of SubstitutionSet (m,a)
b1 \/ y22 is finite Element of Fin (PFuncs (m,a))
mi (b1 \/ y22) is functional finite Element of SubstitutionSet (m,a)
g is Element of the carrier of (SubstLatt (m,a))
P1 is Element of the carrier of (SubstLatt (m,a))
x is functional finite Element of SubstitutionSet (m,a)
y is functional finite Element of SubstitutionSet (m,a)
mX is Relation-like [: the carrier of (SubstLatt (m,a)), the carrier of (SubstLatt (m,a)):] -defined the carrier of (SubstLatt (m,a)) -valued Function-like V18([: the carrier of (SubstLatt (m,a)), the carrier of (SubstLatt (m,a)):], the carrier of (SubstLatt (m,a))) Element of bool [:[: the carrier of (SubstLatt (m,a)), the carrier of (SubstLatt (m,a)):], the carrier of (SubstLatt (m,a)):]
mX . (g,P1) is Element of the carrier of (SubstLatt (m,a))
[g,P1] is V15() set
{g,P1} is non empty finite set
{g} is non empty finite set
{{g,P1},{g}} is non empty finite V48() set
mX . [g,P1] is set
x \/ y is finite Element of Fin (PFuncs (m,a))
mi (x \/ y) is functional finite Element of SubstitutionSet (m,a)
a1 is functional finite Element of SubstitutionSet (K,a9)
b1 is functional finite Element of SubstitutionSet (K,a9)
a1 \/ b1 is finite Element of Fin (PFuncs (K,a9))
mi (a1 \/ b1) is functional finite Element of SubstitutionSet (K,a9)
the L_join of (SubstLatt (K,a9)) . (g,P1) is set
the L_join of (SubstLatt (K,a9)) . [g,P1] is set
b is Relation-like [: the carrier of (SubstLatt (m,a)), the carrier of (SubstLatt (m,a)):] -defined the carrier of (SubstLatt (m,a)) -valued Function-like V18([: the carrier of (SubstLatt (m,a)), the carrier of (SubstLatt (m,a)):], the carrier of (SubstLatt (m,a))) Element of bool [:[: the carrier of (SubstLatt (m,a)), the carrier of (SubstLatt (m,a)):], the carrier of (SubstLatt (m,a)):]
[g,P1] is V15() Element of [: the carrier of (SubstLatt (m,a)), the carrier of (SubstLatt (m,a)):]
b . [g,P1] is set
b . (g,P1) is Element of the carrier of (SubstLatt (m,a))
b . [g,P1] is set
m is set
K is set
SubstLatt (m,K) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V99() LattStr
LattPOSet (SubstLatt (m,K)) is non empty strict reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V118() RelStr
the carrier of (SubstLatt (m,K)) is non empty set
K262((SubstLatt (m,K))) is Relation-like the carrier of (SubstLatt (m,K)) -defined the carrier of (SubstLatt (m,K)) -valued total V26() V29() V33() Element of bool [: the carrier of (SubstLatt (m,K)), the carrier of (SubstLatt (m,K)):]
[: the carrier of (SubstLatt (m,K)), the carrier of (SubstLatt (m,K)):] is Relation-like non empty set
bool [: the carrier of (SubstLatt (m,K)), the carrier of (SubstLatt (m,K)):] is non empty V107() cup-closed diff-closed preBoolean set
RelStr(# the carrier of (SubstLatt (m,K)),K262((SubstLatt (m,K))) #) is strict RelStr
m is set
K is set
(m,K) is RelStr
SubstLatt (m,K) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V99() LattStr
LattPOSet (SubstLatt (m,K)) is non empty strict reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V118() RelStr
the carrier of (SubstLatt (m,K)) is non empty set
K262((SubstLatt (m,K))) is Relation-like the carrier of (SubstLatt (m,K)) -defined the carrier of (SubstLatt (m,K)) -valued total V26() V29() V33() Element of bool [: the carrier of (SubstLatt (m,K)), the carrier of (SubstLatt (m,K)):]
[: the carrier of (SubstLatt (m,K)), the carrier of (SubstLatt (m,K)):] is Relation-like non empty set
bool [: the carrier of (SubstLatt (m,K)), the carrier of (SubstLatt (m,K)):] is non empty V107() cup-closed diff-closed preBoolean set
RelStr(# the carrier of (SubstLatt (m,K)),K262((SubstLatt (m,K))) #) is strict RelStr
m is set
K is set
(m,K) is non empty with_suprema with_infima RelStr
SubstLatt (m,K) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V99() LattStr
LattPOSet (SubstLatt (m,K)) is non empty strict reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V118() RelStr
the carrier of (SubstLatt (m,K)) is non empty set
K262((SubstLatt (m,K))) is Relation-like the carrier of (SubstLatt (m,K)) -defined the carrier of (SubstLatt (m,K)) -valued total V26() V29() V33() Element of bool [: the carrier of (SubstLatt (m,K)), the carrier of (SubstLatt (m,K)):]
[: the carrier of (SubstLatt (m,K)), the carrier of (SubstLatt (m,K)):] is Relation-like non empty set
bool [: the carrier of (SubstLatt (m,K)), the carrier of (SubstLatt (m,K)):] is non empty V107() cup-closed diff-closed preBoolean set
RelStr(# the carrier of (SubstLatt (m,K)),K262((SubstLatt (m,K))) #) is strict RelStr
m is set
K is set
(m,K) is non empty reflexive transitive antisymmetric with_suprema with_infima RelStr
SubstLatt (m,K) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V99() LattStr
LattPOSet (SubstLatt (m,K)) is non empty strict reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V118() RelStr
the carrier of (SubstLatt (m,K)) is non empty set
K262((SubstLatt (m,K))) is Relation-like the carrier of (SubstLatt (m,K)) -defined the carrier of (SubstLatt (m,K)) -valued total V26() V29() V33() Element of bool [: the carrier of (SubstLatt (m,K)), the carrier of (SubstLatt (m,K)):]
[: the carrier of (SubstLatt (m,K)), the carrier of (SubstLatt (m,K)):] is Relation-like non empty set
bool [: the carrier of (SubstLatt (m,K)), the carrier of (SubstLatt (m,K)):] is non empty V107() cup-closed diff-closed preBoolean set
RelStr(# the carrier of (SubstLatt (m,K)),K262((SubstLatt (m,K))) #) is strict RelStr
the carrier of (m,K) is non empty set
a is Element of the carrier of (m,K)
a9 is Element of the carrier of (m,K)
PFuncs (m,K) is functional non empty set
Fin (PFuncs (m,K)) is non empty cup-closed diff-closed preBoolean set
SubstitutionSet (m,K) is non empty Element of bool (Fin (PFuncs (m,K)))
bool (Fin (PFuncs (m,K))) is non empty V107() cup-closed diff-closed preBoolean set
Mi is Element of the carrier of (SubstLatt (m,K))
Mi % is Element of the carrier of (LattPOSet (SubstLatt (m,K)))
the carrier of (LattPOSet (SubstLatt (m,K))) is non empty set
Mi is Element of the carrier of (SubstLatt (m,K))
Mi % is Element of the carrier of (LattPOSet (SubstLatt (m,K)))
Mi "/\" Mi is Element of the carrier of (SubstLatt (m,K))
the L_meet of (SubstLatt (m,K)) is Relation-like [: the carrier of (SubstLatt (m,K)), the carrier of (SubstLatt (m,K)):] -defined the carrier of (SubstLatt (m,K)) -valued Function-like V18([: the carrier of (SubstLatt (m,K)), the carrier of (SubstLatt (m,K)):], the carrier of (SubstLatt (m,K))) Element of bool [:[: the carrier of (SubstLatt (m,K)), the carrier of (SubstLatt (m,K)):], the carrier of (SubstLatt (m,K)):]
[:[: the carrier of (SubstLatt (m,K)), the carrier of (SubstLatt (m,K)):], the carrier of (SubstLatt (m,K)):] is Relation-like non empty set
bool [:[: the carrier of (SubstLatt (m,K)), the carrier of (SubstLatt (m,K)):], the carrier of (SubstLatt (m,K)):] is non empty V107() cup-closed diff-closed preBoolean set
the L_meet of (SubstLatt (m,K)) . (Mi,Mi) is Element of the carrier of (SubstLatt (m,K))
[Mi,Mi] is V15() set
{Mi,Mi} is non empty finite set
{Mi} is non empty finite set
{{Mi,Mi},{Mi}} is non empty finite V48() set
the L_meet of (SubstLatt (m,K)) . [Mi,Mi] is set
mX is functional finite Element of SubstitutionSet (m,K)
Sum is functional finite Element of SubstitutionSet (m,K)
mX ^ Sum is finite Element of Fin (PFuncs (m,K))
mi (mX ^ Sum) is functional finite Element of SubstitutionSet (m,K)
b is set
m is set
K is set
a is set
a9 is set
(m,a) is non empty reflexive transitive antisymmetric with_suprema with_infima RelStr
SubstLatt (m,a) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V99() LattStr
LattPOSet (SubstLatt (m,a)) is non empty strict reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V118() RelStr
the carrier of (SubstLatt (m,a)) is non empty set
K262((SubstLatt (m,a))) is Relation-like the carrier of (SubstLatt (m,a)) -defined the carrier of (SubstLatt (m,a)) -valued total V26() V29() V33() Element of bool [: the carrier of (SubstLatt (m,a)), the carrier of (SubstLatt (m,a)):]
[: the carrier of (SubstLatt (m,a)), the carrier of (SubstLatt (m,a)):] is Relation-like non empty set
bool [: the carrier of (SubstLatt (m,a)), the carrier of (SubstLatt (m,a)):] is non empty V107() cup-closed diff-closed preBoolean set
RelStr(# the carrier of (SubstLatt (m,a)),K262((SubstLatt (m,a))) #) is strict RelStr
(K,a9) is non empty reflexive transitive antisymmetric with_suprema with_infima RelStr
SubstLatt (K,a9) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V99() LattStr
LattPOSet (SubstLatt (K,a9)) is non empty strict reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V118() RelStr
the carrier of (SubstLatt (K,a9)) is non empty set
K262((SubstLatt (K,a9))) is Relation-like the carrier of (SubstLatt (K,a9)) -defined the carrier of (SubstLatt (K,a9)) -valued total V26() V29() V33() Element of bool [: the carrier of (SubstLatt (K,a9)), the carrier of (SubstLatt (K,a9)):]
[: the carrier of (SubstLatt (K,a9)), the carrier of (SubstLatt (K,a9)):] is Relation-like non empty set
bool [: the carrier of (SubstLatt (K,a9)), the carrier of (SubstLatt (K,a9)):] is non empty V107() cup-closed diff-closed preBoolean set
RelStr(# the carrier of (SubstLatt (K,a9)),K262((SubstLatt (K,a9))) #) is strict RelStr
the carrier of (m,a) is non empty set
SubstitutionSet (m,a) is non empty Element of bool (Fin (PFuncs (m,a)))
PFuncs (m,a) is functional non empty set
Fin (PFuncs (m,a)) is non empty cup-closed diff-closed preBoolean set
bool (Fin (PFuncs (m,a))) is non empty V107() cup-closed diff-closed preBoolean set
the carrier of (K,a9) is non empty set
SubstitutionSet (K,a9) is non empty Element of bool (Fin (PFuncs (K,a9)))
PFuncs (K,a9) is functional non empty set
Fin (PFuncs (K,a9)) is non empty cup-closed diff-closed preBoolean set
bool (Fin (PFuncs (K,a9))) is non empty V107() cup-closed diff-closed preBoolean set
mX is set
Sum is set
[mX,Sum] is V15() set
{mX,Sum} is non empty finite set
{mX} is non empty finite set
{{mX,Sum},{mX}} is non empty finite V48() set
the InternalRel of (m,a) is Relation-like the carrier of (m,a) -defined the carrier of (m,a) -valued Element of bool [: the carrier of (m,a), the carrier of (m,a):]
[: the carrier of (m,a), the carrier of (m,a):] is Relation-like non empty set
bool [: the carrier of (m,a), the carrier of (m,a):] is non empty V107() cup-closed diff-closed preBoolean set
b is Element of the carrier of (m,a)
g is Element of the carrier of (m,a)
y is set
P1 is Element of the carrier of (K,a9)
x is Element of the carrier of (K,a9)
the InternalRel of (K,a9) is Relation-like the carrier of (K,a9) -defined the carrier of (K,a9) -valued Element of bool [: the carrier of (K,a9), the carrier of (K,a9):]
[: the carrier of (K,a9), the carrier of (K,a9):] is Relation-like non empty set
bool [: the carrier of (K,a9), the carrier of (K,a9):] is non empty V107() cup-closed diff-closed preBoolean set
Sum is set
b is set
[Sum,b] is V15() set
{Sum,b} is non empty finite set
{Sum} is non empty finite set
{{Sum,b},{Sum}} is non empty finite V48() set
mX is SubRelStr of (K,a9)
the carrier of mX is set
the InternalRel of (K,a9) |_2 the carrier of mX is Relation-like set
[: the carrier of mX, the carrier of mX:] is Relation-like set
the InternalRel of (K,a9) /\ [: the carrier of mX, the carrier of mX:] is Relation-like the carrier of (K,a9) -defined the carrier of (K,a9) -valued set
g is Element of the carrier of (K,a9)
P1 is Element of the carrier of (K,a9)
a1 is set
x is Element of the carrier of mX
y is Element of the carrier of mX
the InternalRel of mX is Relation-like the carrier of mX -defined the carrier of mX -valued Element of bool [: the carrier of mX, the carrier of mX:]
bool [: the carrier of mX, the carrier of mX:] is non empty cup-closed diff-closed preBoolean set
Sum is set
b is set
[Sum,b] is V15() set
{Sum,b} is non empty finite set
{Sum} is non empty finite set
{{Sum,b},{Sum}} is non empty finite V48() set
g is Element of the carrier of mX
P1 is Element of the carrier of mX
a1 is set
x is Element of the carrier of (K,a9)
y is Element of the carrier of (K,a9)
[x,y] is V15() Element of [: the carrier of (K,a9), the carrier of (K,a9):]
{x,y} is non empty finite set
{x} is non empty finite set
{{x,y},{x}} is non empty finite V48() set
K is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
{K} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() Element of bool NAT
PFuncs (NAT,{K}) is functional non empty set
m is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
2 * m is V35() V36() V37() V41() V42() V43() even V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
[(2 * m),K] is V15() Element of [:NAT,NAT:]
[:NAT,NAT:] is Relation-like non empty set
{(2 * m),K} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{(2 * m)} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{{(2 * m),K},{(2 * m)}} is non empty finite V48() set
[:NAT,{K}:] is Relation-like REAL -defined NAT -valued Function-like non empty Element of bool [:REAL,NAT:]
[:REAL,NAT:] is Relation-like set
bool [:REAL,NAT:] is non empty cup-closed diff-closed preBoolean set
a is set
a9 is set
a9 is Relation-like Function-like set
dom a9 is set
rng a9 is set
Mi is Element of PFuncs (NAT,{K})
Mi is set
mX is non empty V35() V36() V37() V41() V42() V43() non even V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
[mX,K] is V15() Element of [:NAT,NAT:]
{mX,K} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{mX} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{{mX,K},{mX}} is non empty finite V48() set
mX is non empty V35() V36() V37() V41() V42() V43() non even V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
[mX,K] is V15() Element of [:NAT,NAT:]
{mX,K} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{mX} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{{mX,K},{mX}} is non empty finite V48() set
mX is non empty V35() V36() V37() V41() V42() V43() non even V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
[mX,K] is V15() Element of [:NAT,NAT:]
{mX,K} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{mX} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{{mX,K},{mX}} is non empty finite V48() set
a is Element of PFuncs (NAT,{K})
a9 is Element of PFuncs (NAT,{K})
m is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
K is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
(m,K) is Element of PFuncs (NAT,{K})
{K} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() Element of bool NAT
PFuncs (NAT,{K}) is functional non empty set
2 * m is V35() V36() V37() V41() V42() V43() even V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
Seg (2 * m) is finite V51(2 * m) V143() V144() V145() V146() V147() V148() V156() V157() V158() Element of bool NAT
(Seg (2 * m)) \/ {0} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() Element of bool NAT
[:((Seg (2 * m)) \/ {0}),{K}:] is Relation-like NAT -defined NAT -valued Function-like non empty finite Element of bool [:NAT,NAT:]
bool [:NAT,NAT:] is non empty V107() cup-closed diff-closed preBoolean set
a is set
a9 is non empty V35() V36() V37() V41() V42() V43() non even V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
[a9,K] is V15() Element of [:NAT,NAT:]
{a9,K} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{a9} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{{a9,K},{a9}} is non empty finite V48() set
a9 is non empty V35() V36() V37() V41() V42() V43() non even V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
[a9,K] is V15() Element of [:NAT,NAT:]
{a9,K} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{a9} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{{a9,K},{a9}} is non empty finite V48() set
[(2 * m),K] is V15() Element of [:NAT,NAT:]
{(2 * m),K} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{(2 * m)} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{{(2 * m),K},{(2 * m)}} is non empty finite V48() set
[(2 * m),K] is V15() Element of [:NAT,NAT:]
{(2 * m),K} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{(2 * m)} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{{(2 * m),K},{(2 * m)}} is non empty finite V48() set
K is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
{K} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() Element of bool NAT
PFuncs (NAT,{K}) is functional non empty set
m is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
2 * m is V35() V36() V37() V41() V42() V43() even V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
(2 * m) + 1 is non empty V35() V36() V37() V41() V42() V43() non even V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
[:NAT,{K}:] is Relation-like REAL -defined NAT -valued Function-like non empty Element of bool [:REAL,NAT:]
[:REAL,NAT:] is Relation-like set
bool [:REAL,NAT:] is non empty cup-closed diff-closed preBoolean set
a is set
a9 is set
a9 is Relation-like Function-like set
dom a9 is set
rng a9 is set
Mi is Element of PFuncs (NAT,{K})
Mi is set
mX is non empty V35() V36() V37() V41() V42() V43() non even V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
[mX,K] is V15() Element of [:NAT,NAT:]
{mX,K} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{mX} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{{mX,K},{mX}} is non empty finite V48() set
a is Element of PFuncs (NAT,{K})
a9 is Element of PFuncs (NAT,{K})
m is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
K is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
(m,K) is Element of PFuncs (NAT,{K})
{K} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() Element of bool NAT
PFuncs (NAT,{K}) is functional non empty set
2 * m is V35() V36() V37() V41() V42() V43() even V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
(2 * m) + 1 is non empty V35() V36() V37() V41() V42() V43() non even V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
Seg ((2 * m) + 1) is non empty finite V51((2 * m) + 1) V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() Element of bool NAT
[:(Seg ((2 * m) + 1)),{K}:] is Relation-like NAT -defined NAT -valued Function-like non empty finite Element of bool [:NAT,NAT:]
bool [:NAT,NAT:] is non empty V107() cup-closed diff-closed preBoolean set
a9 is set
Mi is non empty V35() V36() V37() V41() V42() V43() non even V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
[Mi,K] is V15() Element of [:NAT,NAT:]
{Mi,K} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{Mi} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{{Mi,K},{Mi}} is non empty finite V48() set
m is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
2 * m is V35() V36() V37() V41() V42() V43() even V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
(2 * m) + 1 is non empty V35() V36() V37() V41() V42() V43() non even V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
K is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
[((2 * m) + 1),K] is V15() Element of [:NAT,NAT:]
{((2 * m) + 1),K} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{((2 * m) + 1)} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{{((2 * m) + 1),K},{((2 * m) + 1)}} is non empty finite V48() set
(m,K) is finite Element of PFuncs (NAT,{K})
{K} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() Element of bool NAT
PFuncs (NAT,{K}) is functional non empty set
m is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
K is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
(m,K) is finite Element of PFuncs (NAT,{K})
{K} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() Element of bool NAT
PFuncs (NAT,{K}) is functional non empty set
2 * m is V35() V36() V37() V41() V42() V43() even V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
(2 * m) + 3 is non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
[((2 * m) + 3),K] is V15() Element of [:NAT,NAT:]
{((2 * m) + 3),K} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{((2 * m) + 3)} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{{((2 * m) + 3),K},{((2 * m) + 3)}} is non empty finite V48() set
{[((2 * m) + 3),K]} is Relation-like NAT -defined NAT -valued non empty finite Element of bool [:NAT,NAT:]
bool [:NAT,NAT:] is non empty V107() cup-closed diff-closed preBoolean set
(m,K) /\ {[((2 * m) + 3),K]} is Relation-like NAT -defined NAT -valued finite Element of bool [:NAT,NAT:]
a is set
(2 * m) + 1 is non empty V35() V36() V37() V41() V42() V43() non even V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
a9 is non empty V35() V36() V37() V41() V42() V43() non even V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
[a9,K] is V15() Element of [:NAT,NAT:]
{a9,K} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{a9} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{{a9,K},{a9}} is non empty finite V48() set
m is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
2 * m is V35() V36() V37() V41() V42() V43() even V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
(2 * m) + 1 is non empty V35() V36() V37() V41() V42() V43() non even V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
m + 1 is non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
2 * (m + 1) is V35() V36() V37() V41() V42() V43() even V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
(2 * (m + 1)) + 1 is non empty V35() V36() V37() V41() V42() V43() non even V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
((2 * m) + 1) + 2 is non empty V35() V36() V37() V41() V42() V43() non even V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
m is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
m + 1 is non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
K is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
((m + 1),K) is finite Element of PFuncs (NAT,{K})
{K} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() Element of bool NAT
PFuncs (NAT,{K}) is functional non empty set
(m,K) is finite Element of PFuncs (NAT,{K})
2 * m is V35() V36() V37() V41() V42() V43() even V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
(2 * m) + 3 is non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
[((2 * m) + 3),K] is V15() Element of [:NAT,NAT:]
{((2 * m) + 3),K} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{((2 * m) + 3)} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{{((2 * m) + 3),K},{((2 * m) + 3)}} is non empty finite V48() set
{[((2 * m) + 3),K]} is Relation-like NAT -defined NAT -valued non empty finite Element of bool [:NAT,NAT:]
bool [:NAT,NAT:] is non empty V107() cup-closed diff-closed preBoolean set
(m,K) \/ {[((2 * m) + 3),K]} is non empty finite set
2 * (m + 1) is V35() V36() V37() V41() V42() V43() even V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
(2 * (m + 1)) + 1 is non empty V35() V36() V37() V41() V42() V43() non even V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
a is set
a9 is non empty V35() V36() V37() V41() V42() V43() non even V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
[a9,K] is V15() Element of [:NAT,NAT:]
{a9,K} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{a9} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{{a9,K},{a9}} is non empty finite V48() set
(2 * m) + 1 is non empty V35() V36() V37() V41() V42() V43() non even V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
((2 * m) + 1) + 1 is non empty V35() V36() V37() V41() V42() V43() even V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
a is set
(2 * m) + 1 is non empty V35() V36() V37() V41() V42() V43() non even V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
a9 is non empty V35() V36() V37() V41() V42() V43() non even V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
[a9,K] is V15() Element of [:NAT,NAT:]
{a9,K} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{a9} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{{a9,K},{a9}} is non empty finite V48() set
m is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
m + 1 is non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
K is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
((m + 1),K) is finite Element of PFuncs (NAT,{K})
{K} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() Element of bool NAT
PFuncs (NAT,{K}) is functional non empty set
(m,K) is finite Element of PFuncs (NAT,{K})
2 * m is V35() V36() V37() V41() V42() V43() even V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
(2 * m) + 3 is non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
[((2 * m) + 3),K] is V15() Element of [:NAT,NAT:]
{((2 * m) + 3),K} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{((2 * m) + 3)} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{{((2 * m) + 3),K},{((2 * m) + 3)}} is non empty finite V48() set
{[((2 * m) + 3),K]} is Relation-like NAT -defined NAT -valued non empty finite Element of bool [:NAT,NAT:]
bool [:NAT,NAT:] is non empty V107() cup-closed diff-closed preBoolean set
(m,K) \/ {[((2 * m) + 3),K]} is non empty finite set
(m,K) /\ {[((2 * m) + 3),K]} is Relation-like NAT -defined NAT -valued finite Element of bool [:NAT,NAT:]
m is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
K is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
(m,K) is finite Element of PFuncs (NAT,{K})
{K} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() Element of bool NAT
PFuncs (NAT,{K}) is functional non empty set
m + 1 is non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
((m + 1),K) is finite Element of PFuncs (NAT,{K})
a is set
2 * m is V35() V36() V37() V41() V42() V43() even V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
(2 * m) + 1 is non empty V35() V36() V37() V41() V42() V43() non even V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
a9 is non empty V35() V36() V37() V41() V42() V43() non even V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
[a9,K] is V15() Element of [:NAT,NAT:]
{a9,K} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{a9} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{{a9,K},{a9}} is non empty finite V48() set
2 * (m + 1) is V35() V36() V37() V41() V42() V43() even V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
(2 * (m + 1)) + 1 is non empty V35() V36() V37() V41() V42() V43() non even V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
m is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
K is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
(m,K) is finite Element of PFuncs (NAT,{K})
{K} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() Element of bool NAT
PFuncs (NAT,{K}) is functional non empty set
2 * m is V35() V36() V37() V41() V42() V43() even V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
[(2 * m),K] is V15() Element of [:NAT,NAT:]
{(2 * m),K} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{(2 * m)} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{{(2 * m),K},{(2 * m)}} is non empty finite V48() set
m is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
K is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
(m,K) is non empty finite Element of PFuncs (NAT,{K})
{K} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() Element of bool NAT
PFuncs (NAT,{K}) is functional non empty set
a is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
(a,K) is finite Element of PFuncs (NAT,{K})
2 * m is V35() V36() V37() V41() V42() V43() even V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
[(2 * m),K] is V15() Element of [:NAT,NAT:]
{(2 * m),K} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{(2 * m)} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{{(2 * m),K},{(2 * m)}} is non empty finite V48() set
2 * a is V35() V36() V37() V41() V42() V43() even V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
(2 * a) + 1 is non empty V35() V36() V37() V41() V42() V43() non even V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
Mi is non empty V35() V36() V37() V41() V42() V43() non even V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
[Mi,K] is V15() Element of [:NAT,NAT:]
{Mi,K} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{Mi} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{{Mi,K},{Mi}} is non empty finite V48() set
m is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
K is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
(m,K) is finite Element of PFuncs (NAT,{K})
{K} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() Element of bool NAT
PFuncs (NAT,{K}) is functional non empty set
m + 1 is non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
((m + 1),K) is finite Element of PFuncs (NAT,{K})
m is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
a is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
K is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
(m,K) is finite Element of PFuncs (NAT,{K})
{K} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() Element of bool NAT
PFuncs (NAT,{K}) is functional non empty set
(a,K) is finite Element of PFuncs (NAT,{K})
2 * m is V35() V36() V37() V41() V42() V43() even V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
2 * a is V35() V36() V37() V41() V42() V43() even V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
(2 * m) + 1 is non empty V35() V36() V37() V41() V42() V43() non even V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
(2 * a) + 1 is non empty V35() V36() V37() V41() V42() V43() non even V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
a9 is set
Mi is non empty V35() V36() V37() V41() V42() V43() non even V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
[Mi,K] is V15() Element of [:NAT,NAT:]
{Mi,K} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{Mi} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{{Mi,K},{Mi}} is non empty finite V48() set
a is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
m is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
K is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
(m,K) is finite Element of PFuncs (NAT,{K})
{K} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() Element of bool NAT
PFuncs (NAT,{K}) is functional non empty set
(a,K) is non empty finite Element of PFuncs (NAT,{K})
2 * a is V35() V36() V37() V41() V42() V43() even V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
2 * m is V35() V36() V37() V41() V42() V43() even V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
(2 * m) + 1 is non empty V35() V36() V37() V41() V42() V43() non even V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
a9 is set
Mi is non empty V35() V36() V37() V41() V42() V43() non even V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
[Mi,K] is V15() Element of [:NAT,NAT:]
{Mi,K} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{Mi} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{{Mi,K},{Mi}} is non empty finite V48() set
m is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
(1,m) is non empty finite Element of PFuncs (NAT,{m})
{m} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() Element of bool NAT
PFuncs (NAT,{m}) is functional non empty set
[1,m] is V15() Element of [:NAT,NAT:]
{1,m} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{1} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{{1,m},{1}} is non empty finite V48() set
[2,m] is V15() Element of [:NAT,NAT:]
{2,m} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{2} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{{2,m},{2}} is non empty finite V48() set
{[1,m],[2,m]} is Relation-like NAT -defined NAT -valued non empty finite Element of bool [:NAT,NAT:]
bool [:NAT,NAT:] is non empty V107() cup-closed diff-closed preBoolean set
K is set
2 * 1 is V35() V36() V37() V41() V42() V43() even V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
a is non empty V35() V36() V37() V41() V42() V43() non even V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
[a,m] is V15() Element of [:NAT,NAT:]
{a,m} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{a} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{{a,m},{a}} is non empty finite V48() set
2 * 1 is V35() V36() V37() V41() V42() V43() even V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
[(2 * 1),m] is V15() Element of [:NAT,NAT:]
{(2 * 1),m} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{(2 * 1)} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{{(2 * 1),m},{(2 * 1)}} is non empty finite V48() set
2 * 1 is V35() V36() V37() V41() V42() V43() even V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
[(2 * 1),m] is V15() Element of [:NAT,NAT:]
{(2 * 1),m} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{(2 * 1)} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{{(2 * 1),m},{(2 * 1)}} is non empty finite V48() set
K is set
2 * 1 is V35() V36() V37() V41() V42() V43() even V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
2 * 1 is V35() V36() V37() V41() V42() V43() even V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
[(2 * 1),m] is V15() Element of [:NAT,NAT:]
{(2 * 1),m} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{(2 * 1)} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{{(2 * 1),m},{(2 * 1)}} is non empty finite V48() set
K is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
{K} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() Element of bool NAT
PFuncs (NAT,{K}) is functional non empty set
Fin (PFuncs (NAT,{K})) is non empty cup-closed diff-closed preBoolean set
m is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
(m,K) is finite Element of PFuncs (NAT,{K})
a is set
2 * m is V35() V36() V37() V41() V42() V43() even V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
(2 * m) + 1 is non empty V35() V36() V37() V41() V42() V43() non even V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
Seg ((2 * m) + 1) is non empty finite V51((2 * m) + 1) V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() Element of bool NAT
[:(Seg ((2 * m) + 1)),{K}:] is Relation-like NAT -defined NAT -valued Function-like non empty finite Element of bool [:NAT,NAT:]
bool [:NAT,NAT:] is non empty V107() cup-closed diff-closed preBoolean set
bool [:(Seg ((2 * m) + 1)),{K}:] is non empty finite V48() V107() cup-closed diff-closed preBoolean set
a9 is set
Mi is non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
(Mi,K) is non empty finite Element of PFuncs (NAT,{K})
Mi is non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
(Mi,K) is non empty finite Element of PFuncs (NAT,{K})
2 * Mi is V35() V36() V37() V41() V42() V43() even V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
Mi is set
mX is non empty V35() V36() V37() V41() V42() V43() non even V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
[mX,K] is V15() Element of [:NAT,NAT:]
{mX,K} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{mX} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{{mX,K},{mX}} is non empty finite V48() set
mX is non empty V35() V36() V37() V41() V42() V43() non even V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
[mX,K] is V15() Element of [:NAT,NAT:]
{mX,K} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{mX} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{{mX,K},{mX}} is non empty finite V48() set
[(2 * Mi),K] is V15() Element of [:NAT,NAT:]
{(2 * Mi),K} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{(2 * Mi)} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{{(2 * Mi),K},{(2 * Mi)}} is non empty finite V48() set
[(2 * Mi),K] is V15() Element of [:NAT,NAT:]
{(2 * Mi),K} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{(2 * Mi)} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{{(2 * Mi),K},{(2 * Mi)}} is non empty finite V48() set
Mi is set
Mi is non empty V35() V36() V37() V41() V42() V43() non even V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
[Mi,K] is V15() Element of [:NAT,NAT:]
{Mi,K} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{Mi} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{{Mi,K},{Mi}} is non empty finite V48() set
a9 is set
a9 is finite Element of Fin (PFuncs (NAT,{K}))
Mi is set
Mi is non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
(Mi,K) is non empty finite Element of PFuncs (NAT,{K})
a is finite Element of Fin (PFuncs (NAT,{K}))
a9 is finite Element of Fin (PFuncs (NAT,{K}))
m is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
m + 1 is non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
K is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
((m + 1),K) is finite Element of Fin (PFuncs (NAT,{K}))
{K} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() Element of bool NAT
PFuncs (NAT,{K}) is functional non empty set
Fin (PFuncs (NAT,{K})) is non empty cup-closed diff-closed preBoolean set
(m,K) is finite Element of Fin (PFuncs (NAT,{K}))
a is set
a9 is non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
(a9,K) is non empty finite Element of PFuncs (NAT,{K})
a9 is non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
(a9,K) is non empty finite Element of PFuncs (NAT,{K})
Mi is set
(m,K) is finite Element of PFuncs (NAT,{K})
((m + 1),K) is finite Element of PFuncs (NAT,{K})
(m,K) is finite Element of PFuncs (NAT,{K})
a9 is finite Element of PFuncs (NAT,{K})
((m + 1),K) is finite Element of PFuncs (NAT,{K})
m is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
K is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
(m,K) is finite Element of PFuncs (NAT,{K})
{K} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() Element of bool NAT
PFuncs (NAT,{K}) is functional non empty set
m + 1 is non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
((m + 1),K) is finite Element of Fin (PFuncs (NAT,{K}))
Fin (PFuncs (NAT,{K})) is non empty cup-closed diff-closed preBoolean set
((m + 1),K) is finite Element of PFuncs (NAT,{K})
a is non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
(a,K) is non empty finite Element of PFuncs (NAT,{K})
m is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
K is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
(m,K) is finite Element of Fin (PFuncs (NAT,{K}))
{K} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() Element of bool NAT
PFuncs (NAT,{K}) is functional non empty set
Fin (PFuncs (NAT,{K})) is non empty cup-closed diff-closed preBoolean set
a is set
(m,K) is finite Element of PFuncs (NAT,{K})
a9 is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
(a9,K) is non empty finite Element of PFuncs (NAT,{K})
a9 is non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
(a9,K) is non empty finite Element of PFuncs (NAT,{K})
m is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
K is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
(m,K) is non empty finite Element of PFuncs (NAT,{K})
{K} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() Element of bool NAT
PFuncs (NAT,{K}) is functional non empty set
a is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
(a,K) is non empty finite Element of PFuncs (NAT,{K})
2 * m is V35() V36() V37() V41() V42() V43() even V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
2 * a is V35() V36() V37() V41() V42() V43() even V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
[(2 * m),K] is V15() Element of [:NAT,NAT:]
{(2 * m),K} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{(2 * m)} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{{(2 * m),K},{(2 * m)}} is non empty finite V48() set
[(2 * a),K] is V15() Element of [:NAT,NAT:]
{(2 * a),K} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{(2 * a)} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{{(2 * a),K},{(2 * a)}} is non empty finite V48() set
a9 is non empty V35() V36() V37() V41() V42() V43() non even V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
[a9,K] is V15() Element of [:NAT,NAT:]
{a9,K} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{a9} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{{a9,K},{a9}} is non empty finite V48() set
m is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
K is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
(m,K) is finite Element of PFuncs (NAT,{K})
{K} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() Element of bool NAT
PFuncs (NAT,{K}) is functional non empty set
a is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
(a,K) is non empty finite Element of PFuncs (NAT,{K})
2 * m is V35() V36() V37() V41() V42() V43() even V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
(2 * m) + 1 is non empty V35() V36() V37() V41() V42() V43() non even V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
[((2 * m) + 1),K] is V15() Element of [:NAT,NAT:]
{((2 * m) + 1),K} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{((2 * m) + 1)} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{{((2 * m) + 1),K},{((2 * m) + 1)}} is non empty finite V48() set
2 * a is V35() V36() V37() V41() V42() V43() even V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
a9 is non empty V35() V36() V37() V41() V42() V43() non even V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
[a9,K] is V15() Element of [:NAT,NAT:]
{a9,K} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{a9} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{{a9,K},{a9}} is non empty finite V48() set
2 * a is V35() V36() V37() V41() V42() V43() even V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
[(2 * a),K] is V15() Element of [:NAT,NAT:]
{(2 * a),K} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{(2 * a)} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{{(2 * a),K},{(2 * a)}} is non empty finite V48() set
2 * a is V35() V36() V37() V41() V42() V43() even V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
[(2 * a),K] is V15() Element of [:NAT,NAT:]
{(2 * a),K} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{(2 * a)} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{{(2 * a),K},{(2 * a)}} is non empty finite V48() set
m is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
K is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
(m,K) is finite Element of Fin (PFuncs (NAT,{K}))
{K} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() Element of bool NAT
PFuncs (NAT,{K}) is functional non empty set
Fin (PFuncs (NAT,{K})) is non empty cup-closed diff-closed preBoolean set
(NAT,{K}) is non empty reflexive transitive antisymmetric with_suprema with_infima RelStr
SubstLatt (NAT,{K}) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V99() LattStr
LattPOSet (SubstLatt (NAT,{K})) is non empty strict reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V118() RelStr
the carrier of (SubstLatt (NAT,{K})) is non empty set
K262((SubstLatt (NAT,{K}))) is Relation-like the carrier of (SubstLatt (NAT,{K})) -defined the carrier of (SubstLatt (NAT,{K})) -valued total V26() V29() V33() Element of bool [: the carrier of (SubstLatt (NAT,{K})), the carrier of (SubstLatt (NAT,{K})):]
[: the carrier of (SubstLatt (NAT,{K})), the carrier of (SubstLatt (NAT,{K})):] is Relation-like non empty set
bool [: the carrier of (SubstLatt (NAT,{K})), the carrier of (SubstLatt (NAT,{K})):] is non empty V107() cup-closed diff-closed preBoolean set
RelStr(# the carrier of (SubstLatt (NAT,{K})),K262((SubstLatt (NAT,{K}))) #) is strict RelStr
the carrier of (NAT,{K}) is non empty set
a is Element of PFuncs (NAT,{K})
a9 is Element of PFuncs (NAT,{K})
(m,K) is finite Element of PFuncs (NAT,{K})
Mi is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
(Mi,K) is non empty finite Element of PFuncs (NAT,{K})
Mi is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
(Mi,K) is non empty finite Element of PFuncs (NAT,{K})
Mi is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
(Mi,K) is non empty finite Element of PFuncs (NAT,{K})
Mi is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
(Mi,K) is non empty finite Element of PFuncs (NAT,{K})
Mi is non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
(Mi,K) is non empty finite Element of PFuncs (NAT,{K})
Mi is non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
(Mi,K) is non empty finite Element of PFuncs (NAT,{K})
a is set
SubstitutionSet (NAT,{K}) is non empty Element of bool (Fin (PFuncs (NAT,{K})))
bool (Fin (PFuncs (NAT,{K}))) is non empty V107() cup-closed diff-closed preBoolean set
{ b₁ where b₁ is finite Element of Fin (PFuncs (NAT,{K})) : ( ( for b₂ being set holds
( not b₂ in b₁ or b₂ is finite ) ) & ( for b₂, b₃ being Element of PFuncs (NAT,{K}) holds
( not b₂ in b₁ or not b₃ in b₁ or not b₂ c= b₃ or b₂ = b₃ ) ) ) } is set
m is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
{m} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() Element of bool NAT
(NAT,{m}) is non empty reflexive transitive antisymmetric with_suprema with_infima RelStr
SubstLatt (NAT,{m}) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V99() LattStr
LattPOSet (SubstLatt (NAT,{m})) is non empty strict reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V118() RelStr
the carrier of (SubstLatt (NAT,{m})) is non empty set
K262((SubstLatt (NAT,{m}))) is Relation-like the carrier of (SubstLatt (NAT,{m})) -defined the carrier of (SubstLatt (NAT,{m})) -valued total V26() V29() V33() Element of bool [: the carrier of (SubstLatt (NAT,{m})), the carrier of (SubstLatt (NAT,{m})):]
[: the carrier of (SubstLatt (NAT,{m})), the carrier of (SubstLatt (NAT,{m})):] is Relation-like non empty set
bool [: the carrier of (SubstLatt (NAT,{m})), the carrier of (SubstLatt (NAT,{m})):] is non empty V107() cup-closed diff-closed preBoolean set
RelStr(# the carrier of (SubstLatt (NAT,{m})),K262((SubstLatt (NAT,{m}))) #) is strict RelStr
the carrier of (NAT,{m}) is non empty set
bool the carrier of (NAT,{m}) is non empty V107() cup-closed diff-closed preBoolean set
K is set
a is set
a is Element of bool the carrier of (NAT,{m})
a9 is set
Mi is non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
(Mi,m) is finite Element of Fin (PFuncs (NAT,{m}))
PFuncs (NAT,{m}) is functional non empty set
Fin (PFuncs (NAT,{m})) is non empty cup-closed diff-closed preBoolean set
K is Element of bool the carrier of (NAT,{m})
a is Element of bool the carrier of (NAT,{m})
m is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
(1,m) is finite Element of Fin (PFuncs (NAT,{m}))
{m} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() Element of bool NAT
PFuncs (NAT,{m}) is functional non empty set
Fin (PFuncs (NAT,{m})) is non empty cup-closed diff-closed preBoolean set
(1,m) is non empty finite Element of PFuncs (NAT,{m})
(1,m) is finite Element of PFuncs (NAT,{m})
{(1,m),(1,m)} is non empty finite V48() Element of bool (PFuncs (NAT,{m}))
bool (PFuncs (NAT,{m})) is non empty V107() cup-closed diff-closed preBoolean set
K is set
a is non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
(a,m) is non empty finite Element of PFuncs (NAT,{m})
a is non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
(a,m) is non empty finite Element of PFuncs (NAT,{m})
K is set
m is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
(1,m) is finite Element of Fin (PFuncs (NAT,{m}))
{m} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() Element of bool NAT
PFuncs (NAT,{m}) is functional non empty set
Fin (PFuncs (NAT,{m})) is non empty cup-closed diff-closed preBoolean set
(1,m) is non empty finite Element of PFuncs (NAT,{m})
m is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
(1,m) is finite Element of Fin (PFuncs (NAT,{m}))
{m} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() Element of bool NAT
PFuncs (NAT,{m}) is functional non empty set
Fin (PFuncs (NAT,{m})) is non empty cup-closed diff-closed preBoolean set
(1,m) is non empty finite Element of PFuncs (NAT,{m})
K is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
{K} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() Element of bool NAT
PFuncs (NAT,{K}) is functional non empty set
m is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
(m,K) is non empty finite Element of PFuncs (NAT,{K})
{(m,K)} is non empty finite V48() Element of bool (PFuncs (NAT,{K}))
bool (PFuncs (NAT,{K})) is non empty V107() cup-closed diff-closed preBoolean set
(NAT,{K}) is non empty reflexive transitive antisymmetric with_suprema with_infima RelStr
SubstLatt (NAT,{K}) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V99() LattStr
LattPOSet (SubstLatt (NAT,{K})) is non empty strict reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V118() RelStr
the carrier of (SubstLatt (NAT,{K})) is non empty set
K262((SubstLatt (NAT,{K}))) is Relation-like the carrier of (SubstLatt (NAT,{K})) -defined the carrier of (SubstLatt (NAT,{K})) -valued total V26() V29() V33() Element of bool [: the carrier of (SubstLatt (NAT,{K})), the carrier of (SubstLatt (NAT,{K})):]
[: the carrier of (SubstLatt (NAT,{K})), the carrier of (SubstLatt (NAT,{K})):] is Relation-like non empty set
bool [: the carrier of (SubstLatt (NAT,{K})), the carrier of (SubstLatt (NAT,{K})):] is non empty V107() cup-closed diff-closed preBoolean set
RelStr(# the carrier of (SubstLatt (NAT,{K})),K262((SubstLatt (NAT,{K}))) #) is strict RelStr
the carrier of (NAT,{K}) is non empty set
SubstitutionSet (NAT,{K}) is non empty Element of bool (Fin (PFuncs (NAT,{K})))
Fin (PFuncs (NAT,{K})) is non empty cup-closed diff-closed preBoolean set
bool (Fin (PFuncs (NAT,{K}))) is non empty V107() cup-closed diff-closed preBoolean set
m is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
{m} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() Element of bool NAT
K is set
(K,{m}) is non empty reflexive transitive antisymmetric with_suprema with_infima RelStr
SubstLatt (K,{m}) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V99() LattStr
LattPOSet (SubstLatt (K,{m})) is non empty strict reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V118() RelStr
the carrier of (SubstLatt (K,{m})) is non empty set
K262((SubstLatt (K,{m}))) is Relation-like the carrier of (SubstLatt (K,{m})) -defined the carrier of (SubstLatt (K,{m})) -valued total V26() V29() V33() Element of bool [: the carrier of (SubstLatt (K,{m})), the carrier of (SubstLatt (K,{m})):]
[: the carrier of (SubstLatt (K,{m})), the carrier of (SubstLatt (K,{m})):] is Relation-like non empty set
bool [: the carrier of (SubstLatt (K,{m})), the carrier of (SubstLatt (K,{m})):] is non empty V107() cup-closed diff-closed preBoolean set
RelStr(# the carrier of (SubstLatt (K,{m})),K262((SubstLatt (K,{m}))) #) is strict RelStr
the carrier of (K,{m}) is non empty set
a is set
[:K,{m}:] is Relation-like Function-like set
bool [:K,{m}:] is non empty cup-closed diff-closed preBoolean set
a9 is Element of the carrier of (K,{m})
PFuncs (K,{m}) is functional non empty set
SubstitutionSet (K,{m}) is non empty Element of bool (Fin (PFuncs (K,{m})))
Fin (PFuncs (K,{m})) is non empty cup-closed diff-closed preBoolean set
bool (Fin (PFuncs (K,{m}))) is non empty V107() cup-closed diff-closed preBoolean set
m is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
{m} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() Element of bool NAT
(NAT,{m}) is non empty reflexive transitive antisymmetric with_suprema with_infima RelStr
SubstLatt (NAT,{m}) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V99() LattStr
LattPOSet (SubstLatt (NAT,{m})) is non empty strict reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V118() RelStr
the carrier of (SubstLatt (NAT,{m})) is non empty set
K262((SubstLatt (NAT,{m}))) is Relation-like the carrier of (SubstLatt (NAT,{m})) -defined the carrier of (SubstLatt (NAT,{m})) -valued total V26() V29() V33() Element of bool [: the carrier of (SubstLatt (NAT,{m})), the carrier of (SubstLatt (NAT,{m})):]
[: the carrier of (SubstLatt (NAT,{m})), the carrier of (SubstLatt (NAT,{m})):] is Relation-like non empty set
bool [: the carrier of (SubstLatt (NAT,{m})), the carrier of (SubstLatt (NAT,{m})):] is non empty V107() cup-closed diff-closed preBoolean set
RelStr(# the carrier of (SubstLatt (NAT,{m})),K262((SubstLatt (NAT,{m}))) #) is strict RelStr
the carrier of (NAT,{m}) is non empty set
(m) is Element of bool the carrier of (NAT,{m})
bool the carrier of (NAT,{m}) is non empty V107() cup-closed diff-closed preBoolean set
K is Element of the carrier of (NAT,{m})
a is non empty set
[:NAT,{m}:] is Relation-like REAL -defined NAT -valued Function-like non empty Element of bool [:REAL,NAT:]
[:REAL,NAT:] is Relation-like set
bool [:REAL,NAT:] is non empty cup-closed diff-closed preBoolean set
bool [:NAT,{m}:] is non empty V107() cup-closed diff-closed preBoolean set
Mi is non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
(Mi,m) is finite Element of Fin (PFuncs (NAT,{m}))
PFuncs (NAT,{m}) is functional non empty set
Fin (PFuncs (NAT,{m})) is non empty cup-closed diff-closed preBoolean set
2 * Mi is V35() V36() V37() V41() V42() V43() even V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
(2 * Mi) + 1 is non empty V35() V36() V37() V41() V42() V43() non even V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
[((2 * Mi) + 1),m] is V15() Element of [:NAT,NAT:]
{((2 * Mi) + 1),m} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{((2 * Mi) + 1)} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{{((2 * Mi) + 1),m},{((2 * Mi) + 1)}} is non empty finite V48() set
(Mi,m) is finite Element of PFuncs (NAT,{m})
Mi is Element of the carrier of (NAT,{m})
mX is set
Sum is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
(Sum,m) is non empty finite Element of PFuncs (NAT,{m})
2 * Sum is V35() V36() V37() V41() V42() V43() even V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
[(2 * Sum),m] is V15() Element of [:NAT,NAT:]
{(2 * Sum),m} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{(2 * Sum)} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{{(2 * Sum),m},{(2 * Sum)}} is non empty finite V48() set
Sum is non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
(Sum,m) is non empty finite Element of PFuncs (NAT,{m})
a9 is Relation-like REAL -defined NAT -valued non empty finite Element of bool [:NAT,{m}:]
Mi is non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
2 * Mi is V35() V36() V37() V41() V42() V43() even V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
(2 * Mi) + 1 is non empty V35() V36() V37() V41() V42() V43() non even V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
[((2 * Mi) + 1),m] is V15() Element of [:NAT,NAT:]
{((2 * Mi) + 1),m} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{((2 * Mi) + 1)} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{{((2 * Mi) + 1),m},{((2 * Mi) + 1)}} is non empty finite V48() set
m is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
{m} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() Element of bool NAT
(NAT,{m}) is non empty reflexive transitive antisymmetric with_suprema with_infima RelStr
SubstLatt (NAT,{m}) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V99() LattStr
LattPOSet (SubstLatt (NAT,{m})) is non empty strict reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V118() RelStr
the carrier of (SubstLatt (NAT,{m})) is non empty set
K262((SubstLatt (NAT,{m}))) is Relation-like the carrier of (SubstLatt (NAT,{m})) -defined the carrier of (SubstLatt (NAT,{m})) -valued total V26() V29() V33() Element of bool [: the carrier of (SubstLatt (NAT,{m})), the carrier of (SubstLatt (NAT,{m})):]
[: the carrier of (SubstLatt (NAT,{m})), the carrier of (SubstLatt (NAT,{m})):] is Relation-like non empty set
bool [: the carrier of (SubstLatt (NAT,{m})), the carrier of (SubstLatt (NAT,{m})):] is non empty V107() cup-closed diff-closed preBoolean set
RelStr(# the carrier of (SubstLatt (NAT,{m})),K262((SubstLatt (NAT,{m}))) #) is strict RelStr
the carrier of (NAT,{m}) is non empty set
bool the carrier of (NAT,{m}) is non empty V107() cup-closed diff-closed preBoolean set
K is Element of the carrier of (NAT,{m})
a is Element of the carrier of (NAT,{m})
K "\/" a is Element of the carrier of (NAT,{m})
a9 is Element of bool the carrier of (NAT,{m})
Mi is Element of the carrier of (NAT,{m})
m is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
{m} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() Element of bool NAT
(NAT,{m}) is non empty reflexive transitive antisymmetric with_suprema with_infima RelStr
SubstLatt (NAT,{m}) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V99() LattStr
LattPOSet (SubstLatt (NAT,{m})) is non empty strict reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V118() RelStr
the carrier of (SubstLatt (NAT,{m})) is non empty set
K262((SubstLatt (NAT,{m}))) is Relation-like the carrier of (SubstLatt (NAT,{m})) -defined the carrier of (SubstLatt (NAT,{m})) -valued total V26() V29() V33() Element of bool [: the carrier of (SubstLatt (NAT,{m})), the carrier of (SubstLatt (NAT,{m})):]
[: the carrier of (SubstLatt (NAT,{m})), the carrier of (SubstLatt (NAT,{m})):] is Relation-like non empty set
bool [: the carrier of (SubstLatt (NAT,{m})), the carrier of (SubstLatt (NAT,{m})):] is non empty V107() cup-closed diff-closed preBoolean set
RelStr(# the carrier of (SubstLatt (NAT,{m})),K262((SubstLatt (NAT,{m}))) #) is strict RelStr
the carrier of (NAT,{m}) is non empty set
SubstitutionSet (NAT,{m}) is non empty Element of bool (Fin (PFuncs (NAT,{m})))
PFuncs (NAT,{m}) is functional non empty set
Fin (PFuncs (NAT,{m})) is non empty cup-closed diff-closed preBoolean set
bool (Fin (PFuncs (NAT,{m}))) is non empty V107() cup-closed diff-closed preBoolean set
K is Element of the carrier of (NAT,{m})
m is non empty set
K is set
K is set
m is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
{m} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() Element of bool NAT
(NAT,{m}) is non empty reflexive transitive antisymmetric with_suprema with_infima RelStr
SubstLatt (NAT,{m}) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V99() LattStr
LattPOSet (SubstLatt (NAT,{m})) is non empty strict reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V118() RelStr
the carrier of (SubstLatt (NAT,{m})) is non empty set
K262((SubstLatt (NAT,{m}))) is Relation-like the carrier of (SubstLatt (NAT,{m})) -defined the carrier of (SubstLatt (NAT,{m})) -valued total V26() V29() V33() Element of bool [: the carrier of (SubstLatt (NAT,{m})), the carrier of (SubstLatt (NAT,{m})):]
[: the carrier of (SubstLatt (NAT,{m})), the carrier of (SubstLatt (NAT,{m})):] is Relation-like non empty set
bool [: the carrier of (SubstLatt (NAT,{m})), the carrier of (SubstLatt (NAT,{m})):] is non empty V107() cup-closed diff-closed preBoolean set
RelStr(# the carrier of (SubstLatt (NAT,{m})),K262((SubstLatt (NAT,{m}))) #) is strict RelStr
the carrier of (NAT,{m}) is non empty set
K is Element of the carrier of (NAT,{m})
SubstitutionSet (NAT,{m}) is non empty Element of bool (Fin (PFuncs (NAT,{m})))
PFuncs (NAT,{m}) is functional non empty set
Fin (PFuncs (NAT,{m})) is non empty cup-closed diff-closed preBoolean set
bool (Fin (PFuncs (NAT,{m}))) is non empty V107() cup-closed diff-closed preBoolean set
a is set
m is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
{m} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() Element of bool NAT
(NAT,{m}) is non empty reflexive transitive antisymmetric with_suprema with_infima RelStr
SubstLatt (NAT,{m}) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V99() LattStr
LattPOSet (SubstLatt (NAT,{m})) is non empty strict reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V118() RelStr
the carrier of (SubstLatt (NAT,{m})) is non empty set
K262((SubstLatt (NAT,{m}))) is Relation-like the carrier of (SubstLatt (NAT,{m})) -defined the carrier of (SubstLatt (NAT,{m})) -valued total V26() V29() V33() Element of bool [: the carrier of (SubstLatt (NAT,{m})), the carrier of (SubstLatt (NAT,{m})):]
[: the carrier of (SubstLatt (NAT,{m})), the carrier of (SubstLatt (NAT,{m})):] is Relation-like non empty set
bool [: the carrier of (SubstLatt (NAT,{m})), the carrier of (SubstLatt (NAT,{m})):] is non empty V107() cup-closed diff-closed preBoolean set
RelStr(# the carrier of (SubstLatt (NAT,{m})),K262((SubstLatt (NAT,{m}))) #) is strict RelStr
the carrier of (NAT,{m}) is non empty set
K is non empty Element of the carrier of (NAT,{m})
a is set
SubstitutionSet (NAT,{m}) is non empty Element of bool (Fin (PFuncs (NAT,{m})))
PFuncs (NAT,{m}) is functional non empty set
Fin (PFuncs (NAT,{m})) is non empty cup-closed diff-closed preBoolean set
bool (Fin (PFuncs (NAT,{m}))) is non empty V107() cup-closed diff-closed preBoolean set
a9 is Relation-like Function-like finite set
m is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
{m} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() Element of bool NAT
(NAT,{m}) is non empty reflexive transitive antisymmetric with_suprema with_infima RelStr
SubstLatt (NAT,{m}) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V99() LattStr
LattPOSet (SubstLatt (NAT,{m})) is non empty strict reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V118() RelStr
the carrier of (SubstLatt (NAT,{m})) is non empty set
K262((SubstLatt (NAT,{m}))) is Relation-like the carrier of (SubstLatt (NAT,{m})) -defined the carrier of (SubstLatt (NAT,{m})) -valued total V26() V29() V33() Element of bool [: the carrier of (SubstLatt (NAT,{m})), the carrier of (SubstLatt (NAT,{m})):]
[: the carrier of (SubstLatt (NAT,{m})), the carrier of (SubstLatt (NAT,{m})):] is Relation-like non empty set
bool [: the carrier of (SubstLatt (NAT,{m})), the carrier of (SubstLatt (NAT,{m})):] is non empty V107() cup-closed diff-closed preBoolean set
RelStr(# the carrier of (SubstLatt (NAT,{m})),K262((SubstLatt (NAT,{m}))) #) is strict RelStr
the carrier of (NAT,{m}) is non empty set
PFuncs (NAT,{m}) is functional non empty set
Fin (PFuncs (NAT,{m})) is non empty cup-closed diff-closed preBoolean set
K is non empty Element of the carrier of (NAT,{m})
a is finite Element of Fin (PFuncs (NAT,{m}))
Involved a is finite set
a9 is Relation-like Function-like finite set
dom a9 is finite set
Mi is set
m is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
{m} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() Element of bool NAT
(NAT,{m}) is non empty reflexive transitive antisymmetric with_suprema with_infima RelStr
SubstLatt (NAT,{m}) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V99() LattStr
LattPOSet (SubstLatt (NAT,{m})) is non empty strict reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V118() RelStr
the carrier of (SubstLatt (NAT,{m})) is non empty set
K262((SubstLatt (NAT,{m}))) is Relation-like the carrier of (SubstLatt (NAT,{m})) -defined the carrier of (SubstLatt (NAT,{m})) -valued total V26() V29() V33() Element of bool [: the carrier of (SubstLatt (NAT,{m})), the carrier of (SubstLatt (NAT,{m})):]
[: the carrier of (SubstLatt (NAT,{m})), the carrier of (SubstLatt (NAT,{m})):] is Relation-like non empty set
bool [: the carrier of (SubstLatt (NAT,{m})), the carrier of (SubstLatt (NAT,{m})):] is non empty V107() cup-closed diff-closed preBoolean set
RelStr(# the carrier of (SubstLatt (NAT,{m})),K262((SubstLatt (NAT,{m}))) #) is strict RelStr
the carrier of (NAT,{m}) is non empty set
PFuncs (NAT,{m}) is functional non empty set
Fin (PFuncs (NAT,{m})) is non empty cup-closed diff-closed preBoolean set
K is Element of the carrier of (NAT,{m})
a is finite Element of Fin (PFuncs (NAT,{m}))
Involved a is finite set
a9 is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() Element of bool NAT
max a9 is V35() V36() V37() V41() V42() V43() V128() ext-real non negative set
(max a9) + 1 is non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
Mi is set
SubstitutionSet (NAT,{m}) is non empty Element of bool (Fin (PFuncs (NAT,{m})))
bool (Fin (PFuncs (NAT,{m}))) is non empty V107() cup-closed diff-closed preBoolean set
mX is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
[mX,m] is V15() Element of [:NAT,NAT:]
{mX,m} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{mX} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{{mX,m},{mX}} is non empty finite V48() set
Mi is Relation-like Function-like finite set
dom Mi is finite set
m is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
{m} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() Element of bool NAT
(NAT,{m}) is non empty reflexive transitive antisymmetric with_suprema with_infima RelStr
SubstLatt (NAT,{m}) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V99() LattStr
LattPOSet (SubstLatt (NAT,{m})) is non empty strict reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V118() RelStr
the carrier of (SubstLatt (NAT,{m})) is non empty set
K262((SubstLatt (NAT,{m}))) is Relation-like the carrier of (SubstLatt (NAT,{m})) -defined the carrier of (SubstLatt (NAT,{m})) -valued total V26() V29() V33() Element of bool [: the carrier of (SubstLatt (NAT,{m})), the carrier of (SubstLatt (NAT,{m})):]
[: the carrier of (SubstLatt (NAT,{m})), the carrier of (SubstLatt (NAT,{m})):] is Relation-like non empty set
bool [: the carrier of (SubstLatt (NAT,{m})), the carrier of (SubstLatt (NAT,{m})):] is non empty V107() cup-closed diff-closed preBoolean set
RelStr(# the carrier of (SubstLatt (NAT,{m})),K262((SubstLatt (NAT,{m}))) #) is strict RelStr
Top (NAT,{m}) is Element of the carrier of (NAT,{m})
the carrier of (NAT,{m}) is non empty set
SubstitutionSet (NAT,{m}) is non empty Element of bool (Fin (PFuncs (NAT,{m})))
PFuncs (NAT,{m}) is functional non empty set
Fin (PFuncs (NAT,{m})) is non empty cup-closed diff-closed preBoolean set
bool (Fin (PFuncs (NAT,{m}))) is non empty V107() cup-closed diff-closed preBoolean set
K is Element of the carrier of (NAT,{m})
a is Element of the carrier of (NAT,{m})
a9 is set
Mi is Relation-like non-empty empty-yielding functional empty V35() V36() V37() V39() V40() V41() finite finite-yielding V48() FinSequence-like FinSequence-membered ext-real non positive non negative V143() V144() V145() V146() V147() V148() V149() V156() V157() V158() V159() set
"/\" ({},(NAT,{m})) is Element of the carrier of (NAT,{m})
m is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
{m} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() Element of bool NAT
(NAT,{m}) is non empty reflexive transitive antisymmetric with_suprema with_infima RelStr
SubstLatt (NAT,{m}) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V99() LattStr
LattPOSet (SubstLatt (NAT,{m})) is non empty strict reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V118() RelStr
the carrier of (SubstLatt (NAT,{m})) is non empty set
K262((SubstLatt (NAT,{m}))) is Relation-like the carrier of (SubstLatt (NAT,{m})) -defined the carrier of (SubstLatt (NAT,{m})) -valued total V26() V29() V33() Element of bool [: the carrier of (SubstLatt (NAT,{m})), the carrier of (SubstLatt (NAT,{m})):]
[: the carrier of (SubstLatt (NAT,{m})), the carrier of (SubstLatt (NAT,{m})):] is Relation-like non empty set
bool [: the carrier of (SubstLatt (NAT,{m})), the carrier of (SubstLatt (NAT,{m})):] is non empty V107() cup-closed diff-closed preBoolean set
RelStr(# the carrier of (SubstLatt (NAT,{m})),K262((SubstLatt (NAT,{m}))) #) is strict RelStr
Bottom (NAT,{m}) is Element of the carrier of (NAT,{m})
the carrier of (NAT,{m}) is non empty set
SubstitutionSet (NAT,{m}) is non empty Element of bool (Fin (PFuncs (NAT,{m})))
PFuncs (NAT,{m}) is functional non empty set
Fin (PFuncs (NAT,{m})) is non empty cup-closed diff-closed preBoolean set
bool (Fin (PFuncs (NAT,{m}))) is non empty V107() cup-closed diff-closed preBoolean set
K is Element of the carrier of (NAT,{m})
a is Element of the carrier of (NAT,{m})
a9 is set
"\/" ({},(NAT,{m})) is Element of the carrier of (NAT,{m})
m is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
{m} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() Element of bool NAT
(NAT,{m}) is non empty reflexive transitive antisymmetric with_suprema with_infima RelStr
SubstLatt (NAT,{m}) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V99() LattStr
LattPOSet (SubstLatt (NAT,{m})) is non empty strict reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V118() RelStr
the carrier of (SubstLatt (NAT,{m})) is non empty set
K262((SubstLatt (NAT,{m}))) is Relation-like the carrier of (SubstLatt (NAT,{m})) -defined the carrier of (SubstLatt (NAT,{m})) -valued total V26() V29() V33() Element of bool [: the carrier of (SubstLatt (NAT,{m})), the carrier of (SubstLatt (NAT,{m})):]
[: the carrier of (SubstLatt (NAT,{m})), the carrier of (SubstLatt (NAT,{m})):] is Relation-like non empty set
bool [: the carrier of (SubstLatt (NAT,{m})), the carrier of (SubstLatt (NAT,{m})):] is non empty V107() cup-closed diff-closed preBoolean set
RelStr(# the carrier of (SubstLatt (NAT,{m})),K262((SubstLatt (NAT,{m}))) #) is strict RelStr
the carrier of (NAT,{m}) is non empty set
K is Element of the carrier of (NAT,{m})
a is Element of the carrier of (NAT,{m})
Top (NAT,{m}) is Element of the carrier of (NAT,{m})
m is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
{m} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() Element of bool NAT
(NAT,{m}) is non empty reflexive transitive antisymmetric with_suprema with_infima RelStr
SubstLatt (NAT,{m}) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V99() LattStr
LattPOSet (SubstLatt (NAT,{m})) is non empty strict reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V118() RelStr
the carrier of (SubstLatt (NAT,{m})) is non empty set
K262((SubstLatt (NAT,{m}))) is Relation-like the carrier of (SubstLatt (NAT,{m})) -defined the carrier of (SubstLatt (NAT,{m})) -valued total V26() V29() V33() Element of bool [: the carrier of (SubstLatt (NAT,{m})), the carrier of (SubstLatt (NAT,{m})):]
[: the carrier of (SubstLatt (NAT,{m})), the carrier of (SubstLatt (NAT,{m})):] is Relation-like non empty set
bool [: the carrier of (SubstLatt (NAT,{m})), the carrier of (SubstLatt (NAT,{m})):] is non empty V107() cup-closed diff-closed preBoolean set
RelStr(# the carrier of (SubstLatt (NAT,{m})),K262((SubstLatt (NAT,{m}))) #) is strict RelStr
the carrier of (NAT,{m}) is non empty set
K is Element of the carrier of (NAT,{m})
a is Element of the carrier of (NAT,{m})
Bottom (NAT,{m}) is Element of the carrier of (NAT,{m})
m is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
{m} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() Element of bool NAT
(NAT,{m}) is non empty reflexive transitive antisymmetric with_suprema with_infima RelStr
SubstLatt (NAT,{m}) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V99() LattStr
LattPOSet (SubstLatt (NAT,{m})) is non empty strict reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V118() RelStr
the carrier of (SubstLatt (NAT,{m})) is non empty set
K262((SubstLatt (NAT,{m}))) is Relation-like the carrier of (SubstLatt (NAT,{m})) -defined the carrier of (SubstLatt (NAT,{m})) -valued total V26() V29() V33() Element of bool [: the carrier of (SubstLatt (NAT,{m})), the carrier of (SubstLatt (NAT,{m})):]
[: the carrier of (SubstLatt (NAT,{m})), the carrier of (SubstLatt (NAT,{m})):] is Relation-like non empty set
bool [: the carrier of (SubstLatt (NAT,{m})), the carrier of (SubstLatt (NAT,{m})):] is non empty V107() cup-closed diff-closed preBoolean set
RelStr(# the carrier of (SubstLatt (NAT,{m})),K262((SubstLatt (NAT,{m}))) #) is strict RelStr
the carrier of (NAT,{m}) is non empty set
(m) is Element of bool the carrier of (NAT,{m})
bool the carrier of (NAT,{m}) is non empty V107() cup-closed diff-closed preBoolean set
(1,m) is non empty finite Element of Fin (PFuncs (NAT,{m}))
PFuncs (NAT,{m}) is functional non empty set
Fin (PFuncs (NAT,{m})) is non empty cup-closed diff-closed preBoolean set
a is Element of the carrier of (NAT,{m})
K is Element of the carrier of (NAT,{m})
Top (NAT,{m}) is Element of the carrier of (NAT,{m})
m is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
{m} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() Element of bool NAT
(NAT,{m}) is non empty reflexive transitive antisymmetric with_suprema with_infima RelStr
SubstLatt (NAT,{m}) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V99() LattStr
LattPOSet (SubstLatt (NAT,{m})) is non empty strict reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V118() RelStr
the carrier of (SubstLatt (NAT,{m})) is non empty set
K262((SubstLatt (NAT,{m}))) is Relation-like the carrier of (SubstLatt (NAT,{m})) -defined the carrier of (SubstLatt (NAT,{m})) -valued total V26() V29() V33() Element of bool [: the carrier of (SubstLatt (NAT,{m})), the carrier of (SubstLatt (NAT,{m})):]
[: the carrier of (SubstLatt (NAT,{m})), the carrier of (SubstLatt (NAT,{m})):] is Relation-like non empty set
bool [: the carrier of (SubstLatt (NAT,{m})), the carrier of (SubstLatt (NAT,{m})):] is non empty V107() cup-closed diff-closed preBoolean set
RelStr(# the carrier of (SubstLatt (NAT,{m})),K262((SubstLatt (NAT,{m}))) #) is strict RelStr
the carrier of (NAT,{m}) is non empty set
PFuncs (NAT,{m}) is functional non empty set
(1,m) is non empty finite Element of PFuncs (NAT,{m})
{(1,m)} is non empty finite V48() Element of bool (PFuncs (NAT,{m}))
bool (PFuncs (NAT,{m})) is non empty V107() cup-closed diff-closed preBoolean set
(m) is Element of bool the carrier of (NAT,{m})
bool the carrier of (NAT,{m}) is non empty V107() cup-closed diff-closed preBoolean set
a is Element of the carrier of (NAT,{m})
SubstitutionSet (NAT,{m}) is non empty Element of bool (Fin (PFuncs (NAT,{m})))
Fin (PFuncs (NAT,{m})) is non empty cup-closed diff-closed preBoolean set
bool (Fin (PFuncs (NAT,{m}))) is non empty V107() cup-closed diff-closed preBoolean set
a9 is finite Element of Fin (PFuncs (NAT,{m}))
Involved a9 is finite set
K is Element of the carrier of (NAT,{m})
Mi is Element of the carrier of (NAT,{m})
mX is non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
(mX,m) is finite Element of Fin (PFuncs (NAT,{m}))
Sum is set
Mi is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() Element of bool NAT
max Mi is V35() V36() V37() V41() V42() V43() V128() ext-real non negative set
(max Mi) + 1 is non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
mX is non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
(mX,m) is non empty finite Element of PFuncs (NAT,{m})
{(mX,m)} is non empty finite V48() Element of bool (PFuncs (NAT,{m}))
Sum is Element of the carrier of (NAT,{m})
a "\/" Sum is Element of the carrier of (NAT,{m})
g is Element of the carrier of (NAT,{m})
P1 is non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
(P1,m) is finite Element of Fin (PFuncs (NAT,{m}))
x is set
(P1,m) is finite Element of PFuncs (NAT,{m})
y is finite Element of PFuncs (NAT,{m})
y is non empty finite Element of PFuncs (NAT,{m})
g is set
P1 is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
[P1,m] is V15() Element of [:NAT,NAT:]
{P1,m} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{P1} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{{P1,m},{P1}} is non empty finite V48() set
2 * mX is V35() V36() V37() V41() V42() V43() even V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
x is non empty V35() V36() V37() V41() V42() V43() non even V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() Element of NAT
[x,m] is V15() Element of [:NAT,NAT:]
{x,m} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{x} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{{x,m},{x}} is non empty finite V48() set
2 * mX is V35() V36() V37() V41() V42() V43() even V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
[(2 * mX),m] is V15() Element of [:NAT,NAT:]
{(2 * mX),m} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{(2 * mX)} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{{(2 * mX),m},{(2 * mX)}} is non empty finite V48() set
2 * mX is V35() V36() V37() V41() V42() V43() even V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
[(2 * mX),m] is V15() Element of [:NAT,NAT:]
{(2 * mX),m} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{(2 * mX)} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() set
{{(2 * mX),m},{(2 * mX)}} is non empty finite V48() set
(1,m) is non empty finite Element of Fin (PFuncs (NAT,{m}))
P1 is Element of the carrier of (NAT,{m})
m is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
{m} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() Element of bool NAT
(NAT,{m}) is non empty reflexive transitive antisymmetric with_suprema with_infima RelStr
SubstLatt (NAT,{m}) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V99() LattStr
LattPOSet (SubstLatt (NAT,{m})) is non empty strict reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V118() RelStr
the carrier of (SubstLatt (NAT,{m})) is non empty set
K262((SubstLatt (NAT,{m}))) is Relation-like the carrier of (SubstLatt (NAT,{m})) -defined the carrier of (SubstLatt (NAT,{m})) -valued total V26() V29() V33() Element of bool [: the carrier of (SubstLatt (NAT,{m})), the carrier of (SubstLatt (NAT,{m})):]
[: the carrier of (SubstLatt (NAT,{m})), the carrier of (SubstLatt (NAT,{m})):] is Relation-like non empty set
bool [: the carrier of (SubstLatt (NAT,{m})), the carrier of (SubstLatt (NAT,{m})):] is non empty V107() cup-closed diff-closed preBoolean set
RelStr(# the carrier of (SubstLatt (NAT,{m})),K262((SubstLatt (NAT,{m}))) #) is strict RelStr
m is V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() Element of NAT
{m} is non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() Element of bool NAT
SubstLatt (NAT,{m}) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V99() LattStr
K is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete LattStr
LattPOSet K is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V118() RelStr
the carrier of K is non empty set
K262(K) is Relation-like the carrier of K -defined the carrier of K -valued total V26() V29() V33() Element of bool [: the carrier of K, the carrier of K:]
[: the carrier of K, the carrier of K:] is Relation-like non empty set
bool [: the carrier of K, the carrier of K:] is non empty V107() cup-closed diff-closed preBoolean set
RelStr(# the carrier of K,K262(K) #) is strict RelStr
(NAT,{m}) is non empty reflexive transitive antisymmetric with_suprema with_infima non complete RelStr
LattPOSet (SubstLatt (NAT,{m})) is non empty strict reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V118() RelStr
the carrier of (SubstLatt (NAT,{m})) is non empty set
K262((SubstLatt (NAT,{m}))) is Relation-like the carrier of (SubstLatt (NAT,{m})) -defined the carrier of (SubstLatt (NAT,{m})) -valued total V26() V29() V33() Element of bool [: the carrier of (SubstLatt (NAT,{m})), the carrier of (SubstLatt (NAT,{m})):]
[: the carrier of (SubstLatt (NAT,{m})), the carrier of (SubstLatt (NAT,{m})):] is Relation-like non empty set
bool [: the carrier of (SubstLatt (NAT,{m})), the carrier of (SubstLatt (NAT,{m})):] is non empty V107() cup-closed diff-closed preBoolean set
RelStr(# the carrier of (SubstLatt (NAT,{m})),K262((SubstLatt (NAT,{m}))) #) is strict RelStr