:: 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
is non empty non trivial Relation-like non finite V143() V144() V145() set
is non empty non trivial Relation-like non finite V143() V144() V145() set
bool 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 is non empty non trivial non finite set

the carrier of K388(2) is non empty 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

max (k,f) is complex real ext-real set
(max (k,f)) + 1 is complex real ext-real Element of REAL

F1() is non empty set
F2() is non empty set
{ F3(b1,b2) where b1, b2 is Element of F2() : P1[b1,b2] } is set
d is set
G is Element of F2()
k is Element of F2()
F3(G,k) is Element of F1()
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
F1() is non empty set
bool F1() is non empty set
F2() is non empty finite Element of bool F1()
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 F1()
k is Element of bool F1()
k is Element of bool F1()
k is Element of bool F1()
F1() is non empty non trivial set
bool F1() is non empty set
F2() is non empty non trivial finite Element of bool F1()
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 F1()
k \/ {d} is non empty set
k is Element of bool F1()
k is Element of bool F1()
k is Element of bool F1()
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 F1()
k \/ {d} is non empty set
d is 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

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

G is finite set

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

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

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),():] is non empty non trivial Relation-like non finite set
bool [:(Seg d),():] 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

dom G is set
k is set
G . k is set

k . f is V153() V154() V155() Element of bool REAL

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

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

Seg d is non empty finite d -element V153() V154() V155() V156() V157() V158() Element of bool NAT

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

(d,k,f) is non empty non trivial finite V153() V154() V155() Element of bool REAL
f is set

k . f is finite set
d is non empty finite V153() V154() V155() Element of bool REAL

{G} is non empty trivial finite 1 -element V153() V154() V155() Element of bool 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

d is non empty finite V153() V154() V155() Element of bool REAL

{G} is non empty trivial finite 1 -element V153() V154() V155() Element of bool 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

d is non empty non trivial finite V153() V154() V155() Element of bool REAL

{f,g} is non empty finite V153() V154() V155() Element of bool REAL

{G,k} is non empty finite V153() V154() V155() Element of bool 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

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

f is set
g is set

d is non empty non trivial finite V153() V154() V155() Element of bool REAL

