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

F

{ F

d is set

G is Element of F

k is Element of F

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

bool F

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

bool F

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

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

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

( G . b

( not G . b

bool (REAL d) is non empty set

{ b

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

( k . b

( not k . b

{ b

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

( G . b

( not G . b

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

( k . b

( not k . b

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

( G . b

( not G . b

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

( G . b

( not G . b

{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

( G . b

( not G . b

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

( f . b

( not f . b

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

( k . b

( not k . b

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

( f . b

( not f . b

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

( G . b

( not G . b

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

( g . b

( not g . b

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

( G . b

( not G . b

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

( f . b

( not f . b

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

( card b

( ( b

( not b

bool (REAL d) is non empty set

bool (bool (REAL d)) is non empty set

{ H

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

( B9 . b

( not B9 . b

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