REAL is non empty V46() V73() V74() V75() V79() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() Element of Trivial-SigmaField REAL
Trivial-SigmaField REAL is non empty V98() set
ExtREAL is non empty V74() set
+infty is non empty non real ext-real positive non negative set
-infty is non empty non real ext-real non positive negative set
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V71() V72() V73() V74() V75() V76() V77() V78() V79() Element of NAT
[0,REAL] is set
{0,REAL} is non empty V98() set
{0} is non empty V73() V74() V75() V76() V77() V78() set
{{0,REAL},{0}} is non empty set
{+infty,-infty} is non empty V74() set
REAL \/ {+infty,-infty} is non empty V74() set
K7(NAT,ExtREAL) is non empty V34() set
Trivial-SigmaField K7(NAT,ExtREAL) is non empty V98() set
Trivial-SigmaField ExtREAL is non empty V98() set
omega is non empty epsilon-transitive epsilon-connected ordinal V73() V74() V75() V76() V77() V78() V79() set
Trivial-SigmaField omega is non empty V98() set
K7(NAT,REAL) is non empty V33() V34() V35() set
Trivial-SigmaField K7(NAT,REAL) is non empty V98() set
Trivial-SigmaField (Trivial-SigmaField REAL) is non empty V98() set
Trivial-SigmaField NAT is non empty V98() set
COMPLEX is non empty V46() V73() V79() set
RAT is non empty V46() V73() V74() V75() V76() V79() set
INT is non empty V46() V73() V74() V75() V76() V77() V79() set
K7(COMPLEX,COMPLEX) is non empty V33() set
Trivial-SigmaField K7(COMPLEX,COMPLEX) is non empty V98() set
K7(K7(COMPLEX,COMPLEX),COMPLEX) is non empty V33() set
Trivial-SigmaField K7(K7(COMPLEX,COMPLEX),COMPLEX) is non empty V98() set
K7(REAL,REAL) is non empty V33() V34() V35() set
Trivial-SigmaField K7(REAL,REAL) is non empty V98() set
K7(K7(REAL,REAL),REAL) is non empty V33() V34() V35() set
Trivial-SigmaField K7(K7(REAL,REAL),REAL) is non empty V98() set
K7(RAT,RAT) is non empty V17( RAT ) V33() V34() V35() set
Trivial-SigmaField K7(RAT,RAT) is non empty V98() set
K7(K7(RAT,RAT),RAT) is non empty V17( RAT ) V33() V34() V35() set
Trivial-SigmaField K7(K7(RAT,RAT),RAT) is non empty V98() set
K7(INT,INT) is non empty V17( RAT ) V17( INT ) V33() V34() V35() set
Trivial-SigmaField K7(INT,INT) is non empty V98() set
K7(K7(INT,INT),INT) is non empty V17( RAT ) V17( INT ) V33() V34() V35() set
Trivial-SigmaField K7(K7(INT,INT),INT) is non empty V98() set
K7(NAT,NAT) is non empty V17( RAT ) V17( INT ) V33() V34() V35() V36() set
K7(K7(NAT,NAT),NAT) is non empty V17( RAT ) V17( INT ) V33() V34() V35() V36() set
Trivial-SigmaField K7(K7(NAT,NAT),NAT) is non empty V98() set
Trivial-SigmaField RAT is non empty V98() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V71() V72() V73() V74() V75() V76() V77() V78() Element of NAT
{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V73() V74() V75() V76() V77() V78() V79() set
].-infty,+infty.[ is set
Omega is V11() real ext-real set
Sigma is V11() real ext-real set
[.Omega,Sigma.[ is set
[.Omega,Sigma.[ is V73() V74() V75() Element of Trivial-SigmaField REAL
Omega is V11() real ext-real set
[.Omega,+infty.[ is V73() V74() V75() Element of Trivial-SigmaField REAL
REAL \ [.Omega,+infty.[ is V73() V74() V75() Element of Trivial-SigmaField REAL
].-infty,Omega.[ is V73() V74() V75() Element of Trivial-SigmaField REAL
Sigma is set
].-infty,+infty.[ is V73() V74() V75() Element of Trivial-SigmaField REAL
x is V11() real ext-real Element of REAL
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= -infty & not Omega <= b1 ) } is set
x is ext-real Element of ExtREAL
f is ext-real Element of ExtREAL
r is V11() real ext-real Element of REAL
Omega is V11() real ext-real set
].-infty,Omega.[ is V73() V74() V75() Element of Trivial-SigmaField REAL
REAL \ ].-infty,Omega.[ is V73() V74() V75() Element of Trivial-SigmaField REAL
[.Omega,+infty.[ is V73() V74() V75() Element of Trivial-SigmaField REAL
Sigma is set
].-infty,+infty.[ is V73() V74() V75() Element of Trivial-SigmaField REAL
x is V11() real ext-real Element of REAL
{ b1 where b1 is ext-real Element of ExtREAL : ( Omega <= b1 & not +infty <= b1 ) } is set
x is ext-real Element of ExtREAL
f is ext-real Element of ExtREAL
r is V11() real ext-real Element of REAL
K139(REAL) is non empty compl-closed sigma-multiplicative V98() Element of Trivial-SigmaField (Trivial-SigmaField REAL)
K7(NAT,K139(REAL)) is non empty set
Trivial-SigmaField K7(NAT,K139(REAL)) is non empty V98() set
Omega is V11() real ext-real set
Sigma is V11() real ext-real set
Sigma + 1 is V11() real ext-real Element of REAL
(Omega,(Sigma + 1)) is V73() V74() V75() Element of Trivial-SigmaField REAL
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V71() V72() V73() V74() V75() V76() V77() V78() Element of NAT
f is V73() V74() V75() Element of Trivial-SigmaField REAL
x + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V71() V72() V73() V74() V75() V76() V77() V78() Element of NAT
1 / (x + 1) is non empty V11() real ext-real positive non negative V72() Element of RAT
Sigma + (1 / (x + 1)) is V11() real ext-real Element of REAL
(Omega,(Sigma + (1 / (x + 1)))) is V73() V74() V75() Element of Trivial-SigmaField REAL
X is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
r is V73() V74() V75() Element of Trivial-SigmaField REAL
jpi is V73() V74() V75() Element of Trivial-SigmaField REAL
X + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V71() V72() V73() V74() V75() V76() V77() V78() Element of NAT
1 / (X + 1) is non empty V11() real ext-real positive non negative V72() Element of RAT
Sigma + (1 / (X + 1)) is V11() real ext-real Element of REAL
(Omega,(Sigma + (1 / (X + 1)))) is V73() V74() V75() Element of Trivial-SigmaField REAL
x is non empty V13() V16( NAT ) V17(K139(REAL)) Function-like V23( NAT ) V27( NAT ,K139(REAL)) Element of Trivial-SigmaField K7(NAT,K139(REAL))
x . 0 is V73() V74() V75() Element of K139(REAL)
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
f + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V71() V72() V73() V74() V75() V76() V77() V78() Element of NAT
x . (f + 1) is V73() V74() V75() Element of K139(REAL)
1 / (f + 1) is non empty V11() real ext-real positive non negative V72() Element of RAT
Sigma + (1 / (f + 1)) is V11() real ext-real Element of REAL
(Omega,(Sigma + (1 / (f + 1)))) is V73() V74() V75() Element of Trivial-SigmaField REAL
r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V71() V72() V73() V74() V75() V76() V77() V78() Element of NAT
x . r is V73() V74() V75() Element of K139(REAL)
r + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V71() V72() V73() V74() V75() V76() V77() V78() Element of NAT
x . (r + 1) is V73() V74() V75() Element of K139(REAL)
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
jpi is V73() V74() V75() Element of Trivial-SigmaField REAL
X is V73() V74() V75() Element of Trivial-SigmaField REAL
G + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V71() V72() V73() V74() V75() V76() V77() V78() Element of NAT
1 / (G + 1) is non empty V11() real ext-real positive non negative V72() Element of RAT
Sigma + (1 / (G + 1)) is V11() real ext-real Element of REAL
(Omega,(Sigma + (1 / (G + 1)))) is V73() V74() V75() Element of Trivial-SigmaField REAL
x is non empty V13() V16( NAT ) V17(K139(REAL)) Function-like V23( NAT ) V27( NAT ,K139(REAL)) Element of Trivial-SigmaField K7(NAT,K139(REAL))
x . 0 is V73() V74() V75() Element of K139(REAL)
f is non empty V13() V16( NAT ) V17(K139(REAL)) Function-like V23( NAT ) V27( NAT ,K139(REAL)) Element of Trivial-SigmaField K7(NAT,K139(REAL))
f . 0 is V73() V74() V75() Element of K139(REAL)
r is set
x . r is set
f . r is set
x . 0 is set
f . 0 is set
X is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V71() V72() V73() V74() V75() V76() V77() V78() Element of NAT
x . X is set
f . X is set
X + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V71() V72() V73() V74() V75() V76() V77() V78() Element of NAT
x . (X + 1) is set
f . (X + 1) is set
x . X is V73() V74() V75() Element of K139(REAL)
f . X is V73() V74() V75() Element of K139(REAL)
x . (X + 1) is V73() V74() V75() Element of K139(REAL)
1 / (X + 1) is non empty V11() real ext-real positive non negative V72() Element of RAT
Sigma + (1 / (X + 1)) is V11() real ext-real Element of REAL
(Omega,(Sigma + (1 / (X + 1)))) is V73() V74() V75() Element of Trivial-SigmaField REAL
f . (X + 1) is V73() V74() V75() Element of K139(REAL)
jpi is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V71() V72() V73() V74() V75() V76() V77() V78() Element of NAT
x . jpi is V73() V74() V75() Element of K139(REAL)
f . jpi is V73() V74() V75() Element of K139(REAL)
Omega is V11() real ext-real Element of REAL
NAT --> Omega is non empty T-Sequence-like V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of Trivial-SigmaField K7(NAT,REAL)
(NAT --> Omega) . 0 is V11() real ext-real Element of REAL
Sigma is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V71() V72() V73() V74() V75() V76() V77() V78() Element of NAT
(NAT --> Omega) . Sigma is V11() real ext-real Element of REAL
Omega is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of Trivial-SigmaField K7(NAT,REAL)
Sigma is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of Trivial-SigmaField K7(NAT,REAL)
Omega (#) Sigma is V13() V16( NAT ) Function-like V23( NAT ) V33() V34() V35() set
Omega (#) Sigma is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of Trivial-SigmaField K7(NAT,REAL)
Sigma is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of Trivial-SigmaField K7(NAT,REAL)
x is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of Trivial-SigmaField K7(NAT,REAL)
(Sigma,x) is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of Trivial-SigmaField K7(NAT,REAL)
Partial_Sums (Sigma,x) is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of Trivial-SigmaField K7(NAT,REAL)
Omega is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
(Partial_Sums (Sigma,x)) . Omega is V11() real ext-real Element of REAL
(Sigma,x) ^\ 1 is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of Trivial-SigmaField K7(NAT,REAL)
Partial_Sums ((Sigma,x) ^\ 1) is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of Trivial-SigmaField K7(NAT,REAL)
Omega - 1 is V11() real ext-real Element of REAL
(Partial_Sums ((Sigma,x) ^\ 1)) . (Omega - 1) is V11() real ext-real Element of REAL
Omega is set
Trivial-SigmaField Omega is non empty V98() set
Trivial-SigmaField (Trivial-SigmaField Omega) is non empty V98() set
Sigma is set
Trivial-SigmaField Sigma is non empty V98() set
Trivial-SigmaField (Trivial-SigmaField Sigma) is non empty V98() set
Omega is set
Trivial-SigmaField Omega is non empty V98() set
Trivial-SigmaField (Trivial-SigmaField Omega) is non empty V98() set
Sigma is set
Trivial-SigmaField Sigma is non empty V98() set
Trivial-SigmaField (Trivial-SigmaField Sigma) is non empty V98() set
K7(Omega,Sigma) is set
Trivial-SigmaField K7(Omega,Sigma) is non empty V98() set
x is non empty compl-closed sigma-multiplicative V98() Element of Trivial-SigmaField (Trivial-SigmaField Omega)
f is non empty compl-closed sigma-multiplicative V98() Element of Trivial-SigmaField (Trivial-SigmaField Sigma)
{ b1 where b1 is V13() V16(Omega) V17(Sigma) Function-like V27(Omega,Sigma) Element of Trivial-SigmaField K7(Omega,Sigma) : (Omega,Sigma,x,f,b1) } is set
Omega is non empty set
Trivial-SigmaField Omega is non empty V98() set
Trivial-SigmaField (Trivial-SigmaField Omega) is non empty V98() set
Sigma is non empty set
Trivial-SigmaField Sigma is non empty V98() set
Trivial-SigmaField (Trivial-SigmaField Sigma) is non empty V98() set
x is non empty compl-closed sigma-multiplicative V98() Element of Trivial-SigmaField (Trivial-SigmaField Omega)
f is non empty compl-closed sigma-multiplicative V98() Element of Trivial-SigmaField (Trivial-SigmaField Sigma)
(Omega,Sigma,x,f) is set
K7(Omega,Sigma) is non empty set
Trivial-SigmaField K7(Omega,Sigma) is non empty V98() set
{ b1 where b1 is V13() V16(Omega) V17(Sigma) Function-like V27(Omega,Sigma) Element of Trivial-SigmaField K7(Omega,Sigma) : (Omega,Sigma,x,f,b1) } is set
the Element of Sigma is Element of Sigma
Omega --> the Element of Sigma is non empty V13() V16(Omega) V17(Sigma) Function-like V23(Omega) V27(Omega,Sigma) Element of Trivial-SigmaField K7(Omega,Sigma)
G is Element of f
{ b1 where b1 is Element of Omega : (Omega --> the Element of Sigma) . b1 is Element of G } is set
G is Element of f
{ b1 where b1 is Element of Omega : (Omega --> the Element of Sigma) . b1 is Element of G } is set
w is set
g2 is Element of Omega
(Omega --> the Element of Sigma) . g2 is Element of Sigma
(Omega --> the Element of Sigma) . w is set
w is set
g2 is Element of Omega
(Omega --> the Element of Sigma) . g2 is Element of Sigma
G is Element of f
{ b1 where b1 is Element of Omega : (Omega --> the Element of Sigma) . b1 is Element of G } is set
jpi is non empty V13() V16(Omega) V17(Sigma) Function-like V23(Omega) V27(Omega,Sigma) Element of Trivial-SigmaField K7(Omega,Sigma)
jpi is non empty V13() V16(Omega) V17(Sigma) Function-like V23(Omega) V27(Omega,Sigma) Element of Trivial-SigmaField K7(Omega,Sigma)
Omega is non empty set
Trivial-SigmaField Omega is non empty V98() set
Trivial-SigmaField (Trivial-SigmaField Omega) is non empty V98() set
Sigma is non empty set
Trivial-SigmaField Sigma is non empty V98() set
Trivial-SigmaField (Trivial-SigmaField Sigma) is non empty V98() set
r is set
x is non empty compl-closed sigma-multiplicative V98() Element of Trivial-SigmaField (Trivial-SigmaField Omega)
f is non empty compl-closed sigma-multiplicative V98() Element of Trivial-SigmaField (Trivial-SigmaField Sigma)
(Omega,Sigma,x,f) is non empty set
K7(Omega,Sigma) is non empty set
Trivial-SigmaField K7(Omega,Sigma) is non empty V98() set
{ b1 where b1 is V13() V16(Omega) V17(Sigma) Function-like V27(Omega,Sigma) Element of Trivial-SigmaField K7(Omega,Sigma) : (Omega,Sigma,x,f,b1) } is set
jpi is Element of r
X is non empty V13() V16(Omega) V17(Sigma) Function-like V23(Omega) V27(Omega,Sigma) Element of Trivial-SigmaField K7(Omega,Sigma)
Omega is non empty set
Trivial-SigmaField Omega is non empty V98() set
Trivial-SigmaField (Trivial-SigmaField Omega) is non empty V98() set
x is non empty set
K7(Omega,REAL) is non empty V33() V34() V35() set
Trivial-SigmaField K7(Omega,REAL) is non empty V98() set
Sigma is non empty compl-closed sigma-multiplicative V98() Element of Trivial-SigmaField (Trivial-SigmaField Omega)
Borel_Sets is non empty compl-closed sigma-multiplicative V98() Element of Trivial-SigmaField (Trivial-SigmaField REAL)
Family_of_halflines is Element of Trivial-SigmaField (Trivial-SigmaField REAL)
{ (halfline b1) where b1 is V11() real ext-real Element of REAL : verum } is set
sigma Family_of_halflines is non empty compl-closed sigma-multiplicative V98() Element of Trivial-SigmaField (Trivial-SigmaField REAL)
f is Element of x
(Omega,REAL,Sigma,Borel_Sets,x,f) is non empty V13() V16(Omega) V17( REAL ) Function-like V23(Omega) V27(Omega, REAL ) V33() V34() V35() Element of Trivial-SigmaField K7(Omega,REAL)
r is non empty V13() V16(Omega) V17( REAL ) Function-like V23(Omega) V27(Omega, REAL ) V33() V34() V35() Element of Trivial-SigmaField K7(Omega,REAL)
r is non empty V13() V16(Omega) V17( REAL ) Function-like V23(Omega) V27(Omega, REAL ) V33() V34() V35() Element of Trivial-SigmaField K7(Omega,REAL)
jpi is non empty V13() V16(Omega) V17( REAL ) Function-like V23(Omega) V27(Omega, REAL ) V33() V34() V35() Element of Trivial-SigmaField K7(Omega,REAL)
X is Element of Omega
r . X is V11() real ext-real set
jpi . X is V11() real ext-real set
r . X is V11() real ext-real Element of REAL
(Omega,REAL,Sigma,Borel_Sets,x,f) . X is V11() real ext-real Element of REAL
jpi . X is V11() real ext-real Element of REAL
Sigma is non empty set
Trivial-SigmaField Sigma is non empty V98() set
Trivial-SigmaField (Trivial-SigmaField Sigma) is non empty V98() set
x is non empty set
Trivial-SigmaField x is non empty V98() set
Trivial-SigmaField (Trivial-SigmaField x) is non empty V98() set
jpi is set
f is non empty compl-closed sigma-multiplicative V98() Element of Trivial-SigmaField (Trivial-SigmaField Sigma)
r is non empty compl-closed sigma-multiplicative V98() Element of Trivial-SigmaField (Trivial-SigmaField x)
(Sigma,x,f,r) is non empty set
K7(Sigma,x) is non empty set
Trivial-SigmaField K7(Sigma,x) is non empty V98() set
{ b1 where b1 is V13() V16(Sigma) V17(x) Function-like V27(Sigma,x) Element of Trivial-SigmaField K7(Sigma,x) : (Sigma,x,f,r,b1) } is set
K7(NAT,jpi) is set
Trivial-SigmaField K7(NAT,jpi) is non empty V98() set
X is V13() V16( NAT ) V17(jpi) Function-like V27( NAT ,jpi) Element of Trivial-SigmaField K7(NAT,jpi)
Omega is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
X . Omega is set
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V71() V72() V73() V74() V75() V76() V77() V78() Element of NAT
X . G is Element of jpi
x is non empty V13() V16(Sigma) V17(x) Function-like V23(Sigma) V27(Sigma,x) Element of Trivial-SigmaField K7(Sigma,x)
Omega is non empty set
Trivial-SigmaField Omega is non empty V98() set
Trivial-SigmaField (Trivial-SigmaField Omega) is non empty V98() set
x is non empty set
K7(NAT,x) is non empty set
Trivial-SigmaField K7(NAT,x) is non empty V98() set
Sigma is non empty compl-closed sigma-multiplicative V98() Element of Trivial-SigmaField (Trivial-SigmaField Omega)
r is non empty V13() V16( NAT ) V17(x) Function-like V23( NAT ) V27( NAT ,x) Element of Trivial-SigmaField K7(NAT,x)
f is Element of Omega
jpi is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of Trivial-SigmaField K7(NAT,REAL)
X is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of Trivial-SigmaField K7(NAT,REAL)
X is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of Trivial-SigmaField K7(NAT,REAL)
G is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of Trivial-SigmaField K7(NAT,REAL)
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V71() V72() V73() V74() V75() V76() V77() V78() Element of NAT
X . x is V11() real ext-real set
G . x is V11() real ext-real set
X . x is V11() real ext-real Element of REAL
r . x is Element of x
(Omega,Sigma,x,(r . x)) is non empty V13() V16(Omega) V17( REAL ) Function-like V23(Omega) V27(Omega, REAL ) V33() V34() V35() Element of Trivial-SigmaField K7(Omega,REAL)
K7(Omega,REAL) is non empty V33() V34() V35() set
Trivial-SigmaField K7(Omega,REAL) is non empty V98() set
(Omega,Sigma,x,(r . x)) . f is V11() real ext-real Element of REAL
jpi . x is V11() real ext-real Element of REAL
((Omega,Sigma,x,(r . x)) . f) * (jpi . x) is V11() real ext-real Element of REAL
G . x is V11() real ext-real Element of REAL
x is non empty set
Trivial-SigmaField x is non empty V98() set
Trivial-SigmaField (Trivial-SigmaField x) is non empty V98() set
r is non empty set
K7(NAT,r) is non empty set
Trivial-SigmaField K7(NAT,r) is non empty V98() set
f is non empty compl-closed sigma-multiplicative V98() Element of Trivial-SigmaField (Trivial-SigmaField x)
X is Element of x
jpi is non empty V13() V16( NAT ) V17(r) Function-like V23( NAT ) V27( NAT ,r) Element of Trivial-SigmaField K7(NAT,r)
Sigma is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of Trivial-SigmaField K7(NAT,REAL)
(x,f,r,X,jpi,Sigma) is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of Trivial-SigmaField K7(NAT,REAL)
Partial_Sums (x,f,r,X,jpi,Sigma) is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of Trivial-SigmaField K7(NAT,REAL)
Omega is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
(Partial_Sums (x,f,r,X,jpi,Sigma)) . Omega is V11() real ext-real Element of REAL
(x,f,r,X,jpi,Sigma) ^\ 1 is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of Trivial-SigmaField K7(NAT,REAL)
Partial_Sums ((x,f,r,X,jpi,Sigma) ^\ 1) is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of Trivial-SigmaField K7(NAT,REAL)
Omega - 1 is V11() real ext-real Element of REAL
(Partial_Sums ((x,f,r,X,jpi,Sigma) ^\ 1)) . (Omega - 1) is V11() real ext-real Element of REAL
Omega is V11() real ext-real set
halfline Omega is V73() V74() V75() Element of Trivial-SigmaField REAL
].-infty,Omega.[ is set
Trivial-SigmaField Borel_Sets is non empty V98() set
Omega is V11() real ext-real set
[.Omega,+infty.[ is V73() V74() V75() Element of Trivial-SigmaField REAL
].-infty,Omega.[ is V73() V74() V75() Element of Trivial-SigmaField REAL
halfline Omega is V73() V74() V75() Element of Trivial-SigmaField REAL
].-infty,Omega.[ is set
].-infty,Omega.[ ` is V73() V74() V75() Element of Trivial-SigmaField REAL
REAL \ ].-infty,Omega.[ is V73() V74() V75() set
Sigma is V11() real ext-real set
Omega is V11() real ext-real set
[.Sigma,Omega.[ is V73() V74() V75() Element of Trivial-SigmaField REAL
].-infty,Sigma.[ is V73() V74() V75() Element of Trivial-SigmaField REAL
REAL \ ].-infty,Sigma.[ is V73() V74() V75() Element of Trivial-SigmaField REAL
[.Sigma,+infty.[ is V73() V74() V75() Element of Trivial-SigmaField REAL
].-infty,Sigma.[ ` is V73() V74() V75() Element of Trivial-SigmaField REAL
REAL \ ].-infty,Sigma.[ is V73() V74() V75() set
].-infty,Omega.[ is V73() V74() V75() Element of Trivial-SigmaField REAL
[.Omega,+infty.[ is V73() V74() V75() Element of Trivial-SigmaField REAL
].-infty,Omega.[ /\ (].-infty,Sigma.[ `) is V73() V74() V75() Element of Trivial-SigmaField REAL
].-infty,Omega.[ /\ [.Sigma,+infty.[ is V73() V74() V75() Element of Trivial-SigmaField REAL
Omega is V11() real ext-real set
Sigma is V11() real ext-real set
(Omega,Sigma) is non empty V13() V16( NAT ) V17(K139(REAL)) Function-like V23( NAT ) V27( NAT ,K139(REAL)) Element of Trivial-SigmaField K7(NAT,K139(REAL))
Intersection (Omega,Sigma) is V73() V74() V75() Element of Trivial-SigmaField REAL
Complement (Omega,Sigma) is non empty V13() V16( NAT ) V17(K139(REAL)) Function-like V23( NAT ) V27( NAT ,K139(REAL)) Element of Trivial-SigmaField K7(NAT,K139(REAL))
Union (Complement (Omega,Sigma)) is V73() V74() V75() Element of Trivial-SigmaField REAL
(Union (Complement (Omega,Sigma))) ` is V73() V74() V75() Element of Trivial-SigmaField REAL
REAL \ (Union (Complement (Omega,Sigma))) is V73() V74() V75() set
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V71() V72() V73() V74() V75() V76() V77() V78() Element of NAT
(Complement (Omega,Sigma)) . x is V73() V74() V75() Element of K139(REAL)
(Omega,Sigma) . x is V73() V74() V75() Element of K139(REAL)
((Omega,Sigma) . x) ` is V73() V74() V75() Element of Trivial-SigmaField REAL
REAL \ ((Omega,Sigma) . x) is V73() V74() V75() set
(Omega,Sigma) . 0 is V73() V74() V75() Element of K139(REAL)
Sigma + 1 is V11() real ext-real Element of REAL
(Omega,(Sigma + 1)) is V73() V74() V75() Element of Trivial-SigmaField REAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
f + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V71() V72() V73() V74() V75() V76() V77() V78() Element of NAT
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
f + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V71() V72() V73() V74() V75() V76() V77() V78() Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V71() V72() V73() V74() V75() V76() V77() V78() Element of NAT
r + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V71() V72() V73() V74() V75() V76() V77() V78() Element of NAT
(Omega,Sigma) . (r + 1) is V73() V74() V75() Element of K139(REAL)
1 / (r + 1) is non empty V11() real ext-real positive non negative V72() Element of RAT
Sigma + (1 / (r + 1)) is V11() real ext-real Element of REAL
(Omega,(Sigma + (1 / (r + 1)))) is V73() V74() V75() Element of Trivial-SigmaField REAL
Omega is V11() real ext-real set
Sigma is V11() real ext-real set
(Omega,Sigma) is non empty V13() V16( NAT ) V17(K139(REAL)) Function-like V23( NAT ) V27( NAT ,K139(REAL)) Element of Trivial-SigmaField K7(NAT,K139(REAL))
Intersection (Omega,Sigma) is V73() V74() V75() Element of Trivial-SigmaField REAL
Complement (Omega,Sigma) is non empty V13() V16( NAT ) V17(K139(REAL)) Function-like V23( NAT ) V27( NAT ,K139(REAL)) Element of Trivial-SigmaField K7(NAT,K139(REAL))
Union (Complement (Omega,Sigma)) is V73() V74() V75() Element of Trivial-SigmaField REAL
(Union (Complement (Omega,Sigma))) ` is V73() V74() V75() Element of Trivial-SigmaField REAL
REAL \ (Union (Complement (Omega,Sigma))) is V73() V74() V75() set
[.Omega,Sigma.] is V73() V74() V75() Element of Trivial-SigmaField REAL
x is set
f is V11() real ext-real Element of REAL
{ b1 where b1 is ext-real Element of ExtREAL : ( Omega <= b1 & b1 <= Sigma ) } is set
r is ext-real Element of ExtREAL
r is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V71() V72() V73() V74() V75() V76() V77() V78() V79() Element of NAT
(Omega,Sigma) . r is V73() V74() V75() Element of K139(REAL)
(Omega,Sigma) . 0 is V73() V74() V75() Element of K139(REAL)
Sigma + 1 is V11() real ext-real Element of REAL
(Omega,(Sigma + 1)) is V73() V74() V75() Element of Trivial-SigmaField REAL
{ b1 where b1 is ext-real Element of ExtREAL : ( Omega <= b1 & not Sigma + 1 <= b1 ) } is set
jpi is ext-real Element of ExtREAL
r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V71() V72() V73() V74() V75() V76() V77() V78() Element of NAT
(Omega,Sigma) . r is V73() V74() V75() Element of K139(REAL)
f - Sigma is V11() real ext-real Element of REAL
r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V71() V72() V73() V74() V75() V76() V77() V78() Element of NAT
1 / r is V11() real ext-real non negative V72() Element of RAT
(f - Sigma) + Sigma is V11() real ext-real Element of REAL
(1 / r) + Sigma is V11() real ext-real Element of REAL
Sigma + (1 / r) is V11() real ext-real Element of REAL
r + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V71() V72() V73() V74() V75() V76() V77() V78() Element of NAT
(Omega,Sigma) . (r + 1) is V73() V74() V75() Element of K139(REAL)
1 / (r + 1) is non empty V11() real ext-real positive non negative V72() Element of RAT
Sigma + (1 / (r + 1)) is V11() real ext-real Element of REAL
[.Omega,(Sigma + (1 / (r + 1))).[ is V73() V74() V75() Element of Trivial-SigmaField REAL
{ b1 where b1 is ext-real Element of ExtREAL : ( Omega <= b1 & not Sigma + (1 / (r + 1)) <= b1 ) } is set
jpi is ext-real Element of ExtREAL
(r + 1) * 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V71() V72() V73() V74() V75() V76() V77() V78() Element of NAT
r * 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V71() V72() V73() V74() V75() V76() V77() V78() Element of NAT
X is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V71() V72() V73() V74() V75() V76() V77() V78() Element of NAT
X / r is V11() real ext-real non negative V72() Element of RAT
X / (r + 1) is V11() real ext-real non negative V72() Element of RAT
x is set
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V71() V72() V73() V74() V75() V76() V77() V78() Element of NAT
(Omega,Sigma) . f is V73() V74() V75() Element of K139(REAL)
Sigma + 1 is V11() real ext-real Element of REAL
(Omega,Sigma) . 0 is V73() V74() V75() Element of K139(REAL)
(Omega,(Sigma + 1)) is V73() V74() V75() Element of Trivial-SigmaField REAL
r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
r + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V71() V72() V73() V74() V75() V76() V77() V78() Element of NAT
jpi is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V71() V72() V73() V74() V75() V76() V77() V78() Element of NAT
jpi + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V71() V72() V73() V74() V75() V76() V77() V78() Element of NAT
(Omega,Sigma) . (jpi + 1) is V73() V74() V75() Element of K139(REAL)
1 / (jpi + 1) is non empty V11() real ext-real positive non negative V72() Element of RAT
Sigma + (1 / (jpi + 1)) is V11() real ext-real Element of REAL
(Omega,(Sigma + (1 / (jpi + 1)))) is V73() V74() V75() Element of Trivial-SigmaField REAL
1 / f is V11() real ext-real non negative V72() Element of RAT
Sigma + (1 / f) is V11() real ext-real Element of REAL
x is set
f is set
Omega is V11() real ext-real set
Sigma is V11() real ext-real set
(Omega,Sigma) is non empty V13() V16( NAT ) V17(K139(REAL)) Function-like V23( NAT ) V27( NAT ,K139(REAL)) Element of Trivial-SigmaField K7(NAT,K139(REAL))
Partial_Intersection (Omega,Sigma) is non empty V13() V16( NAT ) V17(K139(REAL)) Function-like V23( NAT ) V27( NAT ,K139(REAL)) Element of Trivial-SigmaField K7(NAT,K139(REAL))
(Partial_Intersection (Omega,Sigma)) . 0 is set
(Partial_Intersection (Omega,Sigma)) . 0 is V73() V74() V75() Element of K139(REAL)
(Omega,Sigma) . 0 is V73() V74() V75() Element of K139(REAL)
Sigma + 1 is V11() real ext-real Element of REAL
(Omega,(Sigma + 1)) is V73() V74() V75() Element of Trivial-SigmaField REAL
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
(Partial_Intersection (Omega,Sigma)) . x is set
x + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V71() V72() V73() V74() V75() V76() V77() V78() Element of NAT
(Partial_Intersection (Omega,Sigma)) . (x + 1) is set
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V71() V72() V73() V74() V75() V76() V77() V78() Element of NAT
f + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V71() V72() V73() V74() V75() V76() V77() V78() Element of NAT
(Partial_Intersection (Omega,Sigma)) . (f + 1) is V73() V74() V75() Element of K139(REAL)
(Partial_Intersection (Omega,Sigma)) . f is V73() V74() V75() Element of K139(REAL)
(Omega,Sigma) . (f + 1) is V73() V74() V75() Element of K139(REAL)
((Partial_Intersection (Omega,Sigma)) . f) /\ ((Omega,Sigma) . (f + 1)) is V73() V74() V75() M9( REAL ,K139(REAL))
1 / (f + 1) is non empty V11() real ext-real positive non negative V72() Element of RAT
Sigma + (1 / (f + 1)) is V11() real ext-real Element of REAL
(Omega,(Sigma + (1 / (f + 1)))) is V73() V74() V75() Element of Trivial-SigmaField REAL
((Partial_Intersection (Omega,Sigma)) . f) /\ (Omega,(Sigma + (1 / (f + 1)))) is V73() V74() V75() Element of Trivial-SigmaField REAL
[.Omega,(Sigma + (1 / (f + 1))).[ is V73() V74() V75() Element of Trivial-SigmaField REAL
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
(Partial_Intersection (Omega,Sigma)) . x is set
Sigma is V11() real ext-real set
Omega is V11() real ext-real set
[.Sigma,Omega.] is V73() V74() V75() Element of Trivial-SigmaField REAL
(Sigma,Omega) is non empty V13() V16( NAT ) V17(K139(REAL)) Function-like V23( NAT ) V27( NAT ,K139(REAL)) Element of Trivial-SigmaField K7(NAT,K139(REAL))
Intersection (Sigma,Omega) is V73() V74() V75() Element of Trivial-SigmaField REAL
Complement (Sigma,Omega) is non empty V13() V16( NAT ) V17(K139(REAL)) Function-like V23( NAT ) V27( NAT ,K139(REAL)) Element of Trivial-SigmaField K7(NAT,K139(REAL))
Union (Complement (Sigma,Omega)) is V73() V74() V75() Element of Trivial-SigmaField REAL
(Union (Complement (Sigma,Omega))) ` is V73() V74() V75() Element of Trivial-SigmaField REAL
REAL \ (Union (Complement (Sigma,Omega))) is V73() V74() V75() set
Omega is non empty set
Trivial-SigmaField Omega is non empty V98() set
Trivial-SigmaField (Trivial-SigmaField Omega) is non empty V98() set
K7(Omega,REAL) is non empty V33() V34() V35() set
Trivial-SigmaField K7(Omega,REAL) is non empty V98() set
Sigma is non empty compl-closed sigma-multiplicative V98() Element of Trivial-SigmaField (Trivial-SigmaField Omega)
x is non empty V13() V16(Omega) V17( REAL ) Function-like V23(Omega) V27(Omega, REAL ) V33() V34() V35() Element of Trivial-SigmaField K7(Omega,REAL)
f is V11() real ext-real set
{ b1 where b1 is Element of Omega : f <= x . b1 } is set
{ b1 where b1 is Element of Omega : not f <= x . b1 } is set
[.f,+infty.] is set
r is set
jpi is Element of Omega
x . jpi is V11() real ext-real Element of REAL
jpi is Element of Omega
x . jpi is V11() real ext-real Element of REAL
{ b1 where b1 is ext-real Element of ExtREAL : ( f <= b1 & b1 <= +infty ) } is set
X is ext-real Element of ExtREAL
jpi is Element of Omega
x . jpi is V11() real ext-real Element of REAL
X is Element of Omega
x . X is V11() real ext-real Element of REAL
G is Element of Omega
x . G is V11() real ext-real Element of REAL
[.f,+infty.[ is V73() V74() V75() Element of Trivial-SigmaField REAL
{ b1 where b1 is Element of Omega : x . b1 in [.f,+infty.[ } is set
r is set
jpi is Element of Omega
x . jpi is V11() real ext-real Element of REAL
jpi is Element of Omega
x . jpi is V11() real ext-real Element of REAL
X is Element of Omega
x . X is V11() real ext-real Element of REAL
{ b1 where b1 is Element of Omega : x . b1 in [.f,+infty.] } is set
jpi is Element of Omega
x . jpi is V11() real ext-real Element of REAL
{ b1 where b1 is ext-real Element of ExtREAL : ( f <= b1 & b1 <= +infty ) } is set
X is ext-real Element of ExtREAL
{ b1 where b1 is ext-real Element of ExtREAL : ( f <= b1 & not +infty <= b1 ) } is set
jpi is Element of Omega
x . jpi is V11() real ext-real Element of REAL
X is ext-real Element of ExtREAL
jpi is Element of Omega
x . jpi is V11() real ext-real Element of REAL
{ b1 where b1 is Element of Omega : x . b1 is V11() real ext-real Element of [.f,+infty.[ } is set
r is set
jpi is Element of Omega
x . jpi is V11() real ext-real Element of REAL
jpi is Element of Omega
x . jpi is V11() real ext-real Element of REAL
].-infty,f.[ is V73() V74() V75() Element of Trivial-SigmaField REAL
[.-infty,f.[ is set
r is set
jpi is Element of Omega
x . jpi is V11() real ext-real Element of REAL
jpi is Element of Omega
x . jpi is V11() real ext-real Element of REAL
{ b1 where b1 is ext-real Element of ExtREAL : ( -infty <= b1 & not f <= b1 ) } is set
X is ext-real Element of ExtREAL
jpi is Element of Omega
x . jpi is V11() real ext-real Element of REAL
X is Element of Omega
x . X is V11() real ext-real Element of REAL
G is Element of Omega
x . G is V11() real ext-real Element of REAL
{ b1 where b1 is Element of Omega : x . b1 in ].-infty,f.[ } is set
r is set
jpi is Element of Omega
x . jpi is V11() real ext-real Element of REAL
jpi is Element of Omega
x . jpi is V11() real ext-real Element of REAL
X is Element of Omega
x . X is V11() real ext-real Element of REAL
{ b1 where b1 is Element of Omega : x . b1 in [.-infty,f.[ } is set
jpi is Element of Omega
x . jpi is V11() real ext-real Element of REAL
{ b1 where b1 is ext-real Element of ExtREAL : ( -infty <= b1 & not f <= b1 ) } is set
X is ext-real Element of ExtREAL
{ b1 where b1 is ext-real Element of ExtREAL : ( not b1 <= -infty & not f <= b1 ) } is set
jpi is Element of Omega
x . jpi is V11() real ext-real Element of REAL
X is ext-real Element of ExtREAL
jpi is Element of Omega
x . jpi is V11() real ext-real Element of REAL
{ b1 where b1 is Element of Omega : x . b1 is V11() real ext-real Element of ].-infty,f.[ } is set
r is set
jpi is Element of Omega
x . jpi is V11() real ext-real Element of REAL
jpi is Element of Omega
x . jpi is V11() real ext-real Element of REAL
r is V11() real ext-real set
f is V11() real ext-real set
{ b1 where b1 is Element of Omega : ( f <= x . b1 & not r <= x . b1 ) } is set
[.f,r.[ is V73() V74() V75() Element of Trivial-SigmaField REAL
{ b1 where b1 is Element of Omega : x . b1 is V11() real ext-real Element of [.f,r.[ } is set
jpi is set
X is Element of Omega
x . X is V11() real ext-real Element of REAL
R_EAL (x . X) is ext-real Element of ExtREAL
G is ext-real Element of ExtREAL
{ b1 where b1 is ext-real Element of ExtREAL : ( f <= b1 & not r <= b1 ) } is set
X is Element of Omega
x . X is V11() real ext-real Element of REAL
G is ext-real Element of ExtREAL
[.r,f.[ is V73() V74() V75() Element of Trivial-SigmaField REAL
f is V11() real ext-real set
r is V11() real ext-real set
{ b1 where b1 is Element of Omega : ( f <= x . b1 & x . b1 <= r ) } is set
[.f,r.] is V73() V74() V75() Element of Trivial-SigmaField REAL
{ b1 where b1 is Element of Omega : x . b1 is V11() real ext-real Element of [.f,r.] } is set
jpi is set
X is Element of Omega
x . X is V11() real ext-real Element of REAL
R_EAL (x . X) is ext-real Element of ExtREAL
G is ext-real Element of ExtREAL
{ b1 where b1 is ext-real Element of ExtREAL : ( f <= b1 & b1 <= r ) } is set
X is Element of Omega
x . X is V11() real ext-real Element of REAL
G is ext-real Element of ExtREAL
[.f,r.[ is V73() V74() V75() Element of Trivial-SigmaField REAL
f is V11() real ext-real set
less_dom (x,f) is set
{ b1 where b1 is Element of Omega : not f <= x . b1 } is set
r is set
dom x is Element of Trivial-SigmaField Omega
x . r is V11() real ext-real Element of REAL
jpi is Element of Omega
x . jpi is V11() real ext-real Element of REAL
jpi is Element of Omega
x . jpi is V11() real ext-real Element of REAL
f is V11() real ext-real set
great_eq_dom (x,f) is set
{ b1 where b1 is Element of Omega : f <= x . b1 } is set
r is set
dom x is Element of Trivial-SigmaField Omega
x . r is V11() real ext-real Element of REAL
jpi is Element of Omega
x . jpi is V11() real ext-real Element of REAL
jpi is Element of Omega
x . jpi is V11() real ext-real Element of REAL
f is V11() real ext-real set
eq_dom (x,f) is set
{ b1 where b1 is Element of Omega : x . b1 = f } is set
r is set
dom x is Element of Trivial-SigmaField Omega
x . r is V11() real ext-real Element of REAL
jpi is Element of Omega
x . jpi is V11() real ext-real Element of REAL
jpi is Element of Omega
x . jpi is V11() real ext-real Element of REAL
f is V11() real ext-real set
eq_dom (x,f) is set
{ b1 where b1 is Element of Omega : ( f <= x . b1 & x . b1 <= f ) } is set
{ b1 where b1 is Element of Omega : x . b1 = f } is set
r is set
jpi is Element of Omega
x . jpi is V11() real ext-real Element of REAL
jpi is Element of Omega
x . jpi is V11() real ext-real Element of REAL
X is Element of Omega
x . X is V11() real ext-real Element of REAL
jpi is Element of Omega
x . jpi is V11() real ext-real Element of REAL
f is V11() real ext-real set
{ b1 where b1 is Element of Omega : f <= x . b1 } is set
r is V11() real ext-real set
{ b1 where b1 is Element of Omega : not r <= x . b1 } is set
X is V11() real ext-real set
jpi is V11() real ext-real set
{ b1 where b1 is Element of Omega : ( jpi <= x . b1 & not X <= x . b1 ) } is set
G is V11() real ext-real set
x is V11() real ext-real set
{ b1 where b1 is Element of Omega : ( G <= x . b1 & x . b1 <= x ) } is set
w is V11() real ext-real set
less_dom (x,w) is set
{ b1 where b1 is Element of Omega : not w <= x . b1 } is set
g2 is V11() real ext-real set
great_eq_dom (x,g2) is set
{ b1 where b1 is Element of Omega : g2 <= x . b1 } is set
c12 is V11() real ext-real set
eq_dom (x,c12) is set
{ b1 where b1 is Element of Omega : x . b1 = c12 } is set
c13 is V11() real ext-real set
eq_dom (x,c13) is set
Omega is non empty set
Trivial-SigmaField Omega is non empty V98() set
Trivial-SigmaField (Trivial-SigmaField Omega) is non empty V98() set
Sigma is non empty compl-closed sigma-multiplicative V98() Element of Trivial-SigmaField (Trivial-SigmaField Omega)
x is V11() real ext-real set
Omega --> x is non empty V13() V16(Omega) V17({x}) Function-like V23(Omega) V27(Omega,{x}) V33() V34() V35() Element of Trivial-SigmaField K7(Omega,{x})
{x} is non empty V73() V74() V75() set
K7(Omega,{x}) is non empty V33() V34() V35() set
Trivial-SigmaField K7(Omega,{x}) is non empty V98() set
r is Element of Borel_Sets
{ b1 where b1 is Element of Omega : (Omega --> x) . b1 is Element of r } is set
{ b1 where b1 is Element of Omega : (Omega --> x) . b1 is Element of r } is set
jpi is set
X is Element of Omega
(Omega --> x) . X is V11() real ext-real Element of REAL
X is Element of Omega
(Omega --> x) . X is V11() real ext-real Element of REAL
{ b1 where b1 is Element of Omega : (Omega --> x) . b1 is Element of r } is set
jpi is set
X is Element of Omega
(Omega --> x) . X is V11() real ext-real Element of REAL
Omega is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of Trivial-SigmaField K7(NAT,REAL)
Omega . 0 is V11() real ext-real Element of REAL
Sigma is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() ()
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
(x,Omega,Sigma) is V11() real ext-real Element of REAL
(Omega,Sigma) is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of Trivial-SigmaField K7(NAT,REAL)
Partial_Sums (Omega,Sigma) is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of Trivial-SigmaField K7(NAT,REAL)
(Partial_Sums (Omega,Sigma)) . x is V11() real ext-real Element of REAL
(x,Omega,Sigma) is V11() real ext-real Element of REAL
(Omega,Sigma) ^\ 1 is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of Trivial-SigmaField K7(NAT,REAL)
Partial_Sums ((Omega,Sigma) ^\ 1) is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of Trivial-SigmaField K7(NAT,REAL)
x - 1 is V11() real ext-real Element of REAL
(Partial_Sums ((Omega,Sigma) ^\ 1)) . (x - 1) is V11() real ext-real Element of REAL
(Omega . 0) + (x,Omega,Sigma) is V11() real ext-real Element of REAL
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V71() V72() V73() V74() V75() V76() V77() V78() Element of NAT
(Partial_Sums (Omega,Sigma)) . (0 + 1) is V11() real ext-real Element of REAL
(Partial_Sums ((Omega,Sigma) ^\ 1)) . 0 is V11() real ext-real Element of REAL
(Omega . 0) + ((Partial_Sums ((Omega,Sigma) ^\ 1)) . 0) is V11() real ext-real Element of REAL
(Partial_Sums (Omega,Sigma)) . 0 is V11() real ext-real Element of REAL
(Omega,Sigma) . 1 is V11() real ext-real Element of REAL
((Partial_Sums (Omega,Sigma)) . 0) + ((Omega,Sigma) . 1) is V11() real ext-real Element of REAL
(Omega,Sigma) . 0 is V11() real ext-real Element of REAL
((Omega,Sigma) . 0) + ((Omega,Sigma) . 1) is V11() real ext-real Element of REAL
((Omega,Sigma) ^\ 1) . 0 is V11() real ext-real Element of REAL
((Omega,Sigma) . 0) + (((Omega,Sigma) ^\ 1) . 0) is V11() real ext-real Element of REAL
((Omega,Sigma) . 0) + ((Partial_Sums ((Omega,Sigma) ^\ 1)) . 0) is V11() real ext-real Element of REAL
Sigma . 0 is V11() real ext-real Element of REAL
(Omega . 0) * (Sigma . 0) is V11() real ext-real Element of REAL
((Omega . 0) * (Sigma . 0)) + ((Partial_Sums ((Omega,Sigma) ^\ 1)) . 0) is V11() real ext-real Element of REAL
(Omega . 0) * 1 is V11() real ext-real Element of REAL
((Omega . 0) * 1) + ((Partial_Sums ((Omega,Sigma) ^\ 1)) . 0) is V11() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
f + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V71() V72() V73() V74() V75() V76() V77() V78() Element of NAT
(Partial_Sums (Omega,Sigma)) . (f + 1) is V11() real ext-real Element of REAL
(Partial_Sums ((Omega,Sigma) ^\ 1)) . f is V11() real ext-real Element of REAL
(Omega . 0) + ((Partial_Sums ((Omega,Sigma) ^\ 1)) . f) is V11() real ext-real Element of REAL
(f + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V71() V72() V73() V74() V75() V76() V77() V78() Element of NAT
(Partial_Sums (Omega,Sigma)) . ((f + 1) + 1) is V11() real ext-real Element of REAL
(Partial_Sums ((Omega,Sigma) ^\ 1)) . (f + 1) is V11() real ext-real Element of REAL
(Omega . 0) + ((Partial_Sums ((Omega,Sigma) ^\ 1)) . (f + 1)) is V11() real ext-real Element of REAL
r is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V71() V72() V73() V74() V75() V76() V77() V78() Element of NAT
r + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V71() V72() V73() V74() V75() V76() V77() V78() Element of NAT
(r + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V71() V72() V73() V74() V75() V76() V77() V78() Element of NAT
(Partial_Sums (Omega,Sigma)) . ((r + 1) + 1) is V11() real ext-real Element of REAL
(Partial_Sums ((Omega,Sigma) ^\ 1)) . r is V11() real ext-real Element of REAL
(Omega . 0) + ((Partial_Sums ((Omega,Sigma) ^\ 1)) . r) is V11() real ext-real Element of REAL
(Omega,Sigma) . ((r + 1) + 1) is V11() real ext-real Element of REAL
((Omega . 0) + ((Partial_Sums ((Omega,Sigma) ^\ 1)) . r)) + ((Omega,Sigma) . ((r + 1) + 1)) is V11() real ext-real Element of REAL
((Omega,Sigma) ^\ 1) . (r + 1) is V11() real ext-real Element of REAL
((Omega . 0) + ((Partial_Sums ((Omega,Sigma) ^\ 1)) . r)) + (((Omega,Sigma) ^\ 1) . (r + 1)) is V11() real ext-real Element of REAL
((Partial_Sums ((Omega,Sigma) ^\ 1)) . r) + (((Omega,Sigma) ^\ 1) . (r + 1)) is V11() real ext-real Element of REAL
(Omega . 0) + (((Partial_Sums ((Omega,Sigma) ^\ 1)) . r) + (((Omega,Sigma) ^\ 1) . (r + 1))) is V11() real ext-real Element of REAL
(x - 1) + 1 is V11() real ext-real Element of REAL
(Partial_Sums (Omega,Sigma)) . ((x - 1) + 1) is V11() real ext-real Element of REAL
Omega is non empty set
Trivial-SigmaField Omega is non empty V98() set
Trivial-SigmaField (Trivial-SigmaField Omega) is non empty V98() set
Sigma is non empty compl-closed sigma-multiplicative V98() Element of Trivial-SigmaField (Trivial-SigmaField Omega)
(Omega,REAL,Sigma,Borel_Sets) is non empty set
K7(Omega,REAL) is non empty V33() V34() V35() set
Trivial-SigmaField K7(Omega,REAL) is non empty V98() set
{ b1 where b1 is V13() V16(Omega) V17( REAL ) Function-like V27(Omega, REAL ) Element of Trivial-SigmaField K7(Omega,REAL) : (Omega, REAL ,Sigma, Borel_Sets ,b1) } is set
K7(NAT,(Omega,REAL,Sigma,Borel_Sets)) is non empty set
Trivial-SigmaField K7(NAT,(Omega,REAL,Sigma,Borel_Sets)) is non empty V98() set
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
f is V11() real ext-real set
1 + f is V11() real ext-real Element of REAL
Omega --> (1 + f) is non empty V13() V16(Omega) V17( REAL ) Function-like V23(Omega) V27(Omega, REAL ) V33() V34() V35() Element of Trivial-SigmaField K7(Omega,REAL)
r is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of Trivial-SigmaField K7(NAT,REAL)
r . 0 is V11() real ext-real Element of REAL
(1 + f) * (r . 0) is V11() real ext-real Element of REAL
X is non empty V13() V16( NAT ) V17((Omega,REAL,Sigma,Borel_Sets)) Function-like V23( NAT ) V27( NAT ,(Omega,REAL,Sigma,Borel_Sets)) Element of Trivial-SigmaField K7(NAT,(Omega,REAL,Sigma,Borel_Sets))
(0,Omega,REAL,Sigma,Borel_Sets,(Omega,REAL,Sigma,Borel_Sets),X) is non empty V13() V16(Omega) V17( REAL ) Function-like V23(Omega) V27(Omega, REAL ) V33() V34() V35() Element of Trivial-SigmaField K7(Omega,REAL)
G is Element of Omega
(x,r,Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),X,G) is V11() real ext-real Element of REAL
(Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),G,X,r) is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of Trivial-SigmaField K7(NAT,REAL)
Partial_Sums (Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),G,X,r) is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of Trivial-SigmaField K7(NAT,REAL)
(Partial_Sums (Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),G,X,r)) . x is V11() real ext-real Element of REAL
(x,r,Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),X,G) is V11() real ext-real Element of REAL
(Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),G,X,r) ^\ 1 is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of Trivial-SigmaField K7(NAT,REAL)
Partial_Sums ((Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),G,X,r) ^\ 1) is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of Trivial-SigmaField K7(NAT,REAL)
x - 1 is V11() real ext-real Element of REAL
(Partial_Sums ((Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),G,X,r) ^\ 1)) . (x - 1) is V11() real ext-real Element of REAL
((1 + f) * (r . 0)) + (x,r,Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),X,G) is V11() real ext-real Element of REAL
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V71() V72() V73() V74() V75() V76() V77() V78() Element of NAT
(Partial_Sums (Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),G,X,r)) . (0 + 1) is V11() real ext-real Element of REAL
(Partial_Sums ((Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),G,X,r) ^\ 1)) . 0 is V11() real ext-real Element of REAL
((1 + f) * (r . 0)) + ((Partial_Sums ((Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),G,X,r) ^\ 1)) . 0) is V11() real ext-real Element of REAL
(Partial_Sums (Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),G,X,r)) . 0 is V11() real ext-real Element of REAL
(Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),G,X,r) . 1 is V11() real ext-real Element of REAL
((Partial_Sums (Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),G,X,r)) . 0) + ((Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),G,X,r) . 1) is V11() real ext-real Element of REAL
(Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),G,X,r) . 0 is V11() real ext-real Element of REAL
((Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),G,X,r) . 0) + ((Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),G,X,r) . 1) is V11() real ext-real Element of REAL
((Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),G,X,r) ^\ 1) . 0 is V11() real ext-real Element of REAL
((Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),G,X,r) . 0) + (((Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),G,X,r) ^\ 1) . 0) is V11() real ext-real Element of REAL
((Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),G,X,r) . 0) + ((Partial_Sums ((Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),G,X,r) ^\ 1)) . 0) is V11() real ext-real Element of REAL
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V71() V72() V73() V74() V75() V76() V77() V78() Element of NAT
x + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V71() V72() V73() V74() V75() V76() V77() V78() Element of NAT
(Partial_Sums (Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),G,X,r)) . (x + 1) is V11() real ext-real Element of REAL
(Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),G,X,r) . x is V11() real ext-real Element of REAL
(Partial_Sums ((Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),G,X,r) ^\ 1)) . x is V11() real ext-real Element of REAL
((Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),G,X,r) . x) + ((Partial_Sums ((Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),G,X,r) ^\ 1)) . x) is V11() real ext-real Element of REAL
X . x is Element of (Omega,REAL,Sigma,Borel_Sets)
(Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),(X . x)) is non empty V13() V16(Omega) V17( REAL ) Function-like V23(Omega) V27(Omega, REAL ) V33() V34() V35() Element of Trivial-SigmaField K7(Omega,REAL)
(Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),(X . x)) . G is V11() real ext-real Element of REAL
r . x is V11() real ext-real Element of REAL
((Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),(X . x)) . G) * (r . x) is V11() real ext-real Element of REAL
(((Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),(X . x)) . G) * (r . x)) + ((Partial_Sums ((Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),G,X,r) ^\ 1)) . x) is V11() real ext-real Element of REAL
(Omega,REAL,Sigma,Borel_Sets,(Omega,REAL,Sigma,Borel_Sets),(X . x)) is non empty V13() V16(Omega) V17( REAL ) Function-like V23(Omega) V27(Omega, REAL ) V33() V34() V35() Element of Trivial-SigmaField K7(Omega,REAL)
(Omega,REAL,Sigma,Borel_Sets,(Omega,REAL,Sigma,Borel_Sets),(X . x)) . G is V11() real ext-real Element of REAL
X . 0 is Element of (Omega,REAL,Sigma,Borel_Sets)
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
x + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V71() V72() V73() V74() V75() V76() V77() V78() Element of NAT
(Partial_Sums (Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),G,X,r)) . (x + 1) is V11() real ext-real Element of REAL
(Partial_Sums ((Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),G,X,r) ^\ 1)) . x is V11() real ext-real Element of REAL
((1 + f) * (r . 0)) + ((Partial_Sums ((Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),G,X,r) ^\ 1)) . x) is V11() real ext-real Element of REAL
(x + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V71() V72() V73() V74() V75() V76() V77() V78() Element of NAT
(Partial_Sums (Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),G,X,r)) . ((x + 1) + 1) is V11() real ext-real Element of REAL
(Partial_Sums ((Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),G,X,r) ^\ 1)) . (x + 1) is V11() real ext-real Element of REAL
((1 + f) * (r . 0)) + ((Partial_Sums ((Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),G,X,r) ^\ 1)) . (x + 1)) is V11() real ext-real Element of REAL
w is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V71() V72() V73() V74() V75() V76() V77() V78() Element of NAT
w + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V71() V72() V73() V74() V75() V76() V77() V78() Element of NAT
(w + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V71() V72() V73() V74() V75() V76() V77() V78() Element of NAT
(Partial_Sums (Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),G,X,r)) . ((w + 1) + 1) is V11() real ext-real Element of REAL
(Partial_Sums ((Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),G,X,r) ^\ 1)) . w is V11() real ext-real Element of REAL
((1 + f) * (r . 0)) + ((Partial_Sums ((Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),G,X,r) ^\ 1)) . w) is V11() real ext-real Element of REAL
(Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),G,X,r) . ((w + 1) + 1) is V11() real ext-real Element of REAL
(((1 + f) * (r . 0)) + ((Partial_Sums ((Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),G,X,r) ^\ 1)) . w)) + ((Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),G,X,r) . ((w + 1) + 1)) is V11() real ext-real Element of REAL
((Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),G,X,r) ^\ 1) . (w + 1) is V11() real ext-real Element of REAL
(((1 + f) * (r . 0)) + ((Partial_Sums ((Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),G,X,r) ^\ 1)) . w)) + (((Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),G,X,r) ^\ 1) . (w + 1)) is V11() real ext-real Element of REAL
((Partial_Sums ((Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),G,X,r) ^\ 1)) . w) + (((Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),G,X,r) ^\ 1) . (w + 1)) is V11() real ext-real Element of REAL
((1 + f) * (r . 0)) + (((Partial_Sums ((Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),G,X,r) ^\ 1)) . w) + (((Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),G,X,r) ^\ 1) . (w + 1))) is V11() real ext-real Element of REAL
(x - 1) + 1 is V11() real ext-real Element of REAL
(Partial_Sums (Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),G,X,r)) . ((x - 1) + 1) is V11() real ext-real Element of REAL
((1 + f) * (r . 0)) + ((Partial_Sums ((Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),G,X,r) ^\ 1)) . (x - 1)) is V11() real ext-real Element of REAL
- 1 is non empty V11() real ext-real non positive negative V71() V72() Element of INT
Omega is non empty set
Trivial-SigmaField Omega is non empty V98() set
Trivial-SigmaField (Trivial-SigmaField Omega) is non empty V98() set
Sigma is non empty compl-closed sigma-multiplicative V98() Element of Trivial-SigmaField (Trivial-SigmaField Omega)
(Omega,REAL,Sigma,Borel_Sets) is non empty set
K7(Omega,REAL) is non empty V33() V34() V35() set
Trivial-SigmaField K7(Omega,REAL) is non empty V98() set
{ b1 where b1 is V13() V16(Omega) V17( REAL ) Function-like V27(Omega, REAL ) Element of Trivial-SigmaField K7(Omega,REAL) : (Omega, REAL ,Sigma, Borel_Sets ,b1) } is set
K7(NAT,(Omega,REAL,Sigma,Borel_Sets)) is non empty set
Trivial-SigmaField K7(NAT,(Omega,REAL,Sigma,Borel_Sets)) is non empty V98() set
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
f is V11() real ext-real set
1 + f is V11() real ext-real Element of REAL
Omega --> (1 + f) is non empty V13() V16(Omega) V17( REAL ) Function-like V23(Omega) V27(Omega, REAL ) V33() V34() V35() Element of Trivial-SigmaField K7(Omega,REAL)
r is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of Trivial-SigmaField K7(NAT,REAL)
jpi is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() ()
(x,r,jpi) is V11() real ext-real Element of REAL
(r,jpi) is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of Trivial-SigmaField K7(NAT,REAL)
Partial_Sums (r,jpi) is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of Trivial-SigmaField K7(NAT,REAL)
(Partial_Sums (r,jpi)) . x is V11() real ext-real Element of REAL
(x,r,jpi) is V11() real ext-real Element of REAL
(r,jpi) ^\ 1 is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of Trivial-SigmaField K7(NAT,REAL)
Partial_Sums ((r,jpi) ^\ 1) is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of Trivial-SigmaField K7(NAT,REAL)
x - 1 is V11() real ext-real Element of REAL
(Partial_Sums ((r,jpi) ^\ 1)) . (x - 1) is V11() real ext-real Element of REAL
(1 + f) * (x,r,jpi) is V11() real ext-real Element of REAL
G is non empty V13() V16( NAT ) V17((Omega,REAL,Sigma,Borel_Sets)) Function-like V23( NAT ) V27( NAT ,(Omega,REAL,Sigma,Borel_Sets)) Element of Trivial-SigmaField K7(NAT,(Omega,REAL,Sigma,Borel_Sets))
(0,Omega,REAL,Sigma,Borel_Sets,(Omega,REAL,Sigma,Borel_Sets),G) is non empty V13() V16(Omega) V17( REAL ) Function-like V23(Omega) V27(Omega, REAL ) V33() V34() V35() Element of Trivial-SigmaField K7(Omega,REAL)
x is Element of Omega
(x,r,Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),G,x) is V11() real ext-real Element of REAL
(Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),x,G,r) is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of Trivial-SigmaField K7(NAT,REAL)
Partial_Sums (Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),x,G,r) is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of Trivial-SigmaField K7(NAT,REAL)
(Partial_Sums (Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),x,G,r)) . x is V11() real ext-real Element of REAL
(x,r,Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),G,x) is V11() real ext-real Element of REAL
(Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),x,G,r) ^\ 1 is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of Trivial-SigmaField K7(NAT,REAL)
Partial_Sums ((Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),x,G,r) ^\ 1) is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of Trivial-SigmaField K7(NAT,REAL)
(Partial_Sums ((Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),x,G,r) ^\ 1)) . (x - 1) is V11() real ext-real Element of REAL
(x,r,Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),G,x) - ((1 + f) * (x,r,jpi)) is V11() real ext-real Element of REAL
(1 + f) * (x,r,jpi) is V11() real ext-real Element of REAL
(x,r,Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),G,x) - ((1 + f) * (x,r,jpi)) is V11() real ext-real Element of REAL
((1 + f) * (x,r,jpi)) + ((x,r,Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),G,x) - ((1 + f) * (x,r,jpi))) is V11() real ext-real Element of REAL
r . 0 is V11() real ext-real Element of REAL
(r . 0) + (x,r,jpi) is V11() real ext-real Element of REAL
(1 + f) * ((r . 0) + (x,r,jpi)) is V11() real ext-real Element of REAL
(x,r,Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),G,x) - ((1 + f) * ((r . 0) + (x,r,jpi))) is V11() real ext-real Element of REAL
(1 + f) * (r . 0) is V11() real ext-real Element of REAL
((x,r,Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),G,x) - ((1 + f) * (x,r,jpi))) - ((1 + f) * (r . 0)) is V11() real ext-real Element of REAL
(x,r,Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),G,x) + ((1 + f) * (r . 0)) is V11() real ext-real Element of REAL
Omega is non empty set
Trivial-SigmaField Omega is non empty V98() set
Trivial-SigmaField (Trivial-SigmaField Omega) is non empty V98() set
Sigma is non empty compl-closed sigma-multiplicative V98() Element of Trivial-SigmaField (Trivial-SigmaField Omega)
(Omega,REAL,Sigma,Borel_Sets) is non empty set
K7(Omega,REAL) is non empty V33() V34() V35() set
Trivial-SigmaField K7(Omega,REAL) is non empty V98() set
{ b1 where b1 is V13() V16(Omega) V17( REAL ) Function-like V27(Omega, REAL ) Element of Trivial-SigmaField K7(Omega,REAL) : (Omega, REAL ,Sigma, Borel_Sets ,b1) } is set
K7(NAT,(Omega,REAL,Sigma,Borel_Sets)) is non empty set
Trivial-SigmaField K7(NAT,(Omega,REAL,Sigma,Borel_Sets)) is non empty V98() set
x is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
f is V11() real ext-real set
1 + f is V11() real ext-real Element of REAL
Omega --> (1 + f) is non empty V13() V16(Omega) V17( REAL ) Function-like V23(Omega) V27(Omega, REAL ) V33() V34() V35() Element of Trivial-SigmaField K7(Omega,REAL)
r is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of Trivial-SigmaField K7(NAT,REAL)
jpi is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() ()
(x,r,jpi) is V11() real ext-real Element of REAL
(r,jpi) is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of Trivial-SigmaField K7(NAT,REAL)
Partial_Sums (r,jpi) is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of Trivial-SigmaField K7(NAT,REAL)
(Partial_Sums (r,jpi)) . x is V11() real ext-real Element of REAL
(x,r,jpi) is V11() real ext-real Element of REAL
(r,jpi) ^\ 1 is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of Trivial-SigmaField K7(NAT,REAL)
Partial_Sums ((r,jpi) ^\ 1) is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of Trivial-SigmaField K7(NAT,REAL)
x - 1 is V11() real ext-real Element of REAL
(Partial_Sums ((r,jpi) ^\ 1)) . (x - 1) is V11() real ext-real Element of REAL
(1 + f) * (x,r,jpi) is V11() real ext-real Element of REAL
G is non empty V13() V16( NAT ) V17((Omega,REAL,Sigma,Borel_Sets)) Function-like V23( NAT ) V27( NAT ,(Omega,REAL,Sigma,Borel_Sets)) Element of Trivial-SigmaField K7(NAT,(Omega,REAL,Sigma,Borel_Sets))
(0,Omega,REAL,Sigma,Borel_Sets,(Omega,REAL,Sigma,Borel_Sets),G) is non empty V13() V16(Omega) V17( REAL ) Function-like V23(Omega) V27(Omega, REAL ) V33() V34() V35() Element of Trivial-SigmaField K7(Omega,REAL)
{ b1 where b1 is Element of Omega : 0 <= (x,r,Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),G,b1) } is set
{ b1 where b1 is Element of Omega : (1 + f) * (x,r,jpi) <= (x,r,Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),G,b1) } is set
{ b1 where b1 is Element of Omega : not (x,r,Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),G,b1) <= 0 } is set
{ b1 where b1 is Element of Omega : not (x,r,Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),G,b1) <= (1 + f) * (x,r,jpi) } is set
x is set
w is Element of Omega
(x,r,Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),G,w) is V11() real ext-real Element of REAL
(Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),w,G,r) is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of Trivial-SigmaField K7(NAT,REAL)
Partial_Sums (Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),w,G,r) is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of Trivial-SigmaField K7(NAT,REAL)
(Partial_Sums (Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),w,G,r)) . x is V11() real ext-real Element of REAL
(x,r,Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),G,w) is V11() real ext-real Element of REAL
(Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),w,G,r) ^\ 1 is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of Trivial-SigmaField K7(NAT,REAL)
Partial_Sums ((Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),w,G,r) ^\ 1) is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of Trivial-SigmaField K7(NAT,REAL)
(Partial_Sums ((Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),w,G,r) ^\ 1)) . (x - 1) is V11() real ext-real Element of REAL
(x,r,Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),G,w) - ((1 + f) * (x,r,jpi)) is V11() real ext-real Element of REAL
0 + ((1 + f) * (x,r,jpi)) is V11() real ext-real Element of REAL
x is set
w is Element of Omega
(x,r,Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),G,w) is V11() real ext-real Element of REAL
(Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),w,G,r) is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of Trivial-SigmaField K7(NAT,REAL)
Partial_Sums (Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),w,G,r) is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of Trivial-SigmaField K7(NAT,REAL)
(Partial_Sums (Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),w,G,r)) . x is V11() real ext-real Element of REAL
(x,r,Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),G,w) is V11() real ext-real Element of REAL
(Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),w,G,r) ^\ 1 is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of Trivial-SigmaField K7(NAT,REAL)
Partial_Sums ((Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),w,G,r) ^\ 1) is non empty V13() V16( NAT ) V17( REAL ) Function-like V23( NAT ) V27( NAT , REAL ) V33() V34() V35() Element of Trivial-SigmaField K7(NAT,REAL)
(Partial_Sums ((Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),w,G,r) ^\ 1)) . (x - 1) is V11() real ext-real Element of REAL
(x,r,Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),G,w) - ((1 + f) * (x,r,jpi)) is V11() real ext-real Element of REAL
((x,r,Omega,Sigma,(Omega,REAL,Sigma,Borel_Sets),G,w) - ((1 + f) * (x,r,jpi))) + ((1 + f) * (x,r,jpi)) is V11() real ext-real Element of REAL
0 + ((1 + f) * (x,r,jpi)) is V11() real ext-real Element of REAL
Omega is non empty set
Trivial-SigmaField Omega is non empty V98() set
Trivial-SigmaField (Trivial-SigmaField Omega) is non empty V98() set
K7(Omega,REAL) is non empty V33() V34() V35() set
Trivial-SigmaField K7(Omega,REAL) is non empty V98() set
Sigma is non empty compl-closed sigma-multiplicative V98() Element of Trivial-SigmaField (Trivial-SigmaField Omega)
[#] Sigma is M9(Omega,Sigma)
x is non empty V13() V16(Omega) V17( REAL ) Function-like V23(Omega) V27(Omega, REAL ) V33() V34() V35() Element of Trivial-SigmaField K7(Omega,REAL)
f is V11() real ext-real Element of REAL
less_dom (x,f) is set
Omega /\ (less_dom (x,f)) is set
{ b1 where b1 is Element of Omega : not f <= x . b1 } is set
f is V11() real ext-real set
less_dom (x,f) is set
([#] Sigma) /\ (less_dom (x,f)) is Element of Trivial-SigmaField Omega
r is V11() real ext-real Element of REAL
less_dom (x,r) is set
([#] Sigma) /\ (less_dom (x,r)) is Element of Trivial-SigmaField Omega
f is Element of Sigma
f is Element of Sigma
Omega is non empty set
Trivial-SigmaField Omega is non empty V98() set
Trivial-SigmaField (Trivial-SigmaField Omega) is non empty V98() set
Sigma is non empty compl-closed sigma-multiplicative V98() Element of Trivial-SigmaField (Trivial-SigmaField Omega)
(Omega,REAL,Sigma,Borel_Sets) is non empty set
K7(Omega,REAL) is non empty V33() V34() V35() set
Trivial-SigmaField K7(Omega,REAL) is non empty V98() set
{ b1 where b1 is V13() V16(Omega) V17( REAL ) Function-like V27(Omega, REAL ) Element of Trivial-SigmaField K7(Omega,REAL) : (Omega, REAL ,Sigma, Borel_Sets ,b1) } is set
Real-Valued-Random-Variables-Set Sigma is non empty Element of Trivial-SigmaField the U1 of K527(Omega)
K527(Omega) is V202() L14()
the U1 of K527(Omega) is set
Trivial-SigmaField the U1 of K527(Omega) is non empty V98() set
x is set
f is non empty V13() V16(Omega) V17( REAL ) Function-like V23(Omega) V27(Omega, REAL ) V33() V34() V35() Element of Trivial-SigmaField K7(Omega,REAL)
{ b1 where b1 is non empty V13() V16(Omega) V17( REAL ) Function-like V23(Omega) V27(Omega, REAL ) V33() V34() V35() Real-Valued-Random-Variable of Sigma : verum } is set