:: TOPGEN_3 semantic presentation

REAL is non empty non trivial non finite V84() V85() V86() V90() set

NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V84() V85() V86() V87() V88() V89() V90() Element of bool REAL

bool REAL is non empty non trivial non finite set

omega is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V84() V85() V86() V87() V88() V89() V90() set

RAT+ is set

bool RAT+ is non empty set

bool (bool RAT+) is non empty set

DEDEKIND_CUTS is Element of bool (bool RAT+)

REAL+ is set

COMPLEX is non empty non trivial non finite V84() V90() set

bool omega is non empty non trivial non finite set

[:NAT,REAL:] is non empty non trivial V37() V38() V39() non finite set

bool [:NAT,REAL:] is non empty non trivial non finite set

bool (bool REAL) is non empty non trivial non finite set

bool NAT is non empty non trivial non finite set

RAT is non empty non trivial non finite V84() V85() V86() V87() V90() set

INT is non empty non trivial non finite V84() V85() V86() V87() V88() V90() set

{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() real ext-real finite V51() cardinal {} -element integer rational V84() V85() V86() V87() V88() V89() V90() set

the empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() real ext-real finite V51() cardinal {} -element integer rational V84() V85() V86() V87() V88() V89() V90() set is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() real ext-real finite V51() cardinal {} -element integer rational V84() V85() V86() V87() V88() V89() V90() set

1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real ext-real positive finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT

0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() real ext-real finite V51() cardinal {} -element integer rational V84() V85() V86() V87() V88() V89() V90() Element of NAT

2 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real ext-real positive finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT

len omega is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal set

{{}} is non empty trivial finite V51() 1 -element V84() V85() V86() V87() V88() V89() set

[:{{}},REAL+:] is set

REAL+ \/ [:{{}},REAL+:] is set

[{},{}] is set

{{},{}} is non empty finite V51() V84() V85() V86() V87() V88() V89() set

{{{},{}},{{}}} is non empty finite V51() set

{[{},{}]} is non empty trivial finite 1 -element set

(REAL+ \/ [:{{}},REAL+:]) \ {[{},{}]} is Element of bool (REAL+ \/ [:{{}},REAL+:])

bool (REAL+ \/ [:{{}},REAL+:]) is non empty set

[:{{}},RAT+:] is set

RAT+ \/ [:{{}},RAT+:] is set

(RAT+ \/ [:{{}},RAT+:]) \ {[{},{}]} is Element of bool (RAT+ \/ [:{{}},RAT+:])

bool (RAT+ \/ [:{{}},RAT+:]) is non empty set

[:{{}},omega:] is non empty non trivial RAT -valued INT -valued V37() V38() V39() V40() non finite set

omega \/ [:{{}},omega:] is non empty set

(omega \/ [:{{}},omega:]) \ {[{},{}]} is Element of bool (omega \/ [:{{}},omega:])

bool (omega \/ [:{{}},omega:]) is non empty set

omega *` omega is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal set

RAT+ \/ DEDEKIND_CUTS is set

{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() real ext-real finite V51() cardinal {} -element integer rational V84() V85() V86() V87() V88() V89() V90() Element of RAT+

{ { b

(RAT+ \/ DEDEKIND_CUTS) \ { { b

bool (RAT+ \/ DEDEKIND_CUTS) is non empty set

K560({}) is M27( {} )

-infty is non real set

+infty is non real set

BB is set

bool BB is non empty set

bool (bool BB) is non empty set

BB is set

bool BB is non empty set

bool (bool BB) is non empty set

X is Element of bool (bool BB)

union X is Element of bool BB

T is set

a is set

a is Element of bool BB

A1 is Element of bool BB

T is set

a is Element of bool BB

BB is set

bool BB is non empty set

bool (bool BB) is non empty set

X is Element of bool (bool BB)

UniCl X is Element of bool (bool BB)

T is TopStruct

the carrier of T is set

the topology of T is Element of bool (bool the carrier of T)

bool the carrier of T is non empty set

bool (bool the carrier of T) is non empty set

union X is Element of bool BB

a is Element of bool (bool the carrier of T)

union a is Element of bool the carrier of T

UniCl the topology of T is Element of bool (bool the carrier of T)

a is Element of bool the carrier of T

a is Element of bool the carrier of T

a /\ a is Element of bool the carrier of T

{ b

bool BB is non empty Element of bool (bool BB)

A2 is set

a is Element of bool the carrier of T

a is Element of bool (bool the carrier of T)

union a is Element of bool the carrier of T

a is Element of bool (bool the carrier of T)

union a is Element of bool the carrier of T

A2 is Element of bool (bool the carrier of T)

union A2 is Element of bool the carrier of T

bool (a /\ a) is non empty Element of bool (bool (a /\ a))

bool (a /\ a) is non empty set

bool (bool (a /\ a)) is non empty set

B is set

C is Element of bool the carrier of T

union (bool (a /\ a)) is Element of bool (a /\ a)

B is set

C is set

y is set

C /\ y is set

C is Element of bool BB

B is set

C is Element of bool the carrier of T

a is Element of bool (bool the carrier of T)

BB is set

bool BB is non empty Element of bool (bool BB)

bool BB is non empty set

bool (bool BB) is non empty set

bool (bool BB) is non empty Element of bool (bool (bool BB))

bool (bool BB) is non empty set

bool (bool (bool BB)) is non empty set

X is Relation-like non-empty BB -defined Function-like V33(BB) set

rng X is set

Union X is set

union (rng X) is set

union (bool (bool BB)) is Element of bool (bool BB)

dom X is Element of bool BB

T is Element of bool (bool BB)

a is set

A1 is set

a is set

a /\ A1 is set

X . a is set

A2 is set

X . A2 is set

A2 is set

a is set

X . a is set

a is set

a /\ A2 is set

a is set

B is Element of bool BB

UniCl T is Element of bool (bool BB)

a is TopStruct

the carrier of a is set

the topology of a is Element of bool (bool the carrier of a)

bool the carrier of a is non empty set

bool (bool the carrier of a) is non empty set

a is set

X . a is set

the Element of X . a is Element of X . a

a is non empty TopSpace-like TopStruct

the carrier of a is non empty set

A1 is non empty Relation-like the carrier of a -defined Function-like V33( the carrier of a) set

A2 is Element of the carrier of a

A1 . A2 is set

bool the carrier of a is non empty set

bool (bool the carrier of a) is non empty set

a is Element of bool (bool the carrier of a)

the topology of a is non empty Element of bool (bool the carrier of a)

a is set

Intersect a is Element of bool the carrier of a

a is Element of bool the carrier of a

B is Element of bool (bool the carrier of a)

union B is Element of bool the carrier of a

C is set

X . A2 is set

y is set

X . y is set

y is set

BB is set

bool BB is non empty set

bool (bool BB) is non empty set

X is Element of bool (bool BB)

COMPLEMENT X is Element of bool (bool BB)

a is TopStruct

the carrier of a is set

the topology of a is Element of bool (bool the carrier of a)

bool the carrier of a is non empty set

bool (bool the carrier of a) is non empty set

{} a is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() real ext-real finite V51() cardinal {} -element integer rational V84() V85() V86() V87() V88() V89() V90() boundary Element of bool the carrier of a

({} a) ` is Element of bool the carrier of a

the carrier of a \ ({} a) is set

a is Element of bool (bool the carrier of a)

COMPLEMENT a is Element of bool (bool the carrier of a)

Intersect (COMPLEMENT a) is Element of bool the carrier of a

union a is Element of bool the carrier of a

(union a) ` is Element of bool the carrier of a

the carrier of a \ (union a) is set

a is Element of bool the carrier of a

A1 is Element of bool the carrier of a

a /\ A1 is Element of bool the carrier of a

A1 ` is Element of bool the carrier of a

the carrier of a \ A1 is set

a ` is Element of bool the carrier of a

the carrier of a \ a is set

(a `) \/ (A1 `) is Element of bool the carrier of a

(a /\ A1) ` is Element of bool the carrier of a

the carrier of a \ (a /\ A1) is set

a is Element of bool the carrier of a

a ` is Element of bool the carrier of a

the carrier of a \ a is set

F

bool F

bool (bool F

{ b

bool F

T is set

a is Element of bool F

T is Element of bool (bool F

COMPLEMENT T is Element of bool (bool F

TopStruct(# F

a is set

A1 is set

a \/ A1 is set

A2 is Element of bool F

a is Element of bool F

A2 \/ a is Element of bool F

a is Element of bool (bool F

Intersect a is Element of bool F

A1 is set

A2 is Element of bool F

a is strict TopSpace-like TopStruct

the carrier of a is set

bool the carrier of a is non empty set

A1 is Element of bool the carrier of a

A2 is Element of bool F

A2 is Element of bool F

BB is TopSpace-like TopStruct

the carrier of BB is set

bool the carrier of BB is non empty set

X is TopSpace-like TopStruct

the carrier of X is set

bool the carrier of X is non empty set

the topology of BB is non empty Element of bool (bool the carrier of BB)

bool (bool the carrier of BB) is non empty set

the topology of X is non empty Element of bool (bool the carrier of X)

bool (bool the carrier of X) is non empty set

[#] X is non proper open closed dense Element of bool the carrier of X

[#] BB is non proper open closed dense Element of bool the carrier of BB

T is set

a is Element of bool the carrier of BB

a is Element of bool the carrier of X

BB is TopSpace-like TopStruct

the carrier of BB is set

bool the carrier of BB is non empty set

X is TopSpace-like TopStruct

the carrier of X is set

bool the carrier of X is non empty set

the topology of BB is non empty Element of bool (bool the carrier of BB)

bool (bool the carrier of BB) is non empty set

TopStruct(# the carrier of BB, the topology of BB #) is strict TopSpace-like TopStruct

the topology of X is non empty Element of bool (bool the carrier of X)

bool (bool the carrier of X) is non empty set

TopStruct(# the carrier of X, the topology of X #) is strict TopSpace-like TopStruct

BB is TopSpace-like TopStruct

the carrier of BB is set

bool the carrier of BB is non empty set

X is TopSpace-like TopStruct

the carrier of X is set

bool the carrier of X is non empty set

the topology of BB is non empty Element of bool (bool the carrier of BB)

bool (bool the carrier of BB) is non empty set

the topology of X is non empty Element of bool (bool the carrier of X)

bool (bool the carrier of X) is non empty set

[#] X is non proper open closed dense Element of bool the carrier of X

[#] BB is non proper open closed dense Element of bool the carrier of BB

T is set

a is Element of bool the carrier of BB

a is Element of bool the carrier of X

a ` is Element of bool the carrier of X

the carrier of X \ a is set

BB is TopSpace-like TopStruct

the carrier of BB is set

bool the carrier of BB is non empty set

X is TopSpace-like TopStruct

the carrier of X is set

bool the carrier of X is non empty set

the topology of BB is non empty Element of bool (bool the carrier of BB)

bool (bool the carrier of BB) is non empty set

TopStruct(# the carrier of BB, the topology of BB #) is strict TopSpace-like TopStruct

the topology of X is non empty Element of bool (bool the carrier of X)

bool (bool the carrier of X) is non empty set

TopStruct(# the carrier of X, the topology of X #) is strict TopSpace-like TopStruct

BB is set

X is set

bool X is non empty Element of bool (bool X)

bool X is non empty set

bool (bool X) is non empty set

[:BB,(bool X):] is set

bool [:BB,(bool X):] is non empty set

T is Relation-like BB -defined bool X -valued Element of bool [:BB,(bool X):]

rng T is set

BB is set

bool BB is non empty Element of bool (bool BB)

bool BB is non empty set

bool (bool BB) is non empty set

[:(bool BB),(bool BB):] is non empty set

bool [:(bool BB),(bool BB):] is non empty set

X is non empty Relation-like bool BB -defined bool BB -valued Function-like V33( bool BB) V34( bool BB, bool BB) Element of bool [:(bool BB),(bool BB):]

X . {} is set

((bool BB),BB,X) is Element of bool (bool BB)

COMPLEMENT ((bool BB),BB,X) is Element of bool (bool BB)

dom X is Element of bool (bool BB)

bool (bool BB) is non empty set

a is set

a is set

A1 is set

X . A1 is set

A2 is set

X . A2 is set

a \/ a is set

X . a is set

(X . a) \/ a is set

X . a is set

(X . a) \/ (X . a) is set

a is Element of bool BB

X . a is Element of bool BB

a is Element of bool BB

X . a is Element of bool BB

(X . a) \/ (X . a) is Element of bool BB

X . ((X . a) \/ (X . a)) is Element of bool BB

a is Element of bool BB

a is Element of bool BB

a \/ a is Element of bool BB

X . a is Element of bool BB

X . a is Element of bool BB

(X . a) \/ (X . a) is Element of bool BB

a is Element of bool (bool BB)

a is set

Intersect a is Element of bool BB

X . (Intersect a) is Element of bool BB

A1 is Element of bool BB

X . A1 is Element of bool BB

A2 is set

X . A2 is set

a is TopStruct

the carrier of a is set

the topology of a is Element of bool (bool the carrier of a)

bool the carrier of a is non empty set

bool (bool the carrier of a) is non empty set

{} BB is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() real ext-real finite V51() cardinal {} -element integer rational V84() V85() V86() V87() V88() V89() V90() Element of bool BB

a is Element of bool the carrier of a

Cl a is Element of bool the carrier of a

X . a is set

A1 is Element of bool BB

X . A1 is Element of bool BB

a is Element of bool the carrier of a

A2 is Element of bool BB

X . A2 is Element of bool BB

a is set

X . a is set

F

F

bool F

bool F

bool (bool F

X is Relation-like Function-like set

dom X is set

T is set

F

X . T is set

[:(bool F

bool [:(bool F

T is non empty Relation-like bool F

a is Element of bool F

T . a is Element of bool F

F

a is Element of bool F

a is Element of bool F

a \/ a is Element of bool F

T . (a \/ a) is Element of bool F

T . a is Element of bool F

T . a is Element of bool F

(T . a) \/ (T . a) is Element of bool F

F

F

F

a is Element of bool F

T . a is Element of bool F

T . (T . a) is Element of bool F

F

F

T . {} is set

((bool F

COMPLEMENT ((bool F

TopStruct(# F

a is strict TopSpace-like TopStruct

the carrier of a is set

bool the carrier of a is non empty set

a is Element of bool the carrier of a

Cl a is closed Element of bool the carrier of a

F

T . a is set

BB is TopSpace-like TopStruct

the carrier of BB is set

X is TopSpace-like TopStruct

the carrier of X is set

bool the carrier of BB is non empty set

bool the carrier of X is non empty set

the topology of BB is non empty Element of bool (bool the carrier of BB)

bool (bool the carrier of BB) is non empty set

the topology of X is non empty Element of bool (bool the carrier of X)

bool (bool the carrier of X) is non empty set

T is set

a is closed Element of bool the carrier of BB

Cl a is closed Element of bool the carrier of BB

a is Element of bool the carrier of X

Cl a is closed Element of bool the carrier of X

a is closed Element of bool the carrier of X

Cl a is closed Element of bool the carrier of X

a is Element of bool the carrier of BB

Cl a is closed Element of bool the carrier of BB

TopStruct(# the carrier of BB, the topology of BB #) is strict TopSpace-like TopStruct

TopStruct(# the carrier of X, the topology of X #) is strict TopSpace-like TopStruct

BB is set

bool BB is non empty Element of bool (bool BB)

bool BB is non empty set

bool (bool BB) is non empty set

[:(bool BB),(bool BB):] is non empty set

bool [:(bool BB),(bool BB):] is non empty set

X is non empty Relation-like bool BB -defined bool BB -valued Function-like V33( bool BB) V34( bool BB, bool BB) Element of bool [:(bool BB),(bool BB):]

X . BB is set

((bool BB),BB,X) is Element of bool (bool BB)

a is TopStruct

the carrier of a is set

the topology of a is Element of bool (bool the carrier of a)

bool the carrier of a is non empty set

bool (bool the carrier of a) is non empty set

dom X is Element of bool (bool BB)

bool (bool BB) is non empty set

a is Element of bool the carrier of a

A1 is Element of bool the carrier of a

A2 is set

X . A2 is set

a is set

X . a is set

a /\ A1 is Element of bool the carrier of a

X . a is set

(X . a) /\ A1 is Element of bool the carrier of a

X . A1 is set

(X . a) /\ (X . A1) is set

a is Element of bool BB

X . a is Element of bool BB

B is Element of bool BB

X . B is Element of bool BB

(X . a) /\ (X . B) is Element of bool BB

X . ((X . a) /\ (X . B)) is Element of bool BB

a is Element of bool BB

A1 is Element of bool BB

a /\ A1 is Element of bool BB

X . a is Element of bool BB

X . A1 is Element of bool BB

(X . a) /\ (X . A1) is Element of bool BB

a is Element of bool (bool BB)

A1 is set

A2 is Element of bool BB

X . A2 is Element of bool BB

union a is Element of bool BB

X . (union a) is Element of bool BB

a is set

X . a is set

[#] BB is non proper Element of bool BB

a is Element of bool the carrier of a

Int a is Element of bool the carrier of a

X . a is set

A2 is Element of bool BB

X . A2 is Element of bool BB

a is set

X . a is set

A1 is Element of bool BB

X . A1 is Element of bool BB

a is Element of bool the carrier of a

F

F

bool F

bool F

bool (bool F

X is Relation-like Function-like set

dom X is set

T is set

F

X . T is set

[:(bool F

bool [:(bool F

T is non empty Relation-like bool F

a is Element of bool F

T . a is Element of bool F

F

a is Element of bool F

a is Element of bool F

a /\ a is Element of bool F

T . (a /\ a) is Element of bool F

T . a is Element of bool F

T . a is Element of bool F

(T . a) /\ (T . a) is Element of bool F

F

F

F

a is Element of bool F

T . a is Element of bool F

T . (T . a) is Element of bool F

F

F

T . F

((bool F

TopStruct(# F

a is strict TopSpace-like TopStruct

the carrier of a is set

bool the carrier of a is non empty set

a is Element of bool the carrier of a

Int a is open Element of bool the carrier of a

F

T . a is set

BB is TopSpace-like TopStruct

the carrier of BB is set

X is TopSpace-like TopStruct

the carrier of X is set

bool the carrier of BB is non empty set

bool the carrier of X is non empty set

the topology of BB is non empty Element of bool (bool the carrier of BB)

bool (bool the carrier of BB) is non empty set

the topology of X is non empty Element of bool (bool the carrier of X)

bool (bool the carrier of X) is non empty set

T is Element of bool the carrier of BB

a is Element of bool the carrier of X

T ` is Element of bool the carrier of BB

the carrier of BB \ T is set

Int (T `) is open Element of bool the carrier of BB

a ` is Element of bool the carrier of X

the carrier of X \ a is set

Int (a `) is open Element of bool the carrier of X

Cl T is closed Element of bool the carrier of BB

(Int (a `)) ` is closed Element of bool the carrier of X

the carrier of X \ (Int (a `)) is set

Cl a is closed Element of bool the carrier of X

{ [.b

BB is non empty strict TopSpace-like TopStruct

the carrier of BB is non empty set

the topology of BB is non empty Element of bool (bool the carrier of BB)

bool the carrier of BB is non empty set

bool (bool the carrier of BB) is non empty set

T is Element of bool (bool REAL)

UniCl T is Element of bool (bool REAL)

X is non empty strict TopSpace-like TopStruct

the carrier of X is non empty set

the topology of X is non empty Element of bool (bool the carrier of X)

bool the carrier of X is non empty set

bool (bool the carrier of X) is non empty set

a is Element of bool (bool REAL)

UniCl a is Element of bool (bool REAL)

bool REAL is non empty non trivial non finite Element of bool (bool REAL)

X is set

T is V28() real ext-real Element of REAL

a is V28() real ext-real Element of REAL

[.T,a.[ is V84() V85() V86() Element of bool REAL

X is Element of bool (bool REAL)

a is set

a is set

T is set

a /\ a is set

A1 is V28() real ext-real Element of REAL

A2 is V28() real ext-real Element of REAL

[.A1,A2.[ is V84() V85() V86() Element of bool REAL

a is V28() real ext-real Element of REAL

a is V28() real ext-real Element of REAL

[.a,a.[ is V84() V85() V86() Element of bool REAL

max (A1,a) is V28() real ext-real Element of REAL

min (A2,a) is V28() real ext-real Element of REAL

y is V28() real ext-real Element of REAL

[.(max (A1,a)),(min (A2,a)).[ is V84() V85() V86() Element of bool REAL

T is set

a is V28() real ext-real Element of REAL

a + 1 is V28() real ext-real set

a + 0 is V28() real ext-real set

a is V28() real ext-real rational set

[.a,a.[ is V84() V85() V86() Element of bool REAL

A1 is V84() V85() V86() Element of bool REAL

UniCl X is Element of bool (bool REAL)

TopStruct(# REAL,(UniCl X) #) is non empty strict TopStruct

() is non empty strict TopSpace-like TopStruct

the carrier of () is non empty set

the topology of () is non empty Element of bool (bool the carrier of ())

bool the carrier of () is non empty set

bool (bool the carrier of ()) is non empty set

BB is Element of bool (bool REAL)

UniCl BB is Element of bool (bool REAL)

X is V28() real ext-real set

T is V28() real ext-real set

[.X,T.[ is V84() V85() V86() Element of bool REAL

a is Element of the carrier of ()

A1 is V28() real ext-real Element of REAL

A2 is V28() real ext-real rational set

[.X,A2.[ is V84() V85() V86() Element of bool REAL

a is Element of bool the carrier of ()

a is Element of bool the carrier of ()

a is Element of bool the carrier of ()

X is V28() real ext-real set

T is V28() real ext-real set

].X,T.[ is V84() V85() V86() Element of bool REAL

a is Element of the carrier of ()

a is Element of bool the carrier of ()

A1 is V28() real ext-real Element of REAL

A2 is V28() real ext-real rational set

[.A1,A2.[ is V84() V85() V86() Element of bool REAL

a is Element of bool the carrier of ()

a is Element of bool the carrier of ()

X is V28() real ext-real set

left_open_halfline X is V84() V85() V86() Element of bool REAL

K236(-infty,X) is set

a is Element of the carrier of ()

T is Element of bool the carrier of ()

a is V28() real ext-real Element of REAL

{a} is non empty trivial proper finite 1 -element V84() V85() V86() Element of bool REAL

A1 is V28() real ext-real rational set

[.a,A1.[ is V84() V85() V86() Element of bool REAL

A2 is Element of bool the carrier of ()

a is Element of bool the carrier of ()

].a,A1.[ is V84() V85() V86() Element of bool REAL

{a} \/ ].a,A1.[ is non empty V84() V85() V86() Element of bool REAL

X is V28() real ext-real set

right_open_halfline X is V84() V85() V86() Element of bool REAL

K236(X,+infty) is set

a is Element of the carrier of ()

T is Element of bool the carrier of ()

a is V28() real ext-real Element of REAL

{a} is non empty trivial proper finite 1 -element V84() V85() V86() Element of bool REAL

a + 1 is V28() real ext-real set

a + 0 is V28() real ext-real set

A1 is V28() real ext-real rational set

[.a,A1.[ is V84() V85() V86() Element of bool REAL

A2 is Element of bool the carrier of ()

a is Element of bool the carrier of ()

].a,A1.[ is V84() V85() V86() Element of bool REAL

{a} \/ ].a,A1.[ is non empty V84() V85() V86() Element of bool REAL

X is V28() real ext-real set

right_closed_halfline X is V84() V85() V86() Element of bool REAL

K234(X,+infty) is set

a is Element of the carrier of ()

a is V28() real ext-real Element of REAL

a + 1 is V28() real ext-real set

a + 0 is V28() real ext-real set

A1 is V28() real ext-real rational set

[.a,A1.] is V84() V85() V86() Element of bool REAL

{a} is non empty trivial proper finite 1 -element V84() V85() V86() Element of bool REAL

[.a,A1.[ is V84() V85() V86() Element of bool REAL

T is Element of bool the carrier of ()

A2 is Element of bool the carrier of ()

a is Element of bool the carrier of ()

].a,A1.[ is V84() V85() V86() Element of bool REAL

{a} \/ ].a,A1.[ is non empty V84() V85() V86() Element of bool REAL

len INT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal set

{0} is non empty trivial proper finite V51() 1 -element V84() V85() V86() V87() V88() V89() Element of bool NAT

[:{0},NAT:] is non empty non trivial RAT -valued INT -valued V37() V38() V39() V40() non finite set

NAT \/ [:{0},NAT:] is non empty set

len (NAT \/ [:{0},NAT:]) is non empty epsilon-transitive epsilon-connected ordinal cardinal set

[:NAT,{0}:] is non empty non trivial RAT -valued INT -valued V37() V38() V39() V40() non finite set

len [:NAT,{0}:] is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal set

len [:{0},NAT:] is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal set

len NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal set

omega +` omega is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal set

len RAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal set

[:INT,NAT:] is non empty non trivial RAT -valued INT -valued V37() V38() V39() V40() non finite set

X is set

T is set

a is set

[T,a] is set

{T,a} is non empty finite set

{T} is non empty trivial finite 1 -element set

{{T,a},{T}} is non empty finite V51() set

A1 is V28() real ext-real integer rational set

a is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational set

A1 / a is V28() real ext-real rational Element of COMPLEX

X is Relation-like Function-like set

dom X is set

rng X is set

T is set

a is V28() real ext-real integer rational set

a is V28() real ext-real integer rational set

a / a is V28() real ext-real rational Element of COMPLEX

A1 is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT

- A1 is V28() real ext-real integer rational set

a / (- A1) is V28() real ext-real rational Element of COMPLEX

a / A1 is V28() real ext-real rational Element of COMPLEX

- (a / A1) is V28() real ext-real rational Element of COMPLEX

- a is V28() real ext-real integer rational set

(- a) / A1 is V28() real ext-real rational Element of COMPLEX

A2 is V28() real ext-real integer rational set

A2 / A1 is V28() real ext-real rational Element of COMPLEX

[A2,A1] is set

{A2,A1} is non empty finite V84() V85() V86() V87() V88() set

{A2} is non empty trivial finite 1 -element V84() V85() V86() V87() V88() set

{{A2,A1},{A2}} is non empty finite V51() set

X . [A2,A1] is set

a is V28() real ext-real integer rational set

a is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational set

[a,a] is set

{a,a} is non empty finite V84() V85() V86() V87() V88() set

{a} is non empty trivial finite 1 -element V84() V85() V86() V87() V88() set

{{a,a},{a}} is non empty finite V51() set

a / a is V28() real ext-real rational Element of COMPLEX

len [:INT,NAT:] is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal set

[:omega,omega:] is non empty non trivial RAT -valued INT -valued V37() V38() V39() V40() non finite set

len [:omega,omega:] is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal set

X is set

T is set

a is V28() real ext-real set

a is V28() real ext-real set

].a,a.[ is V84() V85() V86() Element of bool REAL

A1 is V28() real ext-real rational set

T is Relation-like Function-like set

dom T is set

rng T is set

a is set

T . a is set

a is set

T . a is set

len X is epsilon-transitive epsilon-connected ordinal cardinal set

X is V84() V85() V86() Element of bool REAL

{ b

a is set

a is V28() real ext-real Element of REAL

bool REAL is non empty non trivial non finite Element of bool (bool REAL)

A1 is V28() real ext-real set

].A1,a.[ is V84() V85() V86() Element of bool REAL

a is Relation-like Function-like set

dom a is set

rng a is set

a is set

A1 is set

a . a is set

a . A1 is set

a is V28() real ext-real set

B is V28() real ext-real set

].B,a.[ is V84() V85() V86() Element of bool REAL

C is V28() real ext-real Element of REAL

C is V28() real ext-real set

y is V28() real ext-real set

].y,C.[ is V84() V85() V86() Element of bool REAL

C is V28() real ext-real rational set

b is V28() real ext-real Element of REAL

len { b

len (rng a) is epsilon-transitive epsilon-connected ordinal cardinal set

a is set

A1 is set

A2 is set

a . A2 is set

a is V28() real ext-real set

a is V28() real ext-real set

].a,a.[ is V84() V85() V86() Element of bool REAL

B is V28() real ext-real Element of REAL

B is set

a . B is set

C is V28() real ext-real set

y is V28() real ext-real set

].y,C.[ is V84() V85() V86() Element of bool REAL

C is set

b is V28() real ext-real Element of REAL

c

a is set

A1 is set

a . A1 is set

A2 is V28() real ext-real set

a is V28() real ext-real set

].a,A2.[ is V84() V85() V86() Element of bool REAL

B is V28() real ext-real set

a is V28() real ext-real set

].a,B.[ is V84() V85() V86() Element of bool REAL

X is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal set

exp (2,X) is epsilon-transitive epsilon-connected ordinal cardinal set

len X is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal set

bool X is non empty non trivial non finite Element of bool (bool X)

bool X is non empty non trivial non finite set

bool (bool X) is non empty non trivial non finite set

len (bool X) is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal set

len REAL is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal set

() is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal set

len { [.b

[:REAL,RAT:] is non empty non trivial RAT -valued V37() V38() V39() non finite set

T is Relation-like Function-like set

dom T is set

rng T is set

a is set

a is V28() real ext-real Element of REAL

A1 is V28() real ext-real Element of REAL

[.a,A1.[ is V84() V85() V86() Element of bool REAL

[a,A1] is Element of [:REAL,REAL:]

[:REAL,REAL:] is non empty non trivial V37() V38() V39() non finite set

{a,A1} is non empty finite V84() V85() V86() set

{a} is non empty trivial finite 1 -element V84() V85() V86() set

{{a,A1},{a}} is non empty finite V51() set

A2 is Element of [:REAL,RAT:]

A2 `2 is V28() real ext-real rational Element of RAT

A2 `1 is V28() real ext-real Element of REAL

T . A2 is set

len [:REAL,RAT:] is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal set

[:(len REAL),(len RAT):] is non empty non trivial non finite set

len [:(len REAL),(len RAT):] is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal set

() *` omega is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal set

a is set

a is V28() real ext-real Element of REAL

a + 1 is V28() real ext-real set

a + 0 is V28() real ext-real set

A1 is V28() real ext-real rational set

A2 is V28() real ext-real Element of REAL

[.a,A2.[ is V84() V85() V86() Element of bool REAL

a is Relation-like Function-like set

dom a is set

rng a is set

a is set

a . a is set

A1 is set

a . A1 is set

A2 is V28() real ext-real Element of REAL

a is V28() real ext-real Element of REAL

[.A2,a.[ is V84() V85() V86() Element of bool REAL

a is V28() real ext-real Element of REAL

B is V28() real ext-real Element of REAL

[.a,B.[ is V84() V85() V86() Element of bool REAL

X is set

T is V28() real ext-real set

a is set

In (a,NAT) is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT

T |^ (In (a,NAT)) is V28() real ext-real set

a is non empty Relation-like NAT -defined REAL -valued Function-like V33( NAT ) V34( NAT , REAL ) V37() V38() V39() Element of bool [:NAT,REAL:]

a is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational set

a . a is V28() real ext-real Element of REAL

T |^ a is V28() real ext-real set

In (a,NAT) is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT

a is non empty Relation-like NAT -defined REAL -valued Function-like V33( NAT ) V34( NAT , REAL ) V37() V38() V39() Element of bool [:NAT,REAL:]

a is non empty Relation-like NAT -defined REAL -valued Function-like V33( NAT ) V34( NAT , REAL ) V37() V38() V39() Element of bool [:NAT,REAL:]

A1 is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT

a . A1 is V28() real ext-real Element of REAL

T |^ A1 is V28() real ext-real set

a . A1 is V28() real ext-real Element of REAL

X is set

T is V28() real ext-real set

(X,T) is non empty Relation-like NAT -defined REAL -valued Function-like V33( NAT ) V34( NAT , REAL ) V37() V38() V39() Element of bool [:NAT,REAL:]

a is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT

(X,T) . a is V28() real ext-real Element of REAL

T |^ a is V28() real ext-real set

a is non empty epsilon-transitive epsilon-connected ordinal natural V28() real ext-real positive finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT

a is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT

T GeoSeq is non empty Relation-like NAT -defined REAL -valued Function-like V33( NAT ) V34( NAT , REAL ) V37() V38() V39() Element of bool [:NAT,REAL:]

(T GeoSeq) . a is V28() real ext-real Element of REAL

T |^ a is V28() real ext-real set

(X,T) . a is V28() real ext-real Element of REAL

abs T is V28() real ext-real Element of REAL

a is non empty epsilon-transitive epsilon-connected ordinal natural V28() real ext-real positive finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT

X is V28() real ext-real set

X GeoSeq is non empty Relation-like NAT -defined REAL -valued Function-like V33( NAT ) V34( NAT , REAL ) V37() V38() V39() Element of bool [:NAT,REAL:]

1 - X is V28() real ext-real set

T is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT

(X GeoSeq) ^\ T is non empty Relation-like NAT -defined REAL -valued Function-like V33( NAT ) V34( NAT , REAL ) V37() V38() V39() Element of bool [:NAT,REAL:]

Sum ((X GeoSeq) ^\ T) is V28() real ext-real Element of REAL

X |^ T is V28() real ext-real set

(X |^ T) / (1 - X) is V28() real ext-real Element of COMPLEX

abs X is V28() real ext-real Element of REAL

(X |^ T) (#) (X GeoSeq) is non empty Relation-like NAT -defined REAL -valued Function-like V33( NAT ) V34( NAT , REAL ) V37() V38() V39() Element of bool [:NAT,REAL:]

dom ((X |^ T) (#) (X GeoSeq)) is V84() V85() V86() V87() V88() V89() Element of bool NAT

a is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT

((X GeoSeq) ^\ T) . a is V28() real ext-real Element of REAL

a + T is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT

(X GeoSeq) . (a + T) is V28() real ext-real Element of REAL

X |^ (a + T) is V28() real ext-real set

X |^ a is V28() real ext-real set

(X |^ T) * (X |^ a) is V28() real ext-real set

(X GeoSeq) . a is V28() real ext-real Element of REAL

(X |^ T) * ((X GeoSeq) . a) is V28() real ext-real set

((X |^ T) (#) (X GeoSeq)) . a is V28() real ext-real Element of REAL

Sum (X GeoSeq) is V28() real ext-real Element of REAL

1 / (1 - X) is V28() real ext-real Element of COMPLEX

(X |^ T) * (1 / (1 - X)) is V28() real ext-real set

(X |^ T) * 1 is V28() real ext-real set

((X |^ T) * 1) / (1 - X) is V28() real ext-real Element of COMPLEX

1 / 2 is V28() real ext-real rational Element of COMPLEX

(1 / 2) GeoSeq is non empty Relation-like NAT -defined REAL -valued Function-like V33( NAT ) V34( NAT , REAL ) V37() V38() V39() Element of bool [:NAT,REAL:]

X is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT

X + 1 is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT

((1 / 2) GeoSeq) ^\ (X + 1) is non empty Relation-like NAT -defined REAL -valued Function-like V33( NAT ) V34( NAT , REAL ) V37() V38() V39() Element of bool [:NAT,REAL:]

Sum (((1 / 2) GeoSeq) ^\ (X + 1)) is V28() real ext-real Element of REAL

(1 / 2) |^ X is V28() real ext-real set

(1 / 2) |^ (X + 1) is V28() real ext-real set

1 - (1 / 2) is V28() real ext-real rational set

((1 / 2) |^ (X + 1)) / (1 - (1 / 2)) is V28() real ext-real Element of COMPLEX

((1 / 2) |^ X) * (1 / 2) is V28() real ext-real set

(((1 / 2) |^ X) * (1 / 2)) / (1 / 2) is V28() real ext-real Element of COMPLEX

X is V28() real ext-real set

X GeoSeq is non empty Relation-like NAT -defined REAL -valued Function-like V33( NAT ) V34( NAT , REAL ) V37() V38() V39() Element of bool [:NAT,REAL:]

Sum (X GeoSeq) is V28() real ext-real Element of REAL

T is set

(T,X) is non empty Relation-like NAT -defined REAL -valued Function-like V33( NAT ) V34( NAT , REAL ) V37() V38() V39() Element of bool [:NAT,REAL:]

Sum (T,X) is V28() real ext-real Element of REAL

a is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT

(T,X) . a is V28() real ext-real Element of REAL

X |^ a is V28() real ext-real set

(X GeoSeq) . a is V28() real ext-real Element of REAL

abs X is V28() real ext-real Element of REAL

X is set

(X,(1 / 2)) is non empty Relation-like NAT -defined REAL -valued Function-like V33( NAT ) V34( NAT , REAL ) V37() V38() V39() Element of bool [:NAT,REAL:]

T is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT

T + 1 is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT

(X,(1 / 2)) ^\ (T + 1) is non empty Relation-like NAT -defined REAL -valued Function-like V33( NAT ) V34( NAT , REAL ) V37() V38() V39() Element of bool [:NAT,REAL:]

Sum ((X,(1 / 2)) ^\ (T + 1)) is V28() real ext-real Element of REAL

(1 / 2) |^ T is V28() real ext-real set

abs (1 / 2) is V28() real ext-real rational Element of REAL

((1 / 2) GeoSeq) ^\ (T + 1) is non empty Relation-like NAT -defined REAL -valued Function-like V33( NAT ) V34( NAT , REAL ) V37() V38() V39() Element of bool [:NAT,REAL:]

a is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT

((X,(1 / 2)) ^\ (T + 1)) . a is V28() real ext-real Element of REAL

a + (T + 1) is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT

(X,(1 / 2)) . (a + (T + 1)) is V28() real ext-real Element of REAL

(1 / 2) |^ (a + (T + 1)) is V28() real ext-real set

((1 / 2) GeoSeq) . (a + (T + 1)) is V28() real ext-real Element of REAL

(((1 / 2) GeoSeq) ^\ (T + 1)) . a is V28() real ext-real Element of REAL

Sum (((1 / 2) GeoSeq) ^\ (T + 1)) is V28() real ext-real Element of REAL

T is non empty non trivial non finite V84() V85() V86() V87() V88() V89() Element of bool NAT

(T,(1 / 2)) is non empty Relation-like NAT -defined REAL -valued Function-like V33( NAT ) V34( NAT , REAL ) V37() V38() V39() Element of bool [:NAT,REAL:]

Sum (T,(1 / 2)) is V28() real ext-real Element of REAL

Partial_Sums (T,(1 / 2)) is non empty Relation-like NAT -defined REAL -valued Function-like V33( NAT ) V34( NAT , REAL ) V37() V38() V39() Element of bool [:NAT,REAL:]

a is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational set

(Partial_Sums (T,(1 / 2))) . a is V28() real ext-real Element of REAL

a + 1 is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT

a is set

A1 is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT

(T,(1 / 2)) . A1 is V28() real ext-real Element of REAL

(1 / 2) |^ A1 is V28() real ext-real set

a is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT

(T,(1 / 2)) . a is V28() real ext-real Element of REAL

(1 / 2) |^ a is V28() real ext-real set

a is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT

a + a is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT

(Partial_Sums (T,(1 / 2))) . (a + a) is V28() real ext-real Element of REAL

a + 1 is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT

a + (a + 1) is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT

(a + a) + 1 is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT

A2 is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT

A2 + (a + 1) is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT

(Partial_Sums (T,(1 / 2))) . (A2 + (a + 1)) is V28() real ext-real Element of REAL

A2 + a is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT

(Partial_Sums (T,(1 / 2))) . (A2 + a) is V28() real ext-real Element of REAL

(T,(1 / 2)) . (A2 + (a + 1)) is V28() real ext-real Element of REAL

((Partial_Sums (T,(1 / 2))) . (A2 + a)) + ((T,(1 / 2)) . (A2 + (a + 1))) is V28() real ext-real set

((Partial_Sums (T,(1 / 2))) . (A2 + a)) + 0 is V28() real ext-real set

(Partial_Sums (T,(1 / 2))) . (a + (a + 1)) is V28() real ext-real Element of REAL

A2 + 1 is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT

a is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational set

(A2 + 1) + a is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT

((Partial_Sums (T,(1 / 2))) . a) + ((1 / 2) |^ A1) is V28() real ext-real set

((Partial_Sums (T,(1 / 2))) . a) + 0 is V28() real ext-real set

a + 0 is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT

(Partial_Sums (T,(1 / 2))) . (a + 0) is V28() real ext-real Element of REAL

a is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT

a + a is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT

(Partial_Sums (T,(1 / 2))) . (a + a) is V28() real ext-real Element of REAL

a + 1 is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT

A2 + (a + 1) is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT

A2 + a is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT

(A2 + a) + 1 is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT

(Partial_Sums (T,(1 / 2))) . A1 is V28() real ext-real Element of REAL

(Partial_Sums (T,(1 / 2))) . (A2 + a) is V28() real ext-real Element of REAL

((Partial_Sums (T,(1 / 2))) . (A2 + a)) + ((1 / 2) |^ A1) is V28() real ext-real set

T is non empty non trivial non finite V84() V85() V86() V87() V88() V89() Element of bool NAT

(T,(1 / 2)) is non empty Relation-like NAT -defined REAL -valued Function-like V33( NAT ) V34( NAT , REAL ) V37() V38() V39() Element of bool [:NAT,REAL:]

Sum (T,(1 / 2)) is V28() real ext-real Element of REAL

a is non empty non trivial non finite V84() V85() V86() V87() V88() V89() Element of bool NAT

(a,(1 / 2)) is non empty Relation-like NAT -defined REAL -valued Function-like V33( NAT ) V34( NAT , REAL ) V37() V38() V39() Element of bool [:NAT,REAL:]

Sum (a,(1 / 2)) is V28() real ext-real Element of REAL

a is set

A1 is set

a is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational set

A1 is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT

A2 is non empty non trivial non finite V84() V85() V86() V87() V88() V89() Element of bool NAT

a is non empty non trivial non finite V84() V85() V86() V87() V88() V89() Element of bool NAT

(A2,(1 / 2)) is non empty Relation-like NAT -defined REAL -valued Function-like V33( NAT ) V34( NAT , REAL ) V37() V38() V39() Element of bool [:NAT,REAL:]

(A2,(1 / 2)) . A1 is V28() real ext-real Element of REAL

(1 / 2) |^ A1 is V28() real ext-real set

Partial_Sums (A2,(1 / 2)) is non empty Relation-like NAT -defined REAL -valued Function-like V33( NAT ) V34( NAT , REAL ) V37() V38() V39() Element of bool [:NAT,REAL:]

(a,(1 / 2)) is non empty Relation-like NAT -defined REAL -valued Function-like V33( NAT ) V34( NAT , REAL ) V37() V38() V39() Element of bool [:NAT,REAL:]

Partial_Sums (a,(1 / 2)) is non empty Relation-like NAT -defined REAL -valued Function-like V33( NAT ) V34( NAT , REAL ) V37() V38() V39() Element of bool [:NAT,REAL:]

a is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT

(Partial_Sums (A2,(1 / 2))) . a is V28() real ext-real Element of REAL

(Partial_Sums (a,(1 / 2))) . a is V28() real ext-real Element of REAL

a + 1 is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT

(Partial_Sums (A2,(1 / 2))) . (a + 1) is V28() real ext-real Element of REAL

(Partial_Sums (a,(1 / 2))) . (a + 1) is V28() real ext-real Element of REAL

(a,(1 / 2)) . (a + 1) is V28() real ext-real Element of REAL

(1 / 2) |^ (a + 1) is V28() real ext-real set

(A2,(1 / 2)) . (a + 1) is V28() real ext-real Element of REAL

((Partial_Sums (a,(1 / 2))) . a) + ((A2,(1 / 2)) . (a + 1)) is V28() real ext-real set

(Partial_Sums (A2,(1 / 2))) . 0 is V28() real ext-real Element of REAL

(A2,(1 / 2)) . 0 is V28() real ext-real Element of REAL

(1 / 2) |^ 0 is V28() real ext-real set

(a,(1 / 2)) . A1 is V28() real ext-real Element of REAL

(Partial_Sums (a,(1 / 2))) . 0 is V28() real ext-real Element of REAL

(a,(1 / 2)) . 0 is V28() real ext-real Element of REAL

(Partial_Sums (A2,(1 / 2))) . A1 is V28() real ext-real Element of REAL

(Partial_Sums (a,(1 / 2))) . A1 is V28() real ext-real Element of REAL

((Partial_Sums (a,(1 / 2))) . A1) + ((1 / 2) |^ A1) is V28() real ext-real set

a is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational set

a + 1 is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT

a is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational set

a + 1 is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT

B is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT

(Partial_Sums (A2,(1 / 2))) . B is V28() real ext-real Element of REAL

(Partial_Sums (a,(1 / 2))) . B is V28() real ext-real Element of REAL

((Partial_Sums (a,(1 / 2))) . B) + 0 is V28() real ext-real set

(((Partial_Sums (a,(1 / 2))) . B) + 0) + ((1 / 2) |^ A1) is V28() real ext-real set

Sum (A2,(1 / 2)) is V28() real ext-real Element of REAL

A1 + 1 is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real finite cardinal integer rational V84() V85() V86() V87() V88() V89() Element of NAT

(a,(1 / 2)) ^\ (A1 + 1) is non empty Relation-like NAT -defined REAL -valued Function-like V33( NAT ) V34( NAT , REAL ) V37() V38() V39() Element of bool [:NAT,REAL:]

Sum ((a,(1 / 2)) ^\ (A1 + 1)) is V28() real ext-real Element of REAL

Sum (a,(1 / 2)) is V28() real ext-real Element of REAL

((Partial_Sums (a,(1 / 2))) . A1) + (Sum ((a,(1 / 2)) ^\ (A1 + 1))) is V28() real ext-real set

X is set

Fin X is preBoolean set

{{}} is non empty trivial finite V51() 1 -element V84() V85() V86() V87() V88() V89() set

X * is set

T is set

a is Relation-like Function-like FinSequence-like set

rng a is set

T is Relation-like Function-like set

dom T is set

rng T is set

a is set

T . a is set

a is set

T . a is set

A1 is Relation-like Function-like FinSequence-like set

rng A1 is set

A2 is Relation-like Function-like FinSequence-like set

rng A2 is set

len (Fin X) is epsilon-transitive epsilon-connected ordinal cardinal set

len (X *) is epsilon-transitive epsilon-connected ordinal cardinal set

exp (2,omega) is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal set

[0,0] is Element of [:NAT,NAT:]

[:NAT,NAT:] is non empty non trivial RAT -valued INT -valued V37() V38() V39() V40() non finite set

{0,0} is non empty finite V51() V84() V85() V86() V87() V88() V89() set

{0} is non empty trivial finite V51() 1 -element V84() V85() V86() V87() V88() V89() set

{{0,0},{0}} is non empty finite V51() set

{0} is non empty trivial proper finite V51() 1 -element V84() V85() V86() V87() V88() V89() Element of bool NAT

[:{0},RAT+:] is set

{[0,0]} is non empty trivial proper Relation-like NAT -defined NAT -valued INT -valued V37() V38() V39() V40() finite 1 -element Element of bool [:NAT,NAT:]

bool [:NAT,NAT:] is non empty non trivial non finite set

[:{0},RAT+:] \ {[0,0]} is Relation-like {0} -defined RAT+ -valued Element of bool [:{0},RAT+:]

bool [:{0},RAT+:] is non empty set

RAT+ \/ ([:{0},RAT+:] \ {[0,0]}) is set

bool RAT+ is non empty Element of bool (bool RAT+)

bool RAT is non empty non trivial non finite Element of bool (bool RAT)

bool RAT is non empty non trivial non finite set

bool (bool RAT) is non empty non trivial non finite set

RAT \/ (bool RAT) is non empty set

len REAL+ is epsilon-transitive epsilon-connected ordinal cardinal set

len (RAT \/ (bool RAT)) is non empty epsilon-transitive epsilon-connected ordinal cardinal set

bool NAT is non empty non trivial non finite Element of bool (bool NAT)

bool (bool NAT) is non empty non trivial non finite set

Fin NAT is preBoolean set

(bool NAT) \ (Fin NAT) is Element of bool (bool NAT)

len (bool RAT) is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal set

(len RAT) +` (len (bool RAT)) is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal set

(len REAL+) +` (len REAL+) is epsilon-transitive epsilon-connected ordinal cardinal set

(exp (2,omega)) +` (exp (2,omega)) is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal set

[:{0},REAL+:] is set

len [:{0},REAL+:] is epsilon-transitive epsilon-connected ordinal cardinal set

[:REAL+,{0}:] is RAT -valued INT -valued V37() V38() V39() V40() set

len [:REAL+,{0}:] is epsilon-transitive epsilon-connected ordinal cardinal set

REAL+ \/ [:{0},REAL+:] is set

len (REAL+ \/ [:{0},REAL+:]) is epsilon-transitive epsilon-connected ordinal cardinal set

(len REAL+) +` (len [:{0},REAL+:]) is epsilon-transitive epsilon-connected ordinal cardinal set

len (Fin NAT) is epsilon-transitive epsilon-connected ordinal cardinal set

len (bool NAT) is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal set

(len (bool NAT)) +` (len (Fin NAT)) is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal set

T is non empty set

[:T,REAL:] is non empty non trivial V37() V38() V39() non finite set

bool [:T,REAL:] is non empty non trivial non finite set

a is non empty Relation-like T -defined REAL -valued Function-like V33(T) V34(T, REAL ) V37() V38() V39() Element of bool [:T,REAL:]

a is set

dom a is set

a . a is V28() real ext-real set

A1 is set

a . A1 is V28() real ext-real set

dom a is Element of bool T

bool T is non empty set

(A1,(1 / 2)) is non empty Relation-like NAT -defined REAL -valued Function-like V33( NAT ) V34( NAT , REAL ) V37() V38() V39() Element of bool [:NAT,REAL:]

Sum (A1,(1 / 2)) is V28() real ext-real Element of REAL

(a,(1 / 2)) is non empty Relation-like NAT -defined REAL -valued Function-like V33( NAT ) V34( NAT , REAL ) V37() V38() V39() Element of bool [:NAT,REAL:]

Sum (a,(1 / 2)) is V28() real ext-real Element of REAL

rng a is V84() V85() V86() set

dom a is Element of bool T

bool T is non empty set

len T is non empty epsilon-transitive epsilon-connected ordinal cardinal set

bool omega is non empty non trivial non finite Element of bool (bool omega)

bool (bool omega) is non empty non trivial non finite set

len (bool omega) is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal set

{ b

X is Element of bool (bool REAL)

len X is epsilon-transitive epsilon-connected ordinal cardinal set

UniCl X is Element of bool (bool REAL)

{ b

( b

len { b

( b

(len X) *` omega is epsilon-transitive epsilon-connected ordinal cardinal set

len (len X) is epsilon-transitive epsilon-connected ordinal cardinal set

(len X) *` omega is epsilon-transitive epsilon-connected ordinal cardinal set

(len X) *` omega is epsilon-transitive epsilon-connected ordinal cardinal set

(len X) *` omega is epsilon-transitive epsilon-connected ordinal cardinal set

(len X) *` omega is epsilon-transitive epsilon-connected ordinal cardinal set

{ b

( b

bool REAL is non empty non trivial non finite Element of bool (bool REAL)

a is set

{ b

A1 is set

A2 is V28() real ext-real Element of REAL

[:X,(bool REAL):] is set

bool [:X,(bool REAL):] is non empty set

a is Relation-like X -defined bool REAL -valued Function-like V33(X) V34(X, bool REAL) Element of bool [:X,(bool REAL):]

A1 is set

A2 is V28() real ext-real Element of REAL

a is set

a is set

a is V84() V85() V86() Element of bool REAL

B is Element of bool (bool REAL)

union B is V84() V85() V86() Element of bool REAL

C is set

y is V28() real ext-real set

].y,A2.[ is V84() V85() V86() Element of bool REAL

C is V84() V85() V86() Element of bool REAL

b is set

Union a is set

rng a is set

union (rng a) is set

A1 is set

dom a is Element of bool X

bool X is non empty set

A2 is V28() real ext-real Element of REAL

a is set

a is set

a . a is set

{ b

len (Union a) is epsilon-transitive epsilon-connected ordinal cardinal set

A1 is set

a . A1 is set

len (a . A1) is epsilon-transitive epsilon-connected ordinal cardinal set

A2 is V84() V85() V86() Element of bool REAL

{ b

dom a is Element of bool X

bool X is non empty set

X is Element of bool (bool REAL)

len X is epsilon-transitive epsilon-connected ordinal cardinal set