[G,k] is non empty non natural Element of
{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

d is non empty non trivial finite V153() V154() V155() Element of bool REAL

[G,k] is non empty non natural Element of
{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,g] is non empty non natural Element of
{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

d is non empty non trivial finite V153() V154() V155() Element of bool REAL

{G,k} is non empty finite V153() V154() V155() Element of bool REAL

[f,g] is non empty non natural Element of
{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,A99} is non empty finite V153() V154() V155() Element of bool REAL
[A9,A99] is non empty non natural Element of
{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

d is non empty non trivial finite V153() V154() V155() Element of bool REAL

{ H1(b1) where b1 is complex real ext-real Element of REAL : ( H1(b1) in d & S1[b1] ) } is set
f is finite V153() V154() V155() Element of bool REAL

[G,g] is non empty non natural Element of
{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

{G} is non empty trivial finite 1 -element V153() V154() V155() Element of bool REAL

f is finite V153() V154() V155() Element of bool REAL
g is non empty finite V153() V154() V155() Element of bool REAL

[G,A] is non empty non natural Element of
{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

f is finite V153() V154() V155() Element of bool REAL
d is non empty non trivial finite V153() V154() V155() Element of bool REAL

{ H1(b1) where b1 is complex real ext-real Element of REAL : ( H1(b1) in d & S1[b1] ) } is set
f is finite V153() V154() V155() Element of bool REAL

[g,G] is non empty non natural Element of
{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

{G} is non empty trivial finite 1 -element V153() V154() V155() Element of bool REAL

f is finite V153() V154() V155() Element of bool REAL
g is non empty finite V153() V154() V155() Element of bool REAL

[A,G] is non empty non natural Element of
{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

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,k] is non empty non natural Element of
{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

[G,f] is non empty non natural Element of
{G,f} is non empty finite V153() V154() V155() set
{{G,f},{G}} is non empty finite V28() set

d is non empty non trivial finite V153() V154() V155() Element of bool REAL

[G,k] is non empty non natural Element of
{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,k] is non empty non natural Element of
{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

d is non empty non trivial finite V153() V154() V155() Element of bool REAL

[k,G] is non empty non natural Element of
{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

[g,f] is non empty non natural Element of
{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

Seg d is non empty finite d -element V153() V154() V155() V156() V157() V158() Element of bool NAT

{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d : ( for b2 being ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d holds
( G . b2 <= b1 . b2 & b1 . b2 <= k . b2 ) or ex b2 being ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d st
( not G . b2 <= k . b2 & ( b1 . b2 <= k . b2 or G . b2 <= b1 . b2 ) ) )
}
is set

bool (REAL d) is non empty set
{ } 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

(d,k,f) is non empty functional FinSequence-membered Element of bool (REAL d)
bool (REAL d) is non empty set
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d : ( for b2 being ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d holds
( k . b2 <= b1 . b2 & b1 . b2 <= f . b2 ) or ex b2 being ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d st
( not k . b2 <= f . b2 & ( b1 . b2 <= f . b2 or k . b2 <= b1 . b2 ) ) )
}
is set

{ } 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

(d,G,k) is non empty functional FinSequence-membered Element of bool (REAL d)
bool (REAL d) is non empty set
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d : ( for b2 being ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d holds
( G . b2 <= b1 . b2 & b1 . b2 <= k . b2 ) or ex b2 being ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d st
( not G . b2 <= k . b2 & ( b1 . b2 <= k . b2 or G . b2 <= b1 . b2 ) ) )
}
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

(d,k,G) is non empty functional FinSequence-membered Element of bool (REAL d)
bool (REAL d) is non empty set
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d : ( for b2 being ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d holds
( k . b2 <= b1 . b2 & b1 . b2 <= G . b2 ) or ex b2 being ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d st
( not k . b2 <= G . b2 & ( b1 . b2 <= G . b2 or k . b2 <= b1 . b2 ) ) )
}
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

(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
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d : ( for b2 being ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d holds
( G . b2 <= b1 . b2 & b1 . b2 <= k . b2 ) or ex b2 being ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d st
( not G . b2 <= k . b2 & ( b1 . b2 <= k . b2 or G . b2 <= b1 . b2 ) ) )
}
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

(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
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d : ( for b2 being ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d holds
( G . b2 <= b1 . b2 & b1 . b2 <= G . b2 ) or ex b2 being ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d st
( not G . b2 <= G . b2 & ( b1 . b2 <= G . b2 or G . b2 <= b1 . b2 ) ) )
}
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

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

(d,G,k) is non empty functional FinSequence-membered Element of bool (REAL d)
bool (REAL d) is non empty set
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d : ( for b2 being ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d holds
( G . b2 <= b1 . b2 & b1 . b2 <= k . b2 ) or ex b2 being ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d st
( not G . b2 <= k . b2 & ( b1 . b2 <= k . b2 or G . b2 <= b1 . b2 ) ) )
}
is set

(d,f,g) is non empty functional FinSequence-membered Element of bool (REAL d)
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d : ( for b2 being ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d holds
( f . b2 <= b1 . b2 & b1 . b2 <= g . b2 ) or ex b2 being ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d st
( not f . b2 <= g . b2 & ( b1 . b2 <= g . b2 or f . b2 <= b1 . b2 ) ) )
}
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

A99 . A 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

A99 . B9 is complex real ext-real Element of REAL

A99 . A9 is complex real ext-real Element of REAL

A is set

G . A99 is complex real ext-real Element of REAL
f . A99 is complex real ext-real Element of REAL

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

Seg d is non empty finite d -element V153() V154() V155() V156() V157() V158() Element of bool NAT

(d,k,G) is non empty functional FinSequence-membered Element of bool (REAL d)
bool (REAL d) is non empty set
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d : ( for b2 being ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d holds
( k . b2 <= b1 . b2 & b1 . b2 <= G . b2 ) or ex b2 being ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d st
( not k . b2 <= G . b2 & ( b1 . b2 <= G . b2 or k . b2 <= b1 . b2 ) ) )
}
is set

(d,f,g) is non empty functional FinSequence-membered Element of bool (REAL d)
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d : ( for b2 being ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d holds
( f . b2 <= b1 . b2 & b1 . b2 <= g . b2 ) or ex b2 being ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d st
( not f . b2 <= g . b2 & ( b1 . b2 <= g . b2 or f . b2 <= b1 . b2 ) ) )
}
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

A99 . A is complex real ext-real Element of REAL

A99 . B9 is complex real ext-real Element of REAL

A99 . B9 is complex real ext-real Element of REAL

A99 . 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

A99 . A 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

A99 . B9 is complex real ext-real Element of REAL
A is set

A9 . 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

Seg d is non empty finite d -element V153() V154() V155() V156() V157() V158() Element of bool NAT

(d,G,k) is non empty functional FinSequence-membered Element of bool (REAL d)
bool (REAL d) is non empty set
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d : ( for b2 being ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d holds
( G . b2 <= b1 . b2 & b1 . b2 <= k . b2 ) or ex b2 being ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d st
( not G . b2 <= k . b2 & ( b1 . b2 <= k . b2 or G . b2 <= b1 . b2 ) ) )
}
is set

(d,g,f) is non empty functional FinSequence-membered Element of bool (REAL d)
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d : ( for b2 being ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d holds
( g . b2 <= b1 . b2 & b1 . b2 <= f . b2 ) or ex b2 being ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d st
( not g . b2 <= f . b2 & ( b1 . b2 <= f . b2 or g . b2 <= b1 . b2 ) ) )
}
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

A9 . B9 is complex real ext-real Element of REAL

A9 is set

A99 . A 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

Seg d is non empty finite d -element V153() V154() V155() V156() V157() V158() Element of bool NAT

(d,G,k) is non empty functional FinSequence-membered Element of bool (REAL d)
bool (REAL d) is non empty set
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d : ( for b2 being ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d holds
( G . b2 <= b1 . b2 & b1 . b2 <= k . b2 ) or ex b2 being ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d st
( not G . b2 <= k . b2 & ( b1 . b2 <= k . b2 or G . b2 <= b1 . b2 ) ) )
}
is set

