:: CHAIN_1 semantic presentation

REAL is non empty non trivial non finite V153() V154() V155() V159() set
NAT is non empty non trivial ordinal limit_ordinal non finite cardinal limit_cardinal V153() V154() V155() V156() V157() V158() V159() Element of bool REAL
bool REAL is non empty non trivial non finite set
omega is non empty non trivial ordinal limit_ordinal non finite cardinal limit_cardinal V153() V154() V155() V156() V157() V158() V159() set
bool omega is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set
1 is non empty ordinal natural complex real finite cardinal V43() ext-real positive non negative V64() V153() V154() V155() V156() V157() V158() Element of NAT
[:1,1:] is non empty Relation-like RAT -valued INT -valued finite V143() V144() V145() V146() set
RAT is non empty non trivial non finite V153() V154() V155() V156() V159() set
INT is non empty non trivial non finite V153() V154() V155() V156() V157() V159() set
bool [:1,1:] is non empty finite V28() set
[:[:1,1:],1:] is non empty Relation-like RAT -valued INT -valued finite V143() V144() V145() V146() set
bool [:[:1,1:],1:] is non empty finite V28() set
[:[:1,1:],REAL:] is non empty non trivial Relation-like non finite V143() V144() V145() set
bool [:[:1,1:],REAL:] is non empty non trivial non finite set
[:REAL,REAL:] is non empty non trivial Relation-like non finite V143() V144() V145() set
[:[:REAL,REAL:],REAL:] is non empty non trivial Relation-like non finite V143() V144() V145() set
bool [:[:REAL,REAL:],REAL:] is non empty non trivial non finite set
2 is non empty ordinal natural complex real finite cardinal V43() ext-real positive non negative V64() V153() V154() V155() V156() V157() V158() Element of NAT
[:2,2:] is non empty Relation-like RAT -valued INT -valued finite V143() V144() V145() V146() set
[:[:2,2:],REAL:] is non empty non trivial Relation-like non finite V143() V144() V145() set
bool [:[:2,2:],REAL:] is non empty non trivial non finite set
COMPLEX is non empty non trivial non finite V153() V159() set
bool [:REAL,REAL:] is non empty non trivial non finite set
K388(2) is non empty V81() right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V177() L15()
the carrier of K388(2) is non empty set
{} is empty trivial ordinal natural complex real Relation-like non-empty empty-yielding RAT -valued functional finite finite-yielding V28() cardinal {} -element FinSequence-like FinSequence-membered ext-real non positive non negative V143() V144() V145() V146() V153() V154() V155() V156() V157() V158() V159() set
3 is non empty ordinal natural complex real finite cardinal V43() ext-real positive non negative V64() V153() V154() V155() V156() V157() V158() Element of NAT
card {} is empty trivial ordinal natural complex real Relation-like non-empty empty-yielding RAT -valued functional finite finite-yielding V28() cardinal {} -element FinSequence-like FinSequence-membered ext-real non positive non negative V143() V144() V145() V146() V153() V154() V155() V156() V157() V158() V159() set
0 is empty trivial ordinal natural complex real Relation-like non-empty empty-yielding RAT -valued functional finite finite-yielding V28() cardinal {} -element V43() FinSequence-like FinSequence-membered ext-real non positive non negative V64() V143() V144() V145() V146() V153() V154() V155() V156() V157() V158() V159() Element of NAT
G is complex real ext-real set
d is complex real ext-real set
k is complex real ext-real set
f is complex real ext-real Element of REAL
d is complex real ext-real set
G is complex real ext-real set
k is complex real ext-real Element of REAL
f is complex real ext-real Element of REAL
max (k,f) is complex real ext-real set
(max (k,f)) + 1 is complex real ext-real Element of REAL
g is complex real ext-real Element of REAL
k + 0 is complex real ext-real Element of REAL
f + 0 is complex real ext-real Element of REAL
F₁() is non empty set
F₂() is non empty set
{ F₃(b₁,b₂) where b₁, b₂ is Element of F₂() : P₁[b₁,b₂] } is set
d is set
G is Element of F₂()
k is Element of F₂()
F₃(G,k) is Element of F₁()
d is set
bool d is non empty set
G is Element of bool d
bool G is non empty set
bool (bool d) is non empty set
d is ordinal natural complex real finite cardinal V43() ext-real non negative V64() V153() V154() V155() V156() V157() V158() Element of NAT
d is ordinal natural complex real finite cardinal V43() ext-real non negative V64() V153() V154() V155() V156() V157() V158() Element of NAT
1 + 0 is non empty ordinal natural complex real finite cardinal V43() ext-real positive non negative V64() V153() V154() V155() V156() V157() V158() Element of NAT
d is set
G is set
{d,G} is non empty finite set
{d,d} is non empty finite set
{d} is non empty trivial finite 1 -element set
{0,1} is non empty finite V28() V153() V154() V155() V156() V157() V158() Element of bool NAT
d is non empty non trivial set
G is set
d \/ G is non empty set
k is set
f is set
G \/ d is non empty non trivial set
d is non empty non trivial set
bool d is non empty set
G is set
k is set
{G,k} is non empty finite set
d is set
G is set
{G} is non empty trivial finite 1 -element set
d \/ {G} is non empty set
k is set
{k} is non empty trivial finite 1 -element set
F₁() is non empty set
bool F₁() is non empty set
F₂() is non empty finite Element of bool F₁()
d is set
G is set
{d} is non empty trivial finite 1 -element set
G \/ {d} is non empty set
k is Element of bool F₁()
k is Element of bool F₁()
k is Element of bool F₁()
k is Element of bool F₁()
F₁() is non empty non trivial set
bool F₁() is non empty set
F₂() is non empty non trivial finite Element of bool F₁()
d is set
G is set
{d} is non empty trivial finite 1 -element set
G \/ {d} is non empty set
k is Element of bool F₁()
k \/ {d} is non empty set
k is Element of bool F₁()
k is Element of bool F₁()
k is Element of bool F₁()
k \/ {d} is non empty set
f is set
{f} is non empty trivial finite 1 -element set
{d,f} is non empty finite set
k is Element of bool F₁()
k \/ {d} is non empty set
d is set
card d is ordinal cardinal set
G is finite set
k is set
f is set
{k,f} is non empty finite set
g is set
A is set
A9 is set
G is set
k is set
f is set
g is set
{G,k} is non empty finite set
d is ordinal natural complex real finite cardinal V43() ext-real non negative V64() V153() V154() V155() V156() V157() V158() Element of NAT
G is ordinal natural complex real finite cardinal V43() ext-real non negative V64() V153() V154() V155() V156() V157() V158() Element of NAT
d + G is ordinal natural complex real finite cardinal V43() ext-real non negative V64() V153() V154() V155() V156() V157() V158() Element of NAT
k is ordinal natural complex real finite cardinal V43() ext-real non negative V64() V153() V154() V155() V156() V157() V158() Element of NAT
f is ordinal natural complex real finite cardinal V43() ext-real non negative V64() V153() V154() V155() V156() V157() V158() Element of NAT
k + f is ordinal natural complex real finite cardinal V43() ext-real non negative V64() V153() V154() V155() V156() V157() V158() Element of NAT
d is finite set
G is finite set
card d is ordinal natural complex real finite cardinal V43() ext-real non negative V64() V153() V154() V155() V156() V157() V158() Element of omega
card G is ordinal natural complex real finite cardinal V43() ext-real non negative V64() V153() V154() V155() V156() V157() V158() Element of omega
d \/ G is finite set
card (d \/ G) is ordinal natural complex real finite cardinal V43() ext-real non negative V64() V153() V154() V155() V156() V157() V158() Element of omega
(card d) + (card G) is ordinal natural complex real finite cardinal V43() ext-real non negative V64() V153() V154() V155() V156() V157() V158() Element of NAT
d is finite set
card d is ordinal natural complex real finite cardinal V43() ext-real non negative V64() V153() V154() V155() V156() V157() V158() Element of omega
G is finite set
card G is ordinal natural complex real finite cardinal V43() ext-real non negative V64() V153() V154() V155() V156() V157() V158() Element of omega
d \+\ G is finite set
card (d \+\ G) is ordinal natural complex real finite cardinal V43() ext-real non negative V64() V153() V154() V155() V156() V157() V158() Element of omega
d \ G is finite Element of bool d
bool d is non empty finite V28() set
d /\ G is finite set
(d \ G) \/ (d /\ G) is finite set
G \ d is finite Element of bool G
bool G is non empty finite V28() set
(G \ d) \/ (d /\ G) is finite set
(d \ G) \/ (G \ d) is finite set
card (d \ G) is ordinal natural complex real finite cardinal V43() ext-real non negative V64() V153() V154() V155() V156() V157() V158() Element of omega
card (d /\ G) is ordinal natural complex real finite cardinal V43() ext-real non negative V64() V153() V154() V155() V156() V157() V158() Element of omega
card (G \ d) is ordinal natural complex real finite cardinal V43() ext-real non negative V64() V153() V154() V155() V156() V157() V158() Element of omega
d is ordinal natural complex real finite cardinal V43() ext-real non negative V64() V153() V154() V155() V156() V157() V158() Element of NAT
REAL d is non empty functional FinSequence-membered FinSequenceSet of REAL
Seg d is finite d -element V153() V154() V155() V156() V157() V158() Element of bool NAT
[:(Seg d),REAL:] is Relation-like V143() V144() V145() set
bool [:(Seg d),REAL:] is non empty set
G is set
d -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
Funcs ((Seg d),REAL) is non empty FUNCTION_DOMAIN of Seg d, REAL
G is FinSequenceSet of REAL
k is set
f is set
k is set
d is non empty ordinal natural complex real finite cardinal V43() ext-real positive non negative V64() V153() V154() V155() V156() V157() V158() Element of NAT
Seg d is non empty finite d -element V153() V154() V155() V156() V157() V158() Element of bool NAT
[:(Seg d),(bool REAL):] is non empty non trivial Relation-like non finite set
bool [:(Seg d),(bool REAL):] is non empty non trivial non finite set
G is set
the non empty non trivial finite V153() V154() V155() Element of bool REAL is non empty non trivial finite V153() V154() V155() Element of bool REAL
G is Relation-like Function-like set
dom G is set
k is set
G . k is set
k is Relation-like Seg d -defined bool REAL -valued Function-like finite quasi_total Element of bool [:(Seg d),(bool REAL):]
f is ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d
k . f is V153() V154() V155() Element of bool REAL
g is ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d
k . g is V153() V154() V155() Element of bool REAL
d is non empty ordinal natural complex real finite cardinal V43() ext-real positive non negative V64() V153() V154() V155() V156() V157() V158() Element of NAT
Seg d is non empty finite d -element V153() V154() V155() V156() V157() V158() Element of bool NAT
G is Relation-like Seg d -defined bool REAL -valued Function-like finite quasi_total (d)
k is set
G . k is set
d is non empty ordinal natural complex real finite cardinal V43() ext-real positive non negative V64() V153() V154() V155() V156() V157() V158() Element of NAT
Seg d is non empty finite d -element V153() V154() V155() V156() V157() V158() Element of bool NAT
G is Relation-like Seg d -defined bool REAL -valued Function-like finite finite-yielding quasi_total (d)
k is ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d
G . k is finite set
d is non empty ordinal natural complex real finite cardinal V43() ext-real positive non negative V64() V153() V154() V155() V156() V157() V158() Element of NAT
REAL d is non empty functional FinSequence-membered FinSequenceSet of REAL
Seg d is non empty finite d -element V153() V154() V155() V156() V157() V158() Element of bool NAT
G is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d
k is Relation-like Seg d -defined bool REAL -valued Function-like finite finite-yielding quasi_total (d)
product k is finite set
[:(Seg d),REAL:] is non empty non trivial Relation-like non finite V143() V144() V145() set
bool [:(Seg d),REAL:] is non empty non trivial non finite set
dom G is finite d -element V153() V154() V155() V156() V157() V158() Element of bool NAT
dom k is finite set
f is ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d
G . f is complex real ext-real Element of REAL
(d,k,f) is non empty non trivial finite V153() V154() V155() Element of bool REAL
f is set
G . f is complex real ext-real Element of REAL
k . f is finite set
d is non empty finite V153() V154() V155() Element of bool REAL
G is complex real ext-real Element of REAL
{G} is non empty trivial finite 1 -element V153() V154() V155() Element of bool REAL
k is complex real ext-real Element of REAL
G is complex real ext-real Element of REAL
{G} is non empty trivial finite 1 -element V153() V154() V155() Element of bool REAL
k is non empty finite V153() V154() V155() Element of bool REAL
k \/ {G} is non empty finite V153() V154() V155() Element of bool REAL
f is complex real ext-real Element of REAL
f is complex real ext-real Element of REAL
A is complex real ext-real Element of REAL
A is complex real ext-real Element of REAL
A is complex real ext-real Element of REAL
d is non empty finite V153() V154() V155() Element of bool REAL
G is complex real ext-real Element of REAL
{G} is non empty trivial finite 1 -element V153() V154() V155() Element of bool REAL
k is complex real ext-real Element of REAL
G is complex real ext-real Element of REAL
{G} is non empty trivial finite 1 -element V153() V154() V155() Element of bool REAL
k is non empty finite V153() V154() V155() Element of bool REAL
k \/ {G} is non empty finite V153() V154() V155() Element of bool REAL
f is complex real ext-real Element of REAL
f is complex real ext-real Element of REAL
A is complex real ext-real Element of REAL
A is complex real ext-real Element of REAL
A is complex real ext-real Element of REAL
d is non empty non trivial finite V153() V154() V155() Element of bool REAL
G is complex real ext-real Element of REAL
k is complex real ext-real Element of REAL
g is complex real ext-real Element of REAL
f is complex real ext-real Element of REAL
{f,g} is non empty finite V153() V154() V155() Element of bool REAL
A is complex real ext-real Element of REAL
{G,k} is non empty finite V153() V154() V155() Element of bool REAL
G is complex real ext-real Element of REAL
{G} is non empty trivial finite 1 -element V153() V154() V155() Element of bool REAL
k is non empty non trivial finite V153() V154() V155() Element of bool REAL
k \/ {G} is non empty non trivial finite V153() V154() V155() Element of bool REAL
f is complex real ext-real Element of REAL
g is complex real ext-real Element of REAL
f is complex real ext-real Element of REAL
g is complex real ext-real Element of REAL
A is complex real ext-real Element of REAL
A is complex real ext-real Element of REAL
A is complex real ext-real Element of REAL
d is non empty finite V153() V154() V155() Element of bool REAL
d is non empty non trivial finite V153() V154() V155() Element of bool REAL
G is complex real ext-real Element of REAL
k is complex real ext-real Element of REAL
f is set
g is set
A is complex real ext-real Element of REAL
A9 is complex real ext-real Element of REAL
f is complex real ext-real Element of REAL
d is non empty non trivial finite V153() V154() V155() Element of bool REAL
G is complex real ext-real Element of REAL
k is complex real ext-real Element of REAL
[G,k] is non empty non natural Element of [:REAL,REAL:]
{G,k} is non empty finite V153() V154() V155() set
{G} is non empty trivial finite 1 -element V153() V154() V155() set
{{G,k},{G}} is non empty finite V28() set
f is complex real ext-real Element of REAL
g is complex real ext-real Element of REAL
d is non empty non trivial finite V153() V154() V155() Element of bool REAL
G is complex real ext-real Element of REAL
k is complex real ext-real Element of REAL
[G,k] is non empty non natural Element of [:REAL,REAL:]
{G,k} is non empty finite V153() V154() V155() set
{G} is non empty trivial finite 1 -element V153() V154() V155() set
{{G,k},{G}} is non empty finite V28() set
f is complex real ext-real Element of REAL
g is complex real ext-real Element of REAL
[f,g] is non empty non natural Element of [:REAL,REAL:]
{f,g} is non empty finite V153() V154() V155() set
{f} is non empty trivial finite 1 -element V153() V154() V155() set
{{f,g},{f}} is non empty finite V28() set
A is complex real ext-real Element of REAL
A9 is complex real ext-real Element of REAL
d is non empty non trivial finite V153() V154() V155() Element of bool REAL
G is complex real ext-real Element of REAL
k is complex real ext-real Element of REAL
{G,k} is non empty finite V153() V154() V155() Element of bool REAL
f is complex real ext-real Element of REAL
g is complex real ext-real Element of REAL
[f,g] is non empty non natural Element of [:REAL,REAL:]
{f,g} is non empty finite V153() V154() V155() set
{f} is non empty trivial finite 1 -element V153() V154() V155() set
{{f,g},{f}} is non empty finite V28() set
A is non empty non trivial finite V153() V154() V155() Element of bool REAL
A9 is complex real ext-real Element of REAL
A99 is complex real ext-real Element of REAL
{A9,A99} is non empty finite V153() V154() V155() Element of bool REAL
[A9,A99] is non empty non natural Element of [:REAL,REAL:]
{A9,A99} is non empty finite V153() V154() V155() set
{A9} is non empty trivial finite 1 -element V153() V154() V155() set
{{A9,A99},{A9}} is non empty finite V28() set
B9 is complex real ext-real Element of REAL
A9 is complex real ext-real Element of REAL
d is non empty non trivial finite V153() V154() V155() Element of bool REAL
G is complex real ext-real Element of REAL
{ H₁(b₁) where b₁ is complex real ext-real Element of REAL : ( H₁(b₁) in d & S₁[b₁] ) } is set
f is finite V153() V154() V155() Element of bool REAL
g is complex real ext-real Element of REAL
g is complex real ext-real Element of REAL
[G,g] is non empty non natural Element of [:REAL,REAL:]
{G,g} is non empty finite V153() V154() V155() set
{G} is non empty trivial finite 1 -element V153() V154() V155() set
{{G,g},{G}} is non empty finite V28() set
A is set
A9 is complex real ext-real Element of REAL
{G} is non empty trivial finite 1 -element V153() V154() V155() Element of bool REAL
A is complex real ext-real Element of REAL
f is finite V153() V154() V155() Element of bool REAL
g is non empty finite V153() V154() V155() Element of bool REAL
A is complex real ext-real Element of REAL
[G,A] is non empty non natural Element of [:REAL,REAL:]
{G,A} is non empty finite V153() V154() V155() set
{G} is non empty trivial finite 1 -element V153() V154() V155() set
{{G,A},{G}} is non empty finite V28() set
A9 is complex real ext-real Element of REAL
A9 is complex real ext-real Element of REAL
f is finite V153() V154() V155() Element of bool REAL
d is non empty non trivial finite V153() V154() V155() Element of bool REAL
G is complex real ext-real Element of REAL
{ H₁(b₁) where b₁ is complex real ext-real Element of REAL : ( H₁(b₁) in d & S₁[b₁] ) } is set
f is finite V153() V154() V155() Element of bool REAL
g is complex real ext-real Element of REAL
g is complex real ext-real Element of REAL
[g,G] is non empty non natural Element of [:REAL,REAL:]
{g,G} is non empty finite V153() V154() V155() set
{g} is non empty trivial finite 1 -element V153() V154() V155() set
{{g,G},{g}} is non empty finite V28() set
A is set
A9 is complex real ext-real Element of REAL
{G} is non empty trivial finite 1 -element V153() V154() V155() Element of bool REAL
A is complex real ext-real Element of REAL
f is finite V153() V154() V155() Element of bool REAL
g is non empty finite V153() V154() V155() Element of bool REAL
A is complex real ext-real Element of REAL
[A,G] is non empty non natural Element of [:REAL,REAL:]
{A,G} is non empty finite V153() V154() V155() set
{A} is non empty trivial finite 1 -element V153() V154() V155() set
{{A,G},{A}} is non empty finite V28() set
A9 is complex real ext-real Element of REAL
A9 is complex real ext-real Element of REAL
f is finite V153() V154() V155() Element of bool REAL
d is non empty non trivial finite V153() V154() V155() Element of bool REAL
G is complex real ext-real Element of REAL
k is complex real ext-real Element of REAL
[G,k] is non empty non natural Element of [:REAL,REAL:]
{G,k} is non empty finite V153() V154() V155() set
{G} is non empty trivial finite 1 -element V153() V154() V155() set
{{G,k},{G}} is non empty finite V28() set
f is complex real ext-real Element of REAL
[G,f] is non empty non natural Element of [:REAL,REAL:]
{G,f} is non empty finite V153() V154() V155() set
{{G,f},{G}} is non empty finite V28() set
g is complex real ext-real Element of REAL
A is complex real ext-real Element of REAL
d is non empty non trivial finite V153() V154() V155() Element of bool REAL
G is complex real ext-real Element of REAL
k is complex real ext-real Element of REAL
[G,k] is non empty non natural Element of [:REAL,REAL:]
{G,k} is non empty finite V153() V154() V155() set
{G} is non empty trivial finite 1 -element V153() V154() V155() set
{{G,k},{G}} is non empty finite V28() set
f is complex real ext-real Element of REAL
[f,k] is non empty non natural Element of [:REAL,REAL:]
{f,k} is non empty finite V153() V154() V155() set
{f} is non empty trivial finite 1 -element V153() V154() V155() set
{{f,k},{f}} is non empty finite V28() set
g is complex real ext-real Element of REAL
A is complex real ext-real Element of REAL
d is non empty non trivial finite V153() V154() V155() Element of bool REAL
G is complex real ext-real Element of REAL
k is complex real ext-real Element of REAL
[k,G] is non empty non natural Element of [:REAL,REAL:]
{k,G} is non empty finite V153() V154() V155() set
{k} is non empty trivial finite 1 -element V153() V154() V155() set
{{k,G},{k}} is non empty finite V28() set
f is complex real ext-real Element of REAL
g is complex real ext-real Element of REAL
[g,f] is non empty non natural Element of [:REAL,REAL:]
{g,f} is non empty finite V153() V154() V155() set
{g} is non empty trivial finite 1 -element V153() V154() V155() set
{{g,f},{g}} is non empty finite V28() set
d is non empty ordinal natural complex real finite cardinal V43() ext-real positive non negative V64() V153() V154() V155() V156() V157() V158() Element of NAT
REAL d is non empty functional FinSequence-membered FinSequenceSet of REAL
Seg d is non empty finite d -element V153() V154() V155() V156() V157() V158() Element of bool NAT
G is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d
k is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d : ( for b₂ being ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d holds
( G . b₂ <= b₁ . b₂ & b₁ . b₂ <= k . b₂ ) or ex b₂ being ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d st
( not G . b₂ <= k . b₂ & ( b₁ . b₂ <= k . b₂ or G . b₂ <= b₁ . b₂ ) ) ) } is set
bool (REAL d) is non empty set
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d : S₁[b₁] } is set
g is ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d
G . g is complex real ext-real Element of REAL
A is ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d
G . A is complex real ext-real Element of REAL
k . A is complex real ext-real Element of REAL
g is ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d
G . g is complex real ext-real Element of REAL
k . g is complex real ext-real Element of REAL
d is non empty ordinal natural complex real finite cardinal V43() ext-real positive non negative V64() V153() V154() V155() V156() V157() V158() Element of NAT
REAL d is non empty functional FinSequence-membered FinSequenceSet of REAL
Seg d is non empty finite d -element V153() V154() V155() V156() V157() V158() Element of bool NAT
G is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d
k is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d
f is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d
(d,k,f) is non empty functional FinSequence-membered Element of bool (REAL d)
bool (REAL d) is non empty set
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d : ( for b₂ being ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d holds
( k . b₂ <= b₁ . b₂ & b₁ . b₂ <= f . b₂ ) or ex b₂ being ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d st
( not k . b₂ <= f . b₂ & ( b₁ . b₂ <= f . b₂ or k . b₂ <= b₁ . b₂ ) ) ) } is set
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d : S₁[b₁] } is set
d is non empty ordinal natural complex real finite cardinal V43() ext-real positive non negative V64() V153() V154() V155() V156() V157() V158() Element of NAT
REAL d is non empty functional FinSequence-membered FinSequenceSet of REAL
Seg d is non empty finite d -element V153() V154() V155() V156() V157() V158() Element of bool NAT
G is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d
k is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d
(d,G,k) is non empty functional FinSequence-membered Element of bool (REAL d)
bool (REAL d) is non empty set
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d : ( for b₂ being ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d holds
( G . b₂ <= b₁ . b₂ & b₁ . b₂ <= k . b₂ ) or ex b₂ being ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d st
( not G . b₂ <= k . b₂ & ( b₁ . b₂ <= k . b₂ or G . b₂ <= b₁ . b₂ ) ) ) } is set
f is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d
g is ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d
G . g is complex real ext-real Element of REAL
f . g is complex real ext-real Element of REAL
A is ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d
f . A is complex real ext-real Element of REAL
k . A is complex real ext-real Element of REAL
g is ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d
G . g is complex real ext-real Element of REAL
f . g is complex real ext-real Element of REAL
A is ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d
f . A is complex real ext-real Element of REAL
k . A is complex real ext-real Element of REAL
A9 is ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d
G . A9 is complex real ext-real Element of REAL
k . A9 is complex real ext-real Element of REAL
f . A9 is complex real ext-real Element of REAL
d is non empty ordinal natural complex real finite cardinal V43() ext-real positive non negative V64() V153() V154() V155() V156() V157() V158() Element of NAT
REAL d is non empty functional FinSequence-membered FinSequenceSet of REAL
Seg d is non empty finite d -element V153() V154() V155() V156() V157() V158() Element of bool NAT
G is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d
k is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d
(d,k,G) is non empty functional FinSequence-membered Element of bool (REAL d)
bool (REAL d) is non empty set
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d : ( for b₂ being ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d holds
( k . b₂ <= b₁ . b₂ & b₁ . b₂ <= G . b₂ ) or ex b₂ being ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d st
( not k . b₂ <= G . b₂ & ( b₁ . b₂ <= G . b₂ or k . b₂ <= b₁ . b₂ ) ) ) } is set
f is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d
g is ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d
k . g is complex real ext-real Element of REAL
G . g is complex real ext-real Element of REAL
f . g is complex real ext-real Element of REAL
A is ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d
k . A is complex real ext-real Element of REAL
G . A is complex real ext-real Element of REAL
f . A is complex real ext-real Element of REAL
d is non empty ordinal natural complex real finite cardinal V43() ext-real positive non negative V64() V153() V154() V155() V156() V157() V158() Element of NAT
REAL d is non empty functional FinSequence-membered FinSequenceSet of REAL
G is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d
k is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d
(d,G,k) is non empty functional FinSequence-membered Element of bool (REAL d)
bool (REAL d) is non empty set
Seg d is non empty finite d -element V153() V154() V155() V156() V157() V158() Element of bool NAT
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d : ( for b₂ being ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d holds
( G . b₂ <= b₁ . b₂ & b₁ . b₂ <= k . b₂ ) or ex b₂ being ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d st
( not G . b₂ <= k . b₂ & ( b₁ . b₂ <= k . b₂ or G . b₂ <= b₁ . b₂ ) ) ) } is set
f is ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d
G . f is complex real ext-real Element of REAL
g is ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d
G . g is complex real ext-real Element of REAL
k . g is complex real ext-real Element of REAL
f is ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d
G . f is complex real ext-real Element of REAL
k . f is complex real ext-real Element of REAL
g is ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d
k . g is complex real ext-real Element of REAL
f is ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d
G . f is complex real ext-real Element of REAL
k . f is complex real ext-real Element of REAL
g is ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d
G . g is complex real ext-real Element of REAL
k . g is complex real ext-real Element of REAL
d is non empty ordinal natural complex real finite cardinal V43() ext-real positive non negative V64() V153() V154() V155() V156() V157() V158() Element of NAT
REAL d is non empty functional FinSequence-membered FinSequenceSet of REAL
G is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d
(d,G,G) is non empty functional FinSequence-membered Element of bool (REAL d)
bool (REAL d) is non empty set
Seg d is non empty finite d -element V153() V154() V155() V156() V157() V158() Element of bool NAT
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d : ( for b₂ being ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d holds
( G . b₂ <= b₁ . b₂ & b₁ . b₂ <= G . b₂ ) or ex b₂ being ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d st
( not G . b₂ <= G . b₂ & ( b₁ . b₂ <= G . b₂ or G . b₂ <= b₁ . b₂ ) ) ) } is set
{G} is non empty trivial functional finite V28() 1 -element FinSequence-membered Element of bool (REAL d)
k is set
[:(Seg d),REAL:] is non empty non trivial Relation-like non finite V143() V144() V145() set
bool [:(Seg d),REAL:] is non empty non trivial non finite set
f is Relation-like Seg d -defined REAL -valued Function-like finite quasi_total V143() V144() V145() Element of bool [:(Seg d),REAL:]
A9 is ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d
f . A9 is complex real ext-real Element of REAL
A is ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d
f . A is complex real ext-real Element of REAL
g is Relation-like Seg d -defined REAL -valued Function-like finite quasi_total V143() V144() V145() Element of bool [:(Seg d),REAL:]
g . A is complex real ext-real Element of REAL
d is non empty ordinal natural complex real finite cardinal V43() ext-real positive non negative V64() V153() V154() V155() V156() V157() V158() Element of NAT
REAL d is non empty functional FinSequence-membered FinSequenceSet of REAL
Seg d is non empty finite d -element V153() V154() V155() V156() V157() V158() Element of bool NAT
G is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d
k is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d
(d,G,k) is non empty functional FinSequence-membered Element of bool (REAL d)
bool (REAL d) is non empty set
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d : ( for b₂ being ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d holds
( G . b₂ <= b₁ . b₂ & b₁ . b₂ <= k . b₂ ) or ex b₂ being ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d st
( not G . b₂ <= k . b₂ & ( b₁ . b₂ <= k . b₂ or G . b₂ <= b₁ . b₂ ) ) ) } is set
f is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d
g is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d
(d,f,g) is non empty functional FinSequence-membered Element of bool (REAL d)
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d : ( for b₂ being ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d holds
( f . b₂ <= b₁ . b₂ & b₁ . b₂ <= g . b₂ ) or ex b₂ being ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d st
( not f . b₂ <= g . b₂ & ( b₁ . b₂ <= g . b₂ or f . b₂ <= b₁ . b₂ ) ) ) } is set
A is ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d
G . A is complex real ext-real Element of REAL
f . A is complex real ext-real Element of REAL
g . A is complex real ext-real Element of REAL
k . A is complex real ext-real Element of REAL
A9 is ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d
f . A9 is complex real ext-real Element of REAL
k . A9 is complex real ext-real Element of REAL
[:(Seg d),REAL:] is non empty non trivial Relation-like non finite V143() V144() V145() set
bool [:(Seg d),REAL:] is non empty non trivial non finite set
A9 is Relation-like Seg d -defined REAL -valued Function-like finite quasi_total V143() V144() V145() Element of bool [:(Seg d),REAL:]
A99 is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d
A99 . A is complex real ext-real Element of REAL
B9 is ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d
f . B9 is complex real ext-real Element of REAL
g . B9 is complex real ext-real Element of REAL
A99 . B9 is complex real ext-real Element of REAL
A99 . A is complex real ext-real Element of REAL
B9 is ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d
G . B9 is complex real ext-real Element of REAL
A99 . B9 is complex real ext-real Element of REAL
A9 is ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d
A99 . A9 is complex real ext-real Element of REAL
k . A9 is complex real ext-real Element of REAL
A is set
A99 is ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d
G . A99 is complex real ext-real Element of REAL
f . A99 is complex real ext-real Element of REAL
A9 is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d
A9 . A99 is complex real ext-real Element of REAL
g . A99 is complex real ext-real Element of REAL
k . A99 is complex real ext-real Element of REAL
d is non empty ordinal natural complex real finite cardinal V43() ext-real positive non negative V64() V153() V154() V155() V156() V157() V158() Element of NAT
REAL d is non empty functional FinSequence-membered FinSequenceSet of REAL
Seg d is non empty finite d -element V153() V154() V155() V156() V157() V158() Element of bool NAT
G is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d
k is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d
(d,k,G) is non empty functional FinSequence-membered Element of bool (REAL d)
bool (REAL d) is non empty set
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d : ( for b₂ being ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d holds
( k . b₂ <= b₁ . b₂ & b₁ . b₂ <= G . b₂ ) or ex b₂ being ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d st
( not k . b₂ <= G . b₂ & ( b₁ . b₂ <= G . b₂ or k . b₂ <= b₁ . b₂ ) ) ) } is set
f is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d
g is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d
(d,f,g) is non empty functional FinSequence-membered Element of bool (REAL d)
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d : ( for b₂ being ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d holds
( f . b₂ <= b₁ . b₂ & b₁ . b₂ <= g . b₂ ) or ex b₂ being ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d st
( not f . b₂ <= g . b₂ & ( b₁ . b₂ <= g . b₂ or f . b₂ <= b₁ . b₂ ) ) ) } is set
A is ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d
f . A is complex real ext-real Element of REAL
g . A is complex real ext-real Element of REAL
A9 is ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d
k . A9 is complex real ext-real Element of REAL
g . A9 is complex real ext-real Element of REAL
f . A9 is complex real ext-real Element of REAL
A99 is complex real ext-real Element of REAL
A99 is complex real ext-real Element of REAL
[:(Seg d),REAL:] is non empty non trivial Relation-like non finite V143() V144() V145() set
bool [:(Seg d),REAL:] is non empty non trivial non finite set
A9 is Relation-like Seg d -defined REAL -valued Function-like finite quasi_total V143() V144() V145() Element of bool [:(Seg d),REAL:]
k . A is complex real ext-real Element of REAL
G . A is complex real ext-real Element of REAL
A99 is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d
A99 . A is complex real ext-real Element of REAL
B9 is ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d
f . B9 is complex real ext-real Element of REAL
g . B9 is complex real ext-real Element of REAL
A99 . B9 is complex real ext-real Element of REAL
B9 is ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d
f . B9 is complex real ext-real Element of REAL
A99 . B9 is complex real ext-real Element of REAL
A9 is ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d
A99 . A9 is complex real ext-real Element of REAL
g . A9 is complex real ext-real Element of REAL
A is ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d
G . A is complex real ext-real Element of REAL
g . A is complex real ext-real Element of REAL
f . A is complex real ext-real Element of REAL
k . A is complex real ext-real Element of REAL
A9 is ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d
g . A9 is complex real ext-real Element of REAL
f . A9 is complex real ext-real Element of REAL
G . A9 is complex real ext-real Element of REAL
A99 is complex real ext-real Element of REAL
A99 is complex real ext-real Element of REAL
A99 is complex real ext-real Element of REAL
[:(Seg d),REAL:] is non empty non trivial Relation-like non finite V143() V144() V145() set
bool [:(Seg d),REAL:] is non empty non trivial non finite set
A9 is Relation-like Seg d -defined REAL -valued Function-like finite quasi_total V143() V144() V145() Element of bool [:(Seg d),REAL:]
A99 is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d
A99 . A is complex real ext-real Element of REAL
B9 is ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d
f . B9 is complex real ext-real Element of REAL
g . B9 is complex real ext-real Element of REAL
A99 . B9 is complex real ext-real Element of REAL
A9 is ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d
f . A9 is complex real ext-real Element of REAL
g . A9 is complex real ext-real Element of REAL
k . A9 is complex real ext-real Element of REAL
A99 is complex real ext-real Element of REAL
A99 is complex real ext-real Element of REAL
A99 is complex real ext-real Element of REAL
A9 is Relation-like Seg d -defined REAL -valued Function-like finite quasi_total V143() V144() V145() Element of bool [:(Seg d),REAL:]
A99 is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d
A99 . A is complex real ext-real Element of REAL
B9 is ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d
f . B9 is complex real ext-real Element of REAL
g . B9 is complex real ext-real Element of REAL
A99 . B9 is complex real ext-real Element of REAL
A is set
the ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d is ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d
G . the ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d is complex real ext-real Element of REAL
g . the ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d is complex real ext-real Element of REAL
f . the ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d is complex real ext-real Element of REAL
k . the ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d is complex real ext-real Element of REAL
A9 is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d
A9 . the ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d is complex real ext-real Element of REAL
B9 is ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d
k . B9 is complex real ext-real Element of REAL
G . B9 is complex real ext-real Element of REAL
A9 . B9 is complex real ext-real Element of REAL
g . B9 is complex real ext-real Element of REAL
f . B9 is complex real ext-real Element of REAL
d is non empty ordinal natural complex real finite cardinal V43() ext-real positive non negative V64() V153() V154() V155() V156() V157() V158() Element of NAT
REAL d is non empty functional FinSequence-membered FinSequenceSet of REAL
Seg d is non empty finite d -element V153() V154() V155() V156() V157() V158() Element of bool NAT
G is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d
k is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d
(d,G,k) is non empty functional FinSequence-membered Element of bool (REAL d)
bool (REAL d) is non empty set
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d : ( for b₂ being ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d holds
( G . b₂ <= b₁ . b₂ & b₁ . b₂ <= k . b₂ ) or ex b₂ being ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d st
( not G . b₂ <= k . b₂ & ( b₁ . b₂ <= k . b₂ or G . b₂ <= b₁ . b₂ ) ) ) } is set
f is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d
g is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d
(d,g,f) is non empty functional FinSequence-membered Element of bool (REAL d)
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d : ( for b₂ being ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d holds
( g . b₂ <= b₁ . b₂ & b₁ . b₂ <= f . b₂ ) or ex b₂ being ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d st
( not g . b₂ <= f . b₂ & ( b₁ . b₂ <= f . b₂ or g . b₂ <= b₁ . b₂ ) ) ) } is set
A is ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d
G . A is complex real ext-real Element of REAL
k . A is complex real ext-real Element of REAL
f . A is complex real ext-real Element of REAL
g . A is complex real ext-real Element of REAL
A9 is complex real ext-real Element of REAL
[:(Seg d),REAL:] is non empty non trivial Relation-like non finite V143() V144() V145() set
bool [:(Seg d),REAL:] is non empty non trivial non finite set
A is Relation-like Seg d -defined REAL -valued Function-like finite quasi_total V143() V144() V145() Element of bool [:(Seg d),REAL:]
A9 is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d
the ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d is ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d
g . the ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d is complex real ext-real Element of REAL
f . the ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d is complex real ext-real Element of REAL
B9 is ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d
g . B9 is complex real ext-real Element of REAL
f . B9 is complex real ext-real Element of REAL
A9 . B9 is complex real ext-real Element of REAL
A is ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d
k . A is complex real ext-real Element of REAL
f . A is complex real ext-real Element of REAL
g . A is complex real ext-real Element of REAL
G . A is complex real ext-real Element of REAL
A9 is set
A99 is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d
A99 . A is complex real ext-real Element of REAL
B9 is ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d
g . B9 is complex real ext-real Element of REAL
f . B9 is complex real ext-real Element of REAL
A99 . B9 is complex real ext-real Element of REAL
d is non empty ordinal natural complex real finite cardinal V43() ext-real positive non negative V64() V153() V154() V155() V156() V157() V158() Element of NAT
REAL d is non empty functional FinSequence-membered FinSequenceSet of REAL
Seg d is non empty finite d -element V153() V154() V155() V156() V157() V158() Element of bool NAT
G is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d
k is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d
(d,G,k) is non empty functional FinSequence-membered Element of bool (REAL d)
bool (REAL d) is non empty set
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d : ( for b₂ being ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d holds
( G . b₂ <= b₁ . b₂ & b₁ . b₂ <= k . b₂ ) or ex b₂ being ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d st
( not G . b₂ <= k . b₂ & ( b₁ . b₂ <= k . b₂ or G . b₂ <= b₁ . b₂ ) ) ) } is set
f is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d
g is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d
(d,f,g) is non empty functional FinSequence-membered Element of bool (REAL d)
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d : ( for b₂ being ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d holds
( f . b₂ <= b₁ . b₂ & b₁ . b₂ <= g . b₂ ) or ex b₂ being ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d st
( not f . b₂ <= g . b₂ & ( b₁ . b₂ <= g . b₂ or f . b₂ <= b₁ . b₂ ) ) ) } is set
A is ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d
G . A is complex real ext-real Element of REAL
f . A is complex real ext-real Element of REAL
A9 is ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d
f . A9 is complex real ext-real Element of REAL
g . A9 is complex real ext-real Element of REAL
A99 is ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d
g . A99 is complex real ext-real Element of REAL
k . A99 is complex real ext-real Element of REAL
[:(Seg d),REAL:] is non empty non trivial Relation-like non finite V143() V144() V145() set
bool [:(Seg d),REAL:] is non empty non trivial non finite set
A is Relation-like Seg d -defined REAL -valued Function-like finite quasi_total V143() V144() V145() Element of bool [:(Seg d),REAL:]
A9 is ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d
A . A9 is complex real ext-real Element of REAL
A99 is Relation-like Seg d -defined REAL -valued Function-like finite quasi_total V143() V144() V145() Element of bool [:(Seg d),REAL:]
A99 . A9 is complex real ext-real Element of REAL
A9 is Relation-like Seg d -defined REAL -valued Function-like finite quasi_total V143() V144() V145() Element of bool [:(Seg d),REAL:]
A9 is ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d
A9 . A9 is complex real ext-real Element of REAL
B9 is Relation-like Seg d -defined REAL -valued Function-like finite quasi_total V143() V144() V145() Element of bool [:(Seg d),REAL:]
B9 . A9 is complex real ext-real Element of REAL
A is ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d
k . A is complex real ext-real Element of REAL
g . A is complex real ext-real Element of REAL
A9 is ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d
f . A9 is complex real ext-real Element of REAL
g . A9 is complex real ext-real Element of REAL
A99 is ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d
f . A99 is complex real ext-real Element of REAL
G . A99 is complex real ext-real Element of REAL
[:(Seg d),REAL:] is non empty non trivial Relation-like non finite V143() V144() V145() set
bool [:(Seg d),REAL:] is non empty non trivial non finite set
A is Relation-like Seg d -defined REAL -valued Function-like finite quasi_total V143() V144() V145() Element of bool [:(Seg d),REAL:]
A9 is ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d
A . A9 is complex real ext-real Element of REAL
A99 is Relation-like Seg d -defined REAL -valued Function-like finite quasi_total V143() V144() V145() Element of bool [:(Seg d),REAL:]
A99 . A9 is complex real ext-real Element of REAL
A9 is Relation-like Seg d -defined REAL -valued Function-like finite quasi_total V143() V144() V145() Element of bool [:(Seg d),REAL:]
A9 is ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d
A9 . A9 is complex real ext-real Element of REAL
B9 is Relation-like Seg d -defined REAL -valued Function-like finite quasi_total V143() V144() V145() Element of bool [:(Seg d),REAL:]
B9 . A9 is complex real ext-real Element of REAL
A is ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d
G . A is complex real ext-real Element of REAL
k . A is complex real ext-real Element of REAL
A9 is ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d
G . A9 is complex real ext-real Element of REAL
k . A9 is complex real ext-real Element of REAL
d is non empty ordinal natural complex real finite cardinal V43() ext-real positive non negative V64() V153() V154() V155() V156() V157() V158() Element of NAT
Seg d is non empty finite d -element V153() V154() V155() V156() V157() V158() Element of bool NAT
k is ordinal natural complex real finite cardinal V43() ext-real non negative V64() V153() V154() V155() V156() V157() V158() Element of NAT
REAL d is non empty functional FinSequence-membered FinSequenceSet of REAL
bool (Seg d) is non empty finite V28() set
G is Relation-like Seg d -defined bool REAL -valued Function-like finite finite-yielding quasi_total (d)
{ (d,b₁,b₂) where b₁, b₂ is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d : ( ex b₃ being finite V153() V154() V155() V156() V157() V158() Element of bool (Seg d) st
( card b₃ = k & ( for b₄ being ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d holds
( ( b₄ in b₃ & not b₂ . b₄ <= b₁ . b₄ & [(b₁ . b₄),(b₂ . b₄)] is ((d,G,b₄)) ) or ( not b₄ in b₃ & b₁ . b₄ = b₂ . b₄ & b₁ . b₄ in (d,G,b₄) ) ) ) ) or ( k = d & ( for b₃ being ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d holds
( not b₁ . b₃ <= b₂ . b₃ & [(b₁ . b₃),(b₂ . b₃)] is ((d,G,b₃)) ) ) ) ) } is set
bool (REAL d) is non empty set
bool (bool (REAL d)) is non empty set
{ H₂(b₁,b₂) where b₁, b₂ is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d : S₁[b₁,b₂] } is set
Seg k is finite k -element V153() V154() V155() V156() V157() V158() Element of bool NAT
g is finite V153() V154() V155() V156() V157() V158() Element of bool (Seg d)
A is ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d
(d,G,A) is non empty non trivial finite V153() V154() V155() Element of bool REAL
A9 is complex real ext-real Element of REAL
A99 is complex real ext-real Element of REAL
[A9,A99] is non empty non natural Element of [:REAL,REAL:]
{A9,A99} is non empty finite V153() V154() V155() set
{A9} is non empty trivial finite 1 -element V153() V154() V155() set
{{A9,A99},{A9}} is non empty finite V28() set
the complex real ext-real Element of (d,G,A) is complex real ext-real Element of (d,G,A)
A99 is complex real ext-real Element of REAL
[A99,A99] is non empty non natural Element of [:REAL,REAL:]
{A99,A99} is non empty finite V153() V154() V155() set
{A99} is non empty trivial finite 1 -element V153() V154() V155() set
{{A99,A99},{A99}} is non empty finite V28() set
B9 is Element of [:REAL,REAL:]
[:(Seg d),[:REAL,REAL:]:] is non empty non trivial Relation-like non finite set
bool [:(Seg d),[:REAL,REAL:]:] is non empty non trivial non finite set
A is Relation-like Seg d -defined [:REAL,REAL:] -valued Function-like finite quasi_total Element of bool [:(Seg d),[:REAL,REAL:]:]
[:(Seg d),REAL:] is non empty non trivial Relation-like non finite V143() V144() V145() set
bool [:(Seg d),REAL:] is non empty non trivial non finite set
A9 is Relation-like Seg d -defined REAL -valued Function-like finite quasi_total V143() V144() V145() Element of bool [:(Seg d),REAL:]
A99 is Relation-like Seg d -defined REAL -valued Function-like finite quasi_total V143() V144() V145() Element of bool [:(Seg d),REAL:]
B9 is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d
B9 is ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d
B9 . B9 is complex real ext-real Element of REAL
A . B9 is Element of [:REAL,REAL:]
(A . B9) `1 is complex real ext-real Element of REAL
A9 is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d
A9 . B9 is complex real ext-real Element of REAL
(A . B9) `2 is complex real ext-real Element of REAL
[(B9 . B9),(A9 . B9)] is non empty non natural Element of [:REAL,REAL:]
{(B9 . B9),(A9 . B9)} is non empty finite V153() V154() V155() set
{(B9 . B9)} is non empty trivial finite 1 -element V153() V154() V155() set
{{(B9 . B9),(A9 . B9)},{(B9 . B9)}} is non empty finite V28() set
(d,B9,A9) is non empty functional FinSequence-membered Element of bool (REAL d)
{ b₁ where b₁ is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d : ( for b₂ being ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d holds
( B9 . b₂ <= b₁ . b₂ & b₁ . b₂ <= A9 . b₂ ) or ex b₂ being ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d st
( not B9 . b₂ <= A9 . b₂ & ( b₁ . b₂ <= A9 . b₂ or B9 . b₂ <= b₁ . b₂ ) ) ) } is set
B9 is non empty functional FinSequence-membered Element of bool (REAL d)
A1 is finite V153() V154() V155() V156() V157() V158() Element of bool (Seg d)
card A1 is ordinal natural complex real finite cardinal V43() ext-real non negative V64() V153() V154() V155() V156() V157() V158() Element of omega
B1 is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d
A2 is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d