(d,f,g) is non empty functional FinSequence-membered Element of bool (REAL d)
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d : ( for b2 being ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d holds
( f . b2 <= b1 . b2 & b1 . b2 <= g . b2 ) or ex b2 being ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d st
( not f . b2 <= g . b2 & ( b1 . b2 <= g . b2 or f . b2 <= b1 . b2 ) ) )
}
is set

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

A99 . A9 is complex real ext-real Element of REAL

A9 . A9 is complex real ext-real Element of REAL

B9 . A9 is complex real ext-real Element of REAL

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

A99 . A9 is complex real ext-real Element of REAL

A9 . A9 is complex real ext-real Element of REAL

B9 . 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

bool (Seg d) is non empty finite V28() set

{ (d,b1,b2) where b1, b2 is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d : ( ex b3 being finite V153() V154() V155() V156() V157() V158() Element of bool (Seg d) st
( card b3 = k & ( for b4 being ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d holds
( ( b4 in b3 & not b2 . b4 <= b1 . b4 & [(b1 . b4),(b2 . b4)] is ((d,G,b4)) ) or ( not b4 in b3 & b1 . b4 = b2 . b4 & b1 . b4 in (d,G,b4) ) ) ) ) or ( k = d & ( for b3 being ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d holds
( not b1 . b3 <= b2 . b3 & [(b1 . b3),(b2 . b3)] is ((d,G,b3)) ) ) ) )
}
is set

bool (REAL d) is non empty set
bool (bool (REAL d)) is non empty set
{ H2(b1,b2) where b1, b2 is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d : S1[b1,b2] } 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)

(d,G,A) is non empty non trivial finite V153() V154() V155() Element of bool REAL

[A9,A99] is non empty non natural Element of
{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,A99] is non empty non natural Element of
{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
[:(Seg d),:] is non empty non trivial Relation-like non finite set
bool [:(Seg d),:] is non empty non trivial non 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

B9 . B9 is complex real ext-real Element of REAL
A . B9 is Element of
(A . B9) `1 is complex real ext-real Element of REAL

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
{(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)
{ b1 where b1 is Relation-like NAT -defined REAL -valued Function-like finite d -element FinSequence-like FinSubsequence-like V143() V144() V145() Element of REAL d : ( for b2 being ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d holds
( B9 . b2 <= b1 . b2 & b1 . b2 <= A9 . b2 ) or ex b2 being ordinal natural complex real finite cardinal V43() ext-real non negative V64() Element of Seg d st
( not B9 . b2 <= A9 . b2 & ( b1 . b2 <= A9 . b2 or B9 . b2 <= b1 . b2 ) ) )
}
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)