:: BOR_CANT semantic presentation

REAL is non empty V34() V70() V71() V72() V76() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() Element of bool REAL
bool REAL is non empty V94() set
COMPLEX is non empty V34() V70() V76() set
RAT is non empty V34() V70() V71() V72() V73() V76() set
INT is non empty V34() V70() V71() V72() V73() V74() V76() set
[:COMPLEX,COMPLEX:] is non empty Relation-like V59() set
bool [:COMPLEX,COMPLEX:] is non empty V94() set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty Relation-like V59() set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty V94() set
[:REAL,REAL:] is non empty Relation-like V59() V60() V61() set
bool [:REAL,REAL:] is non empty V94() set
[:[:REAL,REAL:],REAL:] is non empty Relation-like V59() V60() V61() set
bool [:[:REAL,REAL:],REAL:] is non empty V94() set
[:RAT,RAT:] is non empty Relation-like RAT -valued V59() V60() V61() set
bool [:RAT,RAT:] is non empty V94() set
[:[:RAT,RAT:],RAT:] is non empty Relation-like RAT -valued V59() V60() V61() set
bool [:[:RAT,RAT:],RAT:] is non empty V94() set
[:INT,INT:] is non empty Relation-like RAT -valued INT -valued V59() V60() V61() set
bool [:INT,INT:] is non empty V94() set
[:[:INT,INT:],INT:] is non empty Relation-like RAT -valued INT -valued V59() V60() V61() set
bool [:[:INT,INT:],INT:] is non empty V94() set
[:NAT,NAT:] is non empty Relation-like RAT -valued INT -valued V59() V60() V61() V62() set
[:[:NAT,NAT:],NAT:] is non empty Relation-like RAT -valued INT -valued V59() V60() V61() V62() set
bool [:[:NAT,NAT:],NAT:] is non empty V94() set
omega is non empty epsilon-transitive epsilon-connected ordinal V70() V71() V72() V73() V74() V75() V76() set
bool omega is non empty V94() set
bool NAT is non empty V94() set
K246() is set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real positive non negative V70() V71() V72() V73() V74() V75() Element of NAT
[:NAT,REAL:] is non empty Relation-like V59() V60() V61() set
bool [:NAT,REAL:] is non empty V94() set
[:NAT,COMPLEX:] is non empty Relation-like V59() set
bool [:NAT,COMPLEX:] is non empty V94() set
bool (bool REAL) is non empty V94() set
[:COMPLEX,REAL:] is non empty Relation-like V59() V60() V61() set
bool [:COMPLEX,REAL:] is non empty V94() set
{} is empty Relation-like non-empty empty-yielding RAT -valued functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() real V42() V44() ext-real non positive non negative V59() V60() V61() V62() V70() V71() V72() V73() V74() V75() V76() set
K2({},1) is non empty V70() V71() V72() V73() V74() V75() set
0 is empty Relation-like non-empty empty-yielding RAT -valued functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() real V30() V31() V42() V44() ext-real non positive non negative V59() V60() V61() V62() V70() V71() V72() V73() V74() V75() V76() Element of NAT
2 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real positive non negative V70() V71() V72() V73() V74() V75() Element of NAT
3 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real positive non negative V70() V71() V72() V73() V74() V75() Element of NAT
exp_R is non empty Relation-like REAL -defined REAL -valued Function-like V17( REAL ) V18( REAL , REAL ) V59() V60() V61() Element of bool [:REAL,REAL:]
exp_R 0 is V28() real ext-real Element of REAL
exp_R . 0 is V28() real ext-real Element of REAL
0 ! is non empty epsilon-transitive epsilon-connected ordinal natural V28() real ext-real positive non negative Element of REAL
Prod_real_n is non empty Relation-like NAT -defined REAL -valued Function-like V17( NAT ) V18( NAT , REAL ) V59() V60() V61() Element of bool [:NAT,REAL:]
Prod_real_n . 0 is V28() real ext-real Element of REAL
K234(0) is empty Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() real Function-yielding V33() V34() V41( 0 ) V42() V43() V44() ext-real non positive non negative V59() V60() V61() V62() V70() V71() V72() V73() V74() V75() V76() set
K436(K234(0)) is V28() set
1 ! is non empty epsilon-transitive epsilon-connected ordinal natural V28() real ext-real positive non negative Element of REAL
Prod_real_n . 1 is V28() real ext-real Element of REAL
K234(1) is Relation-like NAT -defined RAT -valued Function-like V34() V41(1) V42() V43() V59() V60() V61() V62() set
K436(K234(1)) is V28() set
Omega is set
Sigma is ext-real set
Prob is ext-real set
A is Element of Omega
n is Element of Omega
IFGT (Sigma,Prob,A,n) is set
Omega is epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
Omega + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real positive non negative V70() V71() V72() V73() V74() V75() Element of NAT
Omega + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real positive non negative V70() V71() V72() V73() V74() V75() Element of NAT
Sigma is V28() real ext-real Element of REAL
- Sigma is V28() real ext-real Element of REAL
(- Sigma) rExpSeq is non empty Relation-like NAT -defined REAL -valued Function-like V17( NAT ) V18( NAT , REAL ) V59() V60() V61() Element of bool [:NAT,REAL:]
((- Sigma) rExpSeq) . (Omega + 1) is V28() real ext-real Element of REAL
((- Sigma) rExpSeq) . (Omega + 2) is V28() real ext-real Element of REAL
(((- Sigma) rExpSeq) . (Omega + 1)) + (((- Sigma) rExpSeq) . (Omega + 2)) is V28() real ext-real Element of REAL
Prob is epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 * Prob is epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real non negative V70() V71() V72() V73() V74() V75() even Element of NAT
(2 * Prob) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real positive non negative V70() V71() V72() V73() V74() V75() non even Element of NAT
Prob + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real positive non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 * (Prob + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real positive non negative V70() V71() V72() V73() V74() V75() even Element of NAT
(2 * (Prob + 1)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real positive non negative V70() V71() V72() V73() V74() V75() non even Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 * n is epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real non negative V70() V71() V72() V73() V74() V75() even Element of NAT
(2 * n) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real positive non negative V70() V71() V72() V73() V74() V75() non even Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
(- Sigma) |^ n is V28() real ext-real Element of REAL
K235(n,(- Sigma)) is Relation-like NAT -defined Function-like V34() V41(n) V42() V43() V59() set
K436(K235(n,(- Sigma))) is V28() set
k is epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 * k is epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real non negative V70() V71() V72() V73() V74() V75() even Element of NAT
2 * 0 is empty Relation-like non-empty empty-yielding RAT -valued functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() real V30() V31() V42() V44() ext-real non positive non negative V59() V60() V61() V62() V70() V71() V72() V73() V74() V75() V76() even Element of NAT
(- Sigma) |^ (2 * 0) is V28() real ext-real Element of REAL
K235((2 * 0),(- Sigma)) is Relation-like NAT -defined Function-like V34() V41(2 * 0) V42() V43() V59() set
K436(K235((2 * 0),(- Sigma))) is V28() set
B2 is epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 * B2 is epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real non negative V70() V71() V72() V73() V74() V75() even Element of NAT
(- Sigma) |^ (2 * B2) is V28() real ext-real Element of REAL
K235((2 * B2),(- Sigma)) is Relation-like NAT -defined Function-like V34() V41(2 * B2) V42() V43() V59() set
K436(K235((2 * B2),(- Sigma))) is V28() set
B2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real positive non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 * (B2 + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real positive non negative V70() V71() V72() V73() V74() V75() even Element of NAT
(- Sigma) |^ (2 * (B2 + 1)) is V28() real ext-real Element of REAL
K235((2 * (B2 + 1)),(- Sigma)) is Relation-like NAT -defined Function-like V34() V41(2 * (B2 + 1)) V42() V43() V59() set
K436(K235((2 * (B2 + 1)),(- Sigma))) is V28() set
(2 * B2) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real positive non negative V70() V71() V72() V73() V74() V75() even Element of NAT
(- Sigma) |^ ((2 * B2) + 2) is V28() real ext-real Element of REAL
K235(((2 * B2) + 2),(- Sigma)) is Relation-like NAT -defined Function-like V34() V41((2 * B2) + 2) V42() V43() V59() set
K436(K235(((2 * B2) + 2),(- Sigma))) is V28() set
(- Sigma) |^ 2 is V28() real ext-real Element of REAL
K235(2,(- Sigma)) is Relation-like NAT -defined Function-like V34() V41(2) V42() V43() V59() set
K436(K235(2,(- Sigma))) is V28() set
((- Sigma) |^ (2 * B2)) * ((- Sigma) |^ 2) is V28() real ext-real Element of REAL
(- Sigma) * (- Sigma) is V28() real ext-real Element of REAL
Sigma |^ (Omega + 2) is V28() real ext-real Element of REAL
K235((Omega + 2),Sigma) is Relation-like NAT -defined Function-like V34() V41(Omega + 2) V42() V43() V59() set
K436(K235((Omega + 2),Sigma)) is V28() set
(- Sigma) |^ (Omega + 1) is V28() real ext-real Element of REAL
K235((Omega + 1),(- Sigma)) is Relation-like NAT -defined Function-like V34() V41(Omega + 1) V42() V43() V59() set
K436(K235((Omega + 1),(- Sigma))) is V28() set
(Sigma |^ (Omega + 2)) / ((- Sigma) |^ (Omega + 1)) is V28() real ext-real Element of COMPLEX
(Omega + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real positive non negative V70() V71() V72() V73() V74() V75() Element of NAT
Sigma |^ ((Omega + 1) + 1) is V28() real ext-real Element of REAL
K235(((Omega + 1) + 1),Sigma) is Relation-like NAT -defined Function-like V34() V41((Omega + 1) + 1) V42() V43() V59() set
K436(K235(((Omega + 1) + 1),Sigma)) is V28() set
Sigma |^ (Omega + 1) is V28() real ext-real Element of REAL
K235((Omega + 1),Sigma) is Relation-like NAT -defined Function-like V34() V41(Omega + 1) V42() V43() V59() set
K436(K235((Omega + 1),Sigma)) is V28() set
(Sigma |^ (Omega + 1)) * Sigma is V28() real ext-real Element of REAL
Sigma * ((- Sigma) |^ (Omega + 1)) is V28() real ext-real Element of REAL
((- Sigma) |^ (Omega + 1)) " is V28() real ext-real Element of REAL
(Sigma * ((- Sigma) |^ (Omega + 1))) * (((- Sigma) |^ (Omega + 1)) ") is V28() real ext-real Element of REAL
((- Sigma) |^ (Omega + 1)) * (((- Sigma) |^ (Omega + 1)) ") is V28() real ext-real Element of REAL
Sigma * (((- Sigma) |^ (Omega + 1)) * (((- Sigma) |^ (Omega + 1)) ")) is V28() real ext-real Element of REAL
((- Sigma) |^ (Omega + 1)) / ((- Sigma) |^ (Omega + 1)) is V28() real ext-real Element of COMPLEX
(Omega + 2) ! is non empty epsilon-transitive epsilon-connected ordinal natural V28() real ext-real positive non negative Element of REAL
Prod_real_n . (Omega + 2) is V28() real ext-real Element of REAL
K234((Omega + 2)) is Relation-like NAT -defined RAT -valued Function-like V34() V41(Omega + 2) V42() V43() V59() V60() V61() V62() set
K436(K234((Omega + 2))) is V28() set
(Omega + 1) ! is non empty epsilon-transitive epsilon-connected ordinal natural V28() real ext-real positive non negative Element of REAL
Prod_real_n . (Omega + 1) is V28() real ext-real Element of REAL
K234((Omega + 1)) is Relation-like NAT -defined RAT -valued Function-like V34() V41(Omega + 1) V42() V43() V59() V60() V61() V62() set
K436(K234((Omega + 1))) is V28() set
((Omega + 2) !) / ((Omega + 1) !) is non empty V28() real ext-real positive non negative Element of COMPLEX
(Omega + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real positive non negative V70() V71() V72() V73() V74() V75() Element of NAT
((Omega + 1) + 1) * ((Omega + 1) !) is non empty epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real positive non negative V70() V71() V72() V73() V74() V75() Element of NAT
((Omega + 1) !) " is non empty V28() real ext-real positive non negative Element of REAL
((Omega + 2) !) * (((Omega + 1) !) ") is non empty V28() real ext-real positive non negative Element of REAL
((Omega + 1) !) * (((Omega + 1) !) ") is non empty V28() real ext-real positive non negative Element of REAL
((Omega + 1) + 1) * (((Omega + 1) !) * (((Omega + 1) !) ")) is non empty V28() real ext-real positive non negative Element of REAL
((Omega + 1) !) / ((Omega + 1) !) is non empty V28() real ext-real positive non negative Element of COMPLEX
((Omega + 1) + 1) * 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real positive non negative V70() V71() V72() V73() V74() V75() Element of NAT
((- Sigma) |^ (Omega + 1)) " is V28() real ext-real Element of REAL
(Sigma |^ (Omega + 2)) * (((- Sigma) |^ (Omega + 1)) ") is V28() real ext-real Element of REAL
((Omega + 1) !) " is non empty V28() real ext-real positive non negative Element of REAL
(((Omega + 1) !) ") * ((Omega + 2) !) is non empty V28() real ext-real positive non negative Element of REAL
(Sigma |^ (Omega + 2)) / ((Omega + 2) !) is V28() real ext-real Element of COMPLEX
(((Omega + 1) !) ") / (((- Sigma) |^ (Omega + 1)) ") is V28() real ext-real Element of COMPLEX
(((Omega + 1) !) ") * 1 is non empty V28() real ext-real positive non negative Element of REAL
1 / ((Omega + 1) !) is non empty V28() real ext-real positive non negative Element of COMPLEX
(((- Sigma) |^ (Omega + 1)) ") " is V28() real ext-real Element of REAL
(1 / ((Omega + 1) !)) * ((((- Sigma) |^ (Omega + 1)) ") ") is V28() real ext-real Element of REAL
1 * (((Omega + 1) !) ") is non empty V28() real ext-real positive non negative Element of REAL
((- Sigma) |^ (Omega + 1)) / ((Omega + 1) !) is V28() real ext-real Element of COMPLEX
Sigma rExpSeq is non empty Relation-like NAT -defined REAL -valued Function-like V17( NAT ) V18( NAT , REAL ) V59() V60() V61() Element of bool [:NAT,REAL:]
(Sigma rExpSeq) . (Omega + 2) is V28() real ext-real Element of REAL
((Sigma rExpSeq) . (Omega + 2)) - (((- Sigma) rExpSeq) . (Omega + 1)) is V28() real ext-real Element of REAL
(((- Sigma) rExpSeq) . (Omega + 1)) - (((- Sigma) rExpSeq) . (Omega + 1)) is V28() real ext-real Element of REAL
- (((Sigma rExpSeq) . (Omega + 2)) - (((- Sigma) rExpSeq) . (Omega + 1))) is V28() real ext-real Element of REAL
- ((Sigma rExpSeq) . (Omega + 2)) is V28() real ext-real Element of REAL
2 * 0 is empty Relation-like non-empty empty-yielding RAT -valued functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() real V30() V31() V42() V44() ext-real non positive non negative V59() V60() V61() V62() V70() V71() V72() V73() V74() V75() V76() even Element of NAT
(2 * 0) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real positive non negative V70() V71() V72() V73() V74() V75() non even Element of NAT
(- Sigma) |^ ((2 * 0) + 1) is V28() real ext-real Element of REAL
K235(((2 * 0) + 1),(- Sigma)) is Relation-like NAT -defined Function-like V34() V41((2 * 0) + 1) V42() V43() V59() set
K436(K235(((2 * 0) + 1),(- Sigma))) is V28() set
Sigma |^ ((2 * 0) + 1) is V28() real ext-real Element of REAL
K235(((2 * 0) + 1),Sigma) is Relation-like NAT -defined Function-like V34() V41((2 * 0) + 1) V42() V43() V59() set
K436(K235(((2 * 0) + 1),Sigma)) is V28() set
- (Sigma |^ ((2 * 0) + 1)) is V28() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 * n is epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real non negative V70() V71() V72() V73() V74() V75() even Element of NAT
(2 * n) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real positive non negative V70() V71() V72() V73() V74() V75() non even Element of NAT
Sigma |^ ((2 * n) + 1) is V28() real ext-real Element of REAL
K235(((2 * n) + 1),Sigma) is Relation-like NAT -defined Function-like V34() V41((2 * n) + 1) V42() V43() V59() set
K436(K235(((2 * n) + 1),Sigma)) is V28() set
- (Sigma |^ ((2 * n) + 1)) is V28() real ext-real Element of REAL
(- Sigma) |^ ((2 * n) + 1) is V28() real ext-real Element of REAL
K235(((2 * n) + 1),(- Sigma)) is Relation-like NAT -defined Function-like V34() V41((2 * n) + 1) V42() V43() V59() set
K436(K235(((2 * n) + 1),(- Sigma))) is V28() set
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real positive non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 * (n + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real positive non negative V70() V71() V72() V73() V74() V75() even Element of NAT
(2 * (n + 1)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real positive non negative V70() V71() V72() V73() V74() V75() non even Element of NAT
Sigma |^ ((2 * (n + 1)) + 1) is V28() real ext-real Element of REAL
K235(((2 * (n + 1)) + 1),Sigma) is Relation-like NAT -defined Function-like V34() V41((2 * (n + 1)) + 1) V42() V43() V59() set
K436(K235(((2 * (n + 1)) + 1),Sigma)) is V28() set
- (Sigma |^ ((2 * (n + 1)) + 1)) is V28() real ext-real Element of REAL
(- Sigma) |^ ((2 * (n + 1)) + 1) is V28() real ext-real Element of REAL
K235(((2 * (n + 1)) + 1),(- Sigma)) is Relation-like NAT -defined Function-like V34() V41((2 * (n + 1)) + 1) V42() V43() V59() set
K436(K235(((2 * (n + 1)) + 1),(- Sigma))) is V28() set
((2 * n) + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real positive non negative V70() V71() V72() V73() V74() V75() even Element of NAT
Sigma |^ (((2 * n) + 1) + 1) is V28() real ext-real Element of REAL
K235((((2 * n) + 1) + 1),Sigma) is Relation-like NAT -defined Function-like V34() V41(((2 * n) + 1) + 1) V42() V43() V59() set
K436(K235((((2 * n) + 1) + 1),Sigma)) is V28() set
(Sigma |^ (((2 * n) + 1) + 1)) * Sigma is V28() real ext-real Element of REAL
- ((Sigma |^ (((2 * n) + 1) + 1)) * Sigma) is V28() real ext-real Element of REAL
(Sigma |^ ((2 * n) + 1)) * Sigma is V28() real ext-real Element of REAL
((Sigma |^ ((2 * n) + 1)) * Sigma) * Sigma is V28() real ext-real Element of REAL
- (((Sigma |^ ((2 * n) + 1)) * Sigma) * Sigma) is V28() real ext-real Element of REAL
((- Sigma) |^ ((2 * n) + 1)) * (- Sigma) is V28() real ext-real Element of REAL
(((- Sigma) |^ ((2 * n) + 1)) * (- Sigma)) * (- Sigma) is V28() real ext-real Element of REAL
(- Sigma) |^ (((2 * n) + 1) + 1) is V28() real ext-real Element of REAL
K235((((2 * n) + 1) + 1),(- Sigma)) is Relation-like NAT -defined Function-like V34() V41(((2 * n) + 1) + 1) V42() V43() V59() set
K436(K235((((2 * n) + 1) + 1),(- Sigma))) is V28() set
((- Sigma) |^ (((2 * n) + 1) + 1)) * (- Sigma) is V28() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 * n is epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real non negative V70() V71() V72() V73() V74() V75() even Element of NAT
(2 * n) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real positive non negative V70() V71() V72() V73() V74() V75() non even Element of NAT
- (Sigma |^ (Omega + 2)) is V28() real ext-real Element of REAL
(- Sigma) |^ (Omega + 2) is V28() real ext-real Element of REAL
K235((Omega + 2),(- Sigma)) is Relation-like NAT -defined Function-like V34() V41(Omega + 2) V42() V43() V59() set
K436(K235((Omega + 2),(- Sigma))) is V28() set
- ((Sigma |^ (Omega + 2)) / ((Omega + 2) !)) is V28() real ext-real Element of COMPLEX
((Omega + 2) !) " is non empty V28() real ext-real positive non negative Element of REAL
(Sigma |^ (Omega + 2)) * (((Omega + 2) !) ") is V28() real ext-real Element of REAL
- ((Sigma |^ (Omega + 2)) * (((Omega + 2) !) ")) is V28() real ext-real Element of REAL
(- (Sigma |^ (Omega + 2))) * (((Omega + 2) !) ") is V28() real ext-real Element of REAL
(- (Sigma |^ (Omega + 2))) / ((Omega + 2) !) is V28() real ext-real Element of COMPLEX
Omega is V28() real ext-real Element of REAL
1 + Omega is V28() real ext-real Element of REAL
exp_R . Omega is V28() real ext-real Element of REAL
NAT --> (1 + Omega) is non empty Relation-like NAT -defined REAL -valued Function-like constant V17( NAT ) V18( NAT , REAL ) T-Sequence-like V59() V60() V61() convergent Element of bool [:NAT,REAL:]
Omega rExpSeq is non empty Relation-like NAT -defined REAL -valued Function-like V17( NAT ) V18( NAT , REAL ) V59() V60() V61() Element of bool [:NAT,REAL:]
Partial_Sums (Omega rExpSeq) is non empty Relation-like NAT -defined REAL -valued Function-like V17( NAT ) V18( NAT , REAL ) V59() V60() V61() Element of bool [:NAT,REAL:]
Prob is epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
(NAT --> (1 + Omega)) . Prob is V28() real ext-real Element of REAL
Prob + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real positive non negative V70() V71() V72() V73() V74() V75() Element of NAT
(Partial_Sums (Omega rExpSeq)) . (Prob + 1) is V28() real ext-real Element of REAL
(Partial_Sums (Omega rExpSeq)) . 1 is V28() real ext-real Element of REAL
(Partial_Sums (Omega rExpSeq)) . 0 is V28() real ext-real Element of REAL
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real positive non negative V70() V71() V72() V73() V74() V75() Element of NAT
(Omega rExpSeq) . (0 + 1) is V28() real ext-real Element of REAL
((Partial_Sums (Omega rExpSeq)) . 0) + ((Omega rExpSeq) . (0 + 1)) is V28() real ext-real Element of REAL
(Omega rExpSeq) . 0 is V28() real ext-real Element of REAL
(Omega rExpSeq) . 1 is V28() real ext-real Element of REAL
((Omega rExpSeq) . 0) + ((Omega rExpSeq) . 1) is V28() real ext-real Element of REAL
Omega |^ 0 is V28() real ext-real Element of REAL
K235(0,Omega) is Relation-like NAT -defined Function-like V34() V41( 0 ) V42() V43() V59() set
K436(K235(0,Omega)) is V28() set
(Omega |^ 0) / (0 !) is V28() real ext-real Element of COMPLEX
Omega |^ 1 is V28() real ext-real Element of REAL
K235(1,Omega) is Relation-like NAT -defined Function-like V34() V41(1) V42() V43() V59() set
K436(K235(1,Omega)) is V28() set
(Omega |^ 1) / (1 !) is V28() real ext-real Element of COMPLEX
(NAT --> (1 + Omega)) . 0 is V28() real ext-real set
1 + 0 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real positive non negative V70() V71() V72() V73() V74() V75() Element of NAT
(Partial_Sums (Omega rExpSeq)) . (1 + 0) is V28() real ext-real Element of REAL
A is epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
(NAT --> (1 + Omega)) . A is V28() real ext-real set
1 + A is non empty epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real positive non negative V70() V71() V72() V73() V74() V75() Element of NAT
(Partial_Sums (Omega rExpSeq)) . (1 + A) is V28() real ext-real Element of REAL
A + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real positive non negative V70() V71() V72() V73() V74() V75() Element of NAT
(NAT --> (1 + Omega)) . (A + 1) is V28() real ext-real set
1 + (A + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real positive non negative V70() V71() V72() V73() V74() V75() Element of NAT
(Partial_Sums (Omega rExpSeq)) . (1 + (A + 1)) is V28() real ext-real Element of REAL
(Partial_Sums (Omega rExpSeq)) . (A + 1) is V28() real ext-real Element of REAL
(A + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real positive non negative V70() V71() V72() V73() V74() V75() Element of NAT
(Omega rExpSeq) . ((A + 1) + 1) is V28() real ext-real Element of REAL
((Partial_Sums (Omega rExpSeq)) . (A + 1)) + ((Omega rExpSeq) . ((A + 1) + 1)) is V28() real ext-real Element of REAL
Omega |^ ((A + 1) + 1) is V28() real ext-real Element of REAL
K235(((A + 1) + 1),Omega) is Relation-like NAT -defined Function-like V34() V41((A + 1) + 1) V42() V43() V59() set
K436(K235(((A + 1) + 1),Omega)) is V28() set
((A + 1) + 1) ! is non empty epsilon-transitive epsilon-connected ordinal natural V28() real ext-real positive non negative Element of REAL
Prod_real_n . ((A + 1) + 1) is V28() real ext-real Element of REAL
K234(((A + 1) + 1)) is Relation-like NAT -defined RAT -valued Function-like V34() V41((A + 1) + 1) V42() V43() V59() V60() V61() V62() set
K436(K234(((A + 1) + 1))) is V28() set
(Omega |^ ((A + 1) + 1)) / (((A + 1) + 1) !) is V28() real ext-real Element of COMPLEX
((Omega rExpSeq) . ((A + 1) + 1)) + ((Partial_Sums (Omega rExpSeq)) . (A + 1)) is V28() real ext-real Element of REAL
(Partial_Sums (Omega rExpSeq)) ^\ 1 is non empty Relation-like NAT -defined REAL -valued Function-like V17( NAT ) V18( NAT , REAL ) V59() V60() V61() M16( REAL , Partial_Sums (Omega rExpSeq))
Prob is epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
(NAT --> (1 + Omega)) . Prob is V28() real ext-real Element of REAL
((Partial_Sums (Omega rExpSeq)) ^\ 1) . Prob is V28() real ext-real Element of REAL
Prob + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real positive non negative V70() V71() V72() V73() V74() V75() Element of NAT
(Partial_Sums (Omega rExpSeq)) . (Prob + 1) is V28() real ext-real Element of REAL
lim (NAT --> (1 + Omega)) is V28() real ext-real Element of REAL
(NAT --> (1 + Omega)) . 1 is V28() real ext-real Element of REAL
lim ((Partial_Sums (Omega rExpSeq)) ^\ 1) is V28() real ext-real Element of REAL
lim (Partial_Sums (Omega rExpSeq)) is V28() real ext-real Element of REAL
Sum (Omega rExpSeq) is V28() real ext-real Element of REAL
- Omega is V28() real ext-real Element of REAL
1 - (- Omega) is V28() real ext-real Element of REAL
- (- Omega) is V28() real ext-real Element of REAL
exp_R . (- (- Omega)) is V28() real ext-real Element of REAL
Prob is V28() real ext-real Element of REAL
1 - Prob is V28() real ext-real Element of REAL
- Prob is V28() real ext-real Element of REAL
exp_R . (- Prob) is V28() real ext-real Element of REAL
NAT --> (1 - Prob) is non empty Relation-like NAT -defined REAL -valued Function-like constant V17( NAT ) V18( NAT , REAL ) T-Sequence-like V59() V60() V61() convergent Element of bool [:NAT,REAL:]
(- Prob) rExpSeq is non empty Relation-like NAT -defined REAL -valued Function-like V17( NAT ) V18( NAT , REAL ) V59() V60() V61() Element of bool [:NAT,REAL:]
Partial_Sums ((- Prob) rExpSeq) is non empty Relation-like NAT -defined REAL -valued Function-like V17( NAT ) V18( NAT , REAL ) V59() V60() V61() Element of bool [:NAT,REAL:]
n is epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
(NAT --> (1 - Prob)) . n is V28() real ext-real Element of REAL
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real positive non negative V70() V71() V72() V73() V74() V75() Element of NAT
(Partial_Sums ((- Prob) rExpSeq)) . (n + 1) is V28() real ext-real Element of REAL
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real positive non negative V70() V71() V72() V73() V74() V75() Element of NAT
(Partial_Sums ((- Prob) rExpSeq)) . (0 + 1) is V28() real ext-real Element of REAL
(Partial_Sums ((- Prob) rExpSeq)) . 0 is V28() real ext-real Element of REAL
((- Prob) rExpSeq) . 1 is V28() real ext-real Element of REAL
((Partial_Sums ((- Prob) rExpSeq)) . 0) + (((- Prob) rExpSeq) . 1) is V28() real ext-real Element of REAL
((- Prob) rExpSeq) . 0 is V28() real ext-real Element of REAL
(((- Prob) rExpSeq) . 0) + (((- Prob) rExpSeq) . 1) is V28() real ext-real Element of REAL
(- Prob) |^ 1 is V28() real ext-real Element of REAL
K235(1,(- Prob)) is Relation-like NAT -defined Function-like V34() V41(1) V42() V43() V59() set
K436(K235(1,(- Prob))) is V28() set
((- Prob) |^ 1) / (1 !) is V28() real ext-real Element of COMPLEX
(- Prob) |^ 0 is V28() real ext-real Element of REAL
K235(0,(- Prob)) is Relation-like NAT -defined Function-like V34() V41( 0 ) V42() V43() V59() set
K436(K235(0,(- Prob))) is V28() set
((- Prob) |^ 0) / (0 !) is V28() real ext-real Element of COMPLEX
(NAT --> (1 - Prob)) . 0 is V28() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
(NAT --> (1 - Prob)) . n is V28() real ext-real Element of REAL
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real positive non negative V70() V71() V72() V73() V74() V75() Element of NAT
(Partial_Sums ((- Prob) rExpSeq)) . (n + 1) is V28() real ext-real Element of REAL
(NAT --> (1 - Prob)) . (n + 1) is V28() real ext-real Element of REAL
(n + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real positive non negative V70() V71() V72() V73() V74() V75() Element of NAT
(Partial_Sums ((- Prob) rExpSeq)) . ((n + 1) + 1) is V28() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 * k is epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real non negative V70() V71() V72() V73() V74() V75() even Element of NAT
B2 is epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
c₉ is V28() real ext-real Element of REAL
c₉ rExpSeq is non empty Relation-like NAT -defined REAL -valued Function-like V17( NAT ) V18( NAT , REAL ) V59() V60() V61() Element of bool [:NAT,REAL:]
(c₉ rExpSeq) . B2 is V28() real ext-real Element of REAL
c₉ |^ B2 is V28() real ext-real Element of REAL
K235(B2,c₉) is Relation-like NAT -defined Function-like V34() V41(B2) V42() V43() V59() set
K436(K235(B2,c₉)) is V28() set
B2 ! is non empty epsilon-transitive epsilon-connected ordinal natural V28() real ext-real positive non negative Element of REAL
Prod_real_n . B2 is V28() real ext-real Element of REAL
K234(B2) is Relation-like NAT -defined RAT -valued Function-like V34() V41(B2) V42() V43() V59() V60() V61() V62() set
K436(K234(B2)) is V28() set
(c₉ |^ B2) / (B2 !) is V28() real ext-real Element of COMPLEX
c₉ |^ B2 is V28() real ext-real Element of REAL
K235(B2,c₉) is Relation-like NAT -defined Function-like V34() V41(B2) V42() V43() V59() set
K436(K235(B2,c₉)) is V28() set
B2 ! is non empty epsilon-transitive epsilon-connected ordinal natural V28() real ext-real positive non negative Element of REAL
Prod_real_n . B2 is V28() real ext-real Element of REAL
K234(B2) is Relation-like NAT -defined RAT -valued Function-like V34() V41(B2) V42() V43() V59() V60() V61() V62() set
K436(K234(B2)) is V28() set
(c₉ |^ B2) / (B2 !) is V28() real ext-real Element of COMPLEX
k is epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 * k is epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real non negative V70() V71() V72() V73() V74() V75() even Element of NAT
c₉ |^ B2 is V28() real ext-real Element of REAL
K235(B2,c₉) is Relation-like NAT -defined Function-like V34() V41(B2) V42() V43() V59() set
K436(K235(B2,c₉)) is V28() set
k + k is epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
c₉ |^ (k + k) is V28() real ext-real Element of REAL
K235((k + k),c₉) is Relation-like NAT -defined Function-like V34() V41(k + k) V42() V43() V59() set
K436(K235((k + k),c₉)) is V28() set
c₉ |^ k is V28() real ext-real Element of REAL
K235(k,c₉) is Relation-like NAT -defined Function-like V34() V41(k) V42() V43() V59() set
K436(K235(k,c₉)) is V28() set
(c₉ |^ k) * (c₉ |^ k) is V28() real ext-real Element of REAL
c₉ * c₉ is V28() real ext-real Element of REAL
(c₉ * c₉) |^ k is V28() real ext-real Element of REAL
K235(k,(c₉ * c₉)) is Relation-like NAT -defined Function-like V34() V41(k) V42() V43() V59() set
K436(K235(k,(c₉ * c₉))) is V28() set
B2 ! is non empty epsilon-transitive epsilon-connected ordinal natural V28() real ext-real positive non negative Element of REAL
Prod_real_n . B2 is V28() real ext-real Element of REAL
K234(B2) is Relation-like NAT -defined RAT -valued Function-like V34() V41(B2) V42() V43() V59() V60() V61() V62() set
K436(K234(B2)) is V28() set
(c₉ |^ B2) / (B2 !) is V28() real ext-real Element of COMPLEX
n + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real positive non negative V70() V71() V72() V73() V74() V75() Element of NAT
((- Prob) rExpSeq) . (n + 2) is V28() real ext-real Element of REAL
((Partial_Sums ((- Prob) rExpSeq)) . (n + 1)) + (((- Prob) rExpSeq) . (n + 2)) is V28() real ext-real Element of REAL
((- Prob) rExpSeq) . ((n + 1) + 1) is V28() real ext-real Element of REAL
((Partial_Sums ((- Prob) rExpSeq)) . (n + 1)) + (((- Prob) rExpSeq) . ((n + 1) + 1)) is V28() real ext-real Element of REAL
(Partial_Sums ((- Prob) rExpSeq)) . (n + 2) is V28() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 * k is epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real non negative V70() V71() V72() V73() V74() V75() even Element of NAT
(2 * k) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real positive non negative V70() V71() V72() V73() V74() V75() non even Element of NAT
B2 is epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
c₉ is V28() real ext-real Element of REAL
1 - c₉ is V28() real ext-real Element of REAL
- c₉ is V28() real ext-real Element of REAL
(- c₉) rExpSeq is non empty Relation-like NAT -defined REAL -valued Function-like V17( NAT ) V18( NAT , REAL ) V59() V60() V61() Element of bool [:NAT,REAL:]
Partial_Sums ((- c₉) rExpSeq) is non empty Relation-like NAT -defined REAL -valued Function-like V17( NAT ) V18( NAT , REAL ) V59() V60() V61() Element of bool [:NAT,REAL:]
(Partial_Sums ((- c₉) rExpSeq)) . B2 is V28() real ext-real Element of REAL
2 * 0 is empty Relation-like non-empty empty-yielding RAT -valued functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() real V30() V31() V42() V44() ext-real non positive non negative V59() V60() V61() V62() V70() V71() V72() V73() V74() V75() V76() even Element of NAT
(2 * 0) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real positive non negative V70() V71() V72() V73() V74() V75() non even Element of NAT
(Partial_Sums ((- c₉) rExpSeq)) . ((2 * 0) + 1) is V28() real ext-real Element of REAL
(Partial_Sums ((- c₉) rExpSeq)) . 0 is V28() real ext-real Element of REAL
((- c₉) rExpSeq) . 1 is V28() real ext-real Element of REAL
((Partial_Sums ((- c₉) rExpSeq)) . 0) + (((- c₉) rExpSeq) . 1) is V28() real ext-real Element of REAL
((- c₉) rExpSeq) . 0 is V28() real ext-real Element of REAL
(((- c₉) rExpSeq) . 0) + (((- c₉) rExpSeq) . 1) is V28() real ext-real Element of REAL
(- c₉) |^ 0 is V28() real ext-real Element of REAL
K235(0,(- c₉)) is Relation-like NAT -defined Function-like V34() V41( 0 ) V42() V43() V59() set
K436(K235(0,(- c₉))) is V28() set
((- c₉) |^ 0) / (0 !) is V28() real ext-real Element of COMPLEX
(- c₉) |^ 1 is V28() real ext-real Element of REAL
K235(1,(- c₉)) is Relation-like NAT -defined Function-like V34() V41(1) V42() V43() V59() set
K436(K235(1,(- c₉))) is V28() set
((- c₉) |^ 1) / (1 !) is V28() real ext-real Element of COMPLEX
1 + 0 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real positive non negative V70() V71() V72() V73() V74() V75() Element of NAT
((- c₉) rExpSeq) . (1 + 0) is V28() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 * k is epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real non negative V70() V71() V72() V73() V74() V75() even Element of NAT
(2 * k) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real positive non negative V70() V71() V72() V73() V74() V75() non even Element of NAT
(Partial_Sums ((- c₉) rExpSeq)) . ((2 * k) + 1) is V28() real ext-real Element of REAL
k + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real positive non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 * (k + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real positive non negative V70() V71() V72() V73() V74() V75() even Element of NAT
(2 * (k + 1)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real positive non negative V70() V71() V72() V73() V74() V75() non even Element of NAT
(Partial_Sums ((- c₉) rExpSeq)) . ((2 * (k + 1)) + 1) is V28() real ext-real Element of REAL
(2 * k) + 3 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real positive non negative V70() V71() V72() V73() V74() V75() Element of NAT
(Partial_Sums ((- c₉) rExpSeq)) . ((2 * k) + 3) is V28() real ext-real Element of REAL
(2 * k) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real positive non negative V70() V71() V72() V73() V74() V75() even Element of NAT
(Partial_Sums ((- c₉) rExpSeq)) . ((2 * k) + 2) is V28() real ext-real Element of REAL
((2 * k) + 2) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real positive non negative V70() V71() V72() V73() V74() V75() non even Element of NAT
((- c₉) rExpSeq) . (((2 * k) + 2) + 1) is V28() real ext-real Element of REAL
((Partial_Sums ((- c₉) rExpSeq)) . ((2 * k) + 2)) + (((- c₉) rExpSeq) . (((2 * k) + 2) + 1)) is V28() real ext-real Element of REAL
((2 * k) + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real positive non negative V70() V71() V72() V73() V74() V75() even Element of NAT
(Partial_Sums ((- c₉) rExpSeq)) . (((2 * k) + 1) + 1) is V28() real ext-real Element of REAL
((- c₉) rExpSeq) . ((2 * k) + 3) is V28() real ext-real Element of REAL
((Partial_Sums ((- c₉) rExpSeq)) . (((2 * k) + 1) + 1)) + (((- c₉) rExpSeq) . ((2 * k) + 3)) is V28() real ext-real Element of REAL
((- c₉) rExpSeq) . ((2 * k) + 2) is V28() real ext-real Element of REAL
((Partial_Sums ((- c₉) rExpSeq)) . ((2 * k) + 1)) + (((- c₉) rExpSeq) . ((2 * k) + 2)) is V28() real ext-real Element of REAL
(((Partial_Sums ((- c₉) rExpSeq)) . ((2 * k) + 1)) + (((- c₉) rExpSeq) . ((2 * k) + 2))) + (((- c₉) rExpSeq) . ((2 * k) + 3)) is V28() real ext-real Element of REAL
(((- c₉) rExpSeq) . ((2 * k) + 2)) + (((- c₉) rExpSeq) . ((2 * k) + 3)) is V28() real ext-real Element of REAL
((Partial_Sums ((- c₉) rExpSeq)) . ((2 * k) + 1)) + ((((- c₉) rExpSeq) . ((2 * k) + 2)) + (((- c₉) rExpSeq) . ((2 * k) + 3))) is V28() real ext-real Element of REAL
((- c₉) rExpSeq) . (((2 * k) + 1) + 1) is V28() real ext-real Element of REAL
((2 * k) + 1) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real positive non negative V70() V71() V72() V73() V74() V75() non even Element of NAT
((- c₉) rExpSeq) . (((2 * k) + 1) + 2) is V28() real ext-real Element of REAL
(((- c₉) rExpSeq) . (((2 * k) + 1) + 1)) + (((- c₉) rExpSeq) . (((2 * k) + 1) + 2)) is V28() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
2 * k is epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real non negative V70() V71() V72() V73() V74() V75() even Element of NAT
(2 * k) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real positive non negative V70() V71() V72() V73() V74() V75() non even Element of NAT
n + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real positive non negative V70() V71() V72() V73() V74() V75() Element of NAT
(Partial_Sums ((- Prob) rExpSeq)) . (n + 2) is V28() real ext-real Element of REAL
(Partial_Sums ((- Prob) rExpSeq)) ^\ 1 is non empty Relation-like NAT -defined REAL -valued Function-like V17( NAT ) V18( NAT , REAL ) V59() V60() V61() M16( REAL , Partial_Sums ((- Prob) rExpSeq))
n is epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
(NAT --> (1 - Prob)) . n is V28() real ext-real Element of REAL
((Partial_Sums ((- Prob) rExpSeq)) ^\ 1) . n is V28() real ext-real Element of REAL
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real positive non negative V70() V71() V72() V73() V74() V75() Element of NAT
(Partial_Sums ((- Prob) rExpSeq)) . (n + 1) is V28() real ext-real Element of REAL
lim (NAT --> (1 - Prob)) is V28() real ext-real Element of REAL
(NAT --> (1 - Prob)) . 1 is V28() real ext-real Element of REAL
lim ((Partial_Sums ((- Prob) rExpSeq)) ^\ 1) is V28() real ext-real Element of REAL
lim (Partial_Sums ((- Prob) rExpSeq)) is V28() real ext-real Element of REAL
Sum ((- Prob) rExpSeq) is V28() real ext-real Element of REAL
Omega is non empty Relation-like NAT -defined REAL -valued Function-like V17( NAT ) V18( NAT , REAL ) V59() V60() V61() Element of bool [:NAT,REAL:]
Sigma is non empty Relation-like NAT -defined REAL -valued Function-like V17( NAT ) V18( NAT , REAL ) V59() V60() V61() Element of bool [:NAT,REAL:]
Prob is epsilon-transitive epsilon-connected ordinal natural V28() real ext-real non negative set
Sigma . Prob is V28() real ext-real set
Omega . Prob is V28() real ext-real set
- (Omega . Prob) is V28() real ext-real set
(- (Omega . Prob)) rExpSeq is non empty Relation-like NAT -defined REAL -valued Function-like V17( NAT ) V18( NAT , REAL ) V59() V60() V61() Element of bool [:NAT,REAL:]
Sum ((- (Omega . Prob)) rExpSeq) is V28() real ext-real Element of REAL
Sigma is non empty Relation-like NAT -defined REAL -valued Function-like V17( NAT ) V18( NAT , REAL ) V59() V60() V61() Element of bool [:NAT,REAL:]
Prob is non empty Relation-like NAT -defined REAL -valued Function-like V17( NAT ) V18( NAT , REAL ) V59() V60() V61() Element of bool [:NAT,REAL:]
A is epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
Sigma . A is V28() real ext-real set
Prob . A is V28() real ext-real set
Sigma . A is V28() real ext-real Element of REAL
Omega . A is V28() real ext-real Element of REAL
- (Omega . A) is V28() real ext-real Element of REAL
(- (Omega . A)) rExpSeq is non empty Relation-like NAT -defined REAL -valued Function-like V17( NAT ) V18( NAT , REAL ) V59() V60() V61() Element of bool [:NAT,REAL:]
Sum ((- (Omega . A)) rExpSeq) is V28() real ext-real Element of REAL
Omega is non empty set
bool Omega is non empty V94() set
bool (bool Omega) is non empty V94() set
K496(Omega) is non empty V94() Element of bool (bool Omega)
[:NAT,K496(Omega):] is non empty Relation-like set
bool [:NAT,K496(Omega):] is non empty V94() set
Sigma is non empty compl-closed sigma-multiplicative Element of bool (bool Omega)
Prob is non empty Relation-like Sigma -defined REAL -valued Function-like V17(Sigma) V18(Sigma, REAL ) V59() V60() V61() Probability of Sigma
A is non empty Relation-like NAT -defined K496(Omega) -valued Sigma -valued Function-like V17( NAT ) V18( NAT ,K496(Omega)) Element of bool [:NAT,K496(Omega):]
Prob * A is non empty Relation-like NAT -defined REAL -valued Function-like V17( NAT ) V18( NAT , REAL ) V59() V60() V61() Element of bool [:NAT,REAL:]
((Prob * A)) is non empty Relation-like NAT -defined REAL -valued Function-like V17( NAT ) V18( NAT , REAL ) V59() V60() V61() Element of bool [:NAT,REAL:]
Partial_Product ((Prob * A)) is non empty Relation-like NAT -defined REAL -valued Function-like V17( NAT ) V18( NAT , REAL ) V59() V60() V61() Element of bool [:NAT,REAL:]
Partial_Sums (Prob * A) is non empty Relation-like NAT -defined REAL -valued Function-like V17( NAT ) V18( NAT , REAL ) V59() V60() V61() Element of bool [:NAT,REAL:]
n is epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
(Partial_Product ((Prob * A))) . n is V28() real ext-real Element of REAL
(Partial_Sums (Prob * A)) . n is V28() real ext-real Element of REAL
- ((Partial_Sums (Prob * A)) . n) is V28() real ext-real Element of REAL
exp_R . (- ((Partial_Sums (Prob * A)) . n)) is V28() real ext-real Element of REAL
(Partial_Sums (Prob * A)) . 0 is V28() real ext-real Element of REAL
- ((Partial_Sums (Prob * A)) . 0) is V28() real ext-real Element of REAL
exp_R . (- ((Partial_Sums (Prob * A)) . 0)) is V28() real ext-real Element of REAL
(Prob * A) . 0 is V28() real ext-real Element of REAL
- ((Prob * A) . 0) is V28() real ext-real Element of REAL
exp_R . (- ((Prob * A) . 0)) is V28() real ext-real Element of REAL
(Partial_Product ((Prob * A))) . 0 is V28() real ext-real Element of REAL
((Prob * A)) . 0 is V28() real ext-real Element of REAL
(- ((Prob * A) . 0)) rExpSeq is non empty Relation-like NAT -defined REAL -valued Function-like V17( NAT ) V18( NAT , REAL ) V59() V60() V61() Element of bool [:NAT,REAL:]
Sum ((- ((Prob * A) . 0)) rExpSeq) is V28() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
(Partial_Sums (Prob * A)) . n is V28() real ext-real Element of REAL
- ((Partial_Sums (Prob * A)) . n) is V28() real ext-real Element of REAL
exp_R . (- ((Partial_Sums (Prob * A)) . n)) is V28() real ext-real Element of REAL
(Partial_Product ((Prob * A))) . n is V28() real ext-real Element of REAL
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real positive non negative V70() V71() V72() V73() V74() V75() Element of NAT
(Partial_Sums (Prob * A)) . (n + 1) is V28() real ext-real Element of REAL
- ((Partial_Sums (Prob * A)) . (n + 1)) is V28() real ext-real Element of REAL
exp_R . (- ((Partial_Sums (Prob * A)) . (n + 1))) is V28() real ext-real Element of REAL
(Partial_Product ((Prob * A))) . (n + 1) is V28() real ext-real Element of REAL
((Prob * A)) . (n + 1) is V28() real ext-real Element of REAL
((Partial_Product ((Prob * A))) . n) * (((Prob * A)) . (n + 1)) is V28() real ext-real Element of REAL
(Prob * A) . (n + 1) is V28() real ext-real Element of REAL
- ((Prob * A) . (n + 1)) is V28() real ext-real Element of REAL
(- ((Prob * A) . (n + 1))) rExpSeq is non empty Relation-like NAT -defined REAL -valued Function-like V17( NAT ) V18( NAT , REAL ) V59() V60() V61() Element of bool [:NAT,REAL:]
Sum ((- ((Prob * A) . (n + 1))) rExpSeq) is V28() real ext-real Element of REAL
(exp_R . (- ((Partial_Sums (Prob * A)) . n))) * (Sum ((- ((Prob * A) . (n + 1))) rExpSeq)) is V28() real ext-real Element of REAL
exp_R (- ((Partial_Sums (Prob * A)) . n)) is V28() real ext-real Element of REAL
exp_R . (- ((Partial_Sums (Prob * A)) . n)) is V28() real ext-real Element of REAL
exp_R (- ((Prob * A) . (n + 1))) is V28() real ext-real Element of REAL
exp_R . (- ((Prob * A) . (n + 1))) is V28() real ext-real Element of REAL
(exp_R (- ((Partial_Sums (Prob * A)) . n))) * (exp_R (- ((Prob * A) . (n + 1)))) is V28() real ext-real Element of REAL
(- ((Partial_Sums (Prob * A)) . n)) + (- ((Prob * A) . (n + 1))) is V28() real ext-real Element of REAL
exp_R ((- ((Partial_Sums (Prob * A)) . n)) + (- ((Prob * A) . (n + 1)))) is V28() real ext-real Element of REAL
exp_R . ((- ((Partial_Sums (Prob * A)) . n)) + (- ((Prob * A) . (n + 1)))) is V28() real ext-real Element of REAL
((Partial_Sums (Prob * A)) . n) + ((Prob * A) . (n + 1)) is V28() real ext-real Element of REAL
- (((Partial_Sums (Prob * A)) . n) + ((Prob * A) . (n + 1))) is V28() real ext-real Element of REAL
Omega is non empty set
bool Omega is non empty V94() set
bool (bool Omega) is non empty V94() set
K496(Omega) is non empty V94() Element of bool (bool Omega)
[:NAT,K496(Omega):] is non empty Relation-like set
bool [:NAT,K496(Omega):] is non empty V94() set
Sigma is non empty compl-closed sigma-multiplicative Element of bool (bool Omega)
Prob is non empty Relation-like Sigma -defined REAL -valued Function-like V17(Sigma) V18(Sigma, REAL ) V59() V60() V61() Probability of Sigma
A is non empty Relation-like NAT -defined K496(Omega) -valued Sigma -valued Function-like V17( NAT ) V18( NAT ,K496(Omega)) Element of bool [:NAT,K496(Omega):]
Complement A is non empty Relation-like NAT -defined K496(Omega) -valued Function-like V17( NAT ) V18( NAT ,K496(Omega)) Element of bool [:NAT,K496(Omega):]
Prob * (Complement A) is non empty Relation-like NAT -defined REAL -valued Function-like V17( NAT ) V18( NAT , REAL ) V59() V60() V61() Element of bool [:NAT,REAL:]
Partial_Product (Prob * (Complement A)) is non empty Relation-like NAT -defined REAL -valued Function-like V17( NAT ) V18( NAT , REAL ) V59() V60() V61() Element of bool [:NAT,REAL:]
Prob * A is non empty Relation-like NAT -defined REAL -valued Function-like V17( NAT ) V18( NAT , REAL ) V59() V60() V61() Element of bool [:NAT,REAL:]
((Prob * A)) is non empty Relation-like NAT -defined REAL -valued Function-like V17( NAT ) V18( NAT , REAL ) V59() V60() V61() Element of bool [:NAT,REAL:]
Partial_Product ((Prob * A)) is non empty Relation-like NAT -defined REAL -valued Function-like V17( NAT ) V18( NAT , REAL ) V59() V60() V61() Element of bool [:NAT,REAL:]
n is epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
(Partial_Product (Prob * (Complement A))) . n is V28() real ext-real Element of REAL
(Partial_Product ((Prob * A))) . n is V28() real ext-real Element of REAL
(Partial_Product (Prob * (Complement A))) . 0 is V28() real ext-real Element of REAL
(Prob * (Complement A)) . 0 is V28() real ext-real Element of REAL
dom (Prob * (Complement A)) is non empty V70() V71() V72() V73() V74() V75() Element of bool NAT
(Complement A) . 0 is Event of Sigma
Prob . ((Complement A) . 0) is V28() real ext-real Element of REAL
A . 0 is Event of Sigma
(A . 0) ` is Element of bool Omega
Prob . ((A . 0) `) is V28() real ext-real set
[#] Sigma is Event of Sigma
([#] Sigma) \ (A . 0) is Event of Sigma
Prob . (([#] Sigma) \ (A . 0)) is V28() real ext-real Element of REAL
Prob . (A . 0) is V28() real ext-real Element of REAL
1 - (Prob . (A . 0)) is V28() real ext-real Element of REAL
(Partial_Product ((Prob * A))) . 0 is V28() real ext-real Element of REAL
((Prob * A)) . 0 is V28() real ext-real Element of REAL
(Prob * A) . 0 is V28() real ext-real Element of REAL
- ((Prob * A) . 0) is V28() real ext-real Element of REAL
(- ((Prob * A) . 0)) rExpSeq is non empty Relation-like NAT -defined REAL -valued Function-like V17( NAT ) V18( NAT , REAL ) V59() V60() V61() Element of bool [:NAT,REAL:]
Sum ((- ((Prob * A) . 0)) rExpSeq) is V28() real ext-real Element of REAL
exp_R . (- ((Prob * A) . 0)) is V28() real ext-real Element of REAL
dom (Prob * A) is non empty V70() V71() V72() V73() V74() V75() Element of bool NAT
- (Prob . (A . 0)) is V28() real ext-real Element of REAL
1 + (- (Prob . (A . 0))) is V28() real ext-real Element of REAL
exp_R . (- (Prob . (A . 0))) is V28() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
(Partial_Product (Prob * (Complement A))) . n is V28() real ext-real Element of REAL
(Partial_Product ((Prob * A))) . n is V28() real ext-real Element of REAL
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real positive non negative V70() V71() V72() V73() V74() V75() Element of NAT
(Partial_Product (Prob * (Complement A))) . (n + 1) is V28() real ext-real Element of REAL
(Partial_Product ((Prob * A))) . (n + 1) is V28() real ext-real Element of REAL
(Complement A) . (n + 1) is Event of Sigma
Prob . ((Complement A) . (n + 1)) is V28() real ext-real Element of REAL
A . (n + 1) is Event of Sigma
(A . (n + 1)) ` is Element of bool Omega
Prob . ((A . (n + 1)) `) is V28() real ext-real set
([#] Sigma) \ (A . (n + 1)) is Event of Sigma
Prob . (A . (n + 1)) is V28() real ext-real Element of REAL
1 - (Prob . (A . (n + 1))) is V28() real ext-real Element of REAL
- (Prob . (A . (n + 1))) is V28() real ext-real Element of REAL
1 + (- (Prob . (A . (n + 1)))) is V28() real ext-real Element of REAL
exp_R . (- (Prob . (A . (n + 1)))) is V28() real ext-real Element of REAL
(Prob * (Complement A)) . (n + 1) is V28() real ext-real Element of REAL
((Prob * (Complement A)) . (n + 1)) * ((Partial_Product ((Prob * A))) . n) is V28() real ext-real Element of REAL
(exp_R . (- (Prob . (A . (n + 1))))) * ((Partial_Product ((Prob * A))) . n) is V28() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
((Prob * A)) . k is V28() real ext-real Element of REAL
(Prob * A) . k is V28() real ext-real Element of REAL
- ((Prob * A) . k) is V28() real ext-real Element of REAL
exp_R . (- ((Prob * A) . k)) is V28() real ext-real Element of REAL
(- ((Prob * A) . k)) rExpSeq is non empty Relation-like NAT -defined REAL -valued Function-like V17( NAT ) V18( NAT , REAL ) V59() V60() V61() Element of bool [:NAT,REAL:]
Sum ((- ((Prob * A) . k)) rExpSeq) is V28() real ext-real Element of REAL
((Partial_Product (Prob * (Complement A))) . n) * ((Prob * (Complement A)) . (n + 1)) is V28() real ext-real Element of REAL
((Partial_Product ((Prob * A))) . n) * ((Prob * (Complement A)) . (n + 1)) is V28() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V28() real V30() V31() ext-real non negative V70() V71() V72() V73() V74() V75() Element of NAT
(Prob * (Complement A)) . k is V28() real ext-real Element of REAL
(Complement A) . k is Event of Sigma
Prob . ((Complement A) . k) is V28() real ext-real Element of REAL
(- (Prob . (A . (n + 1)))) rExpSeq is non empty Relation-like NAT -defined REAL -valued Function-like V17( NAT ) V18( NAT , REAL ) V59() V60() V61() Element of bool [:NAT,REAL:]
Sum ((- (Prob . (A . (n + 1)))) rExpSeq) is V28() real ext-real Element of REAL
(Sum ((- (Prob . (A . (n + 1)))) rExpSeq)) * ((Partial_Product ((Prob * A))) . n) is V28() real ext-real Element of REAL
Partial_Sums (Prob * A) is non empty Relation-like NAT -defined REAL -valued Function-like V17( NAT ) V18( NAT , REAL ) V59() V60() V61() Element of bool [:NAT,REAL:]
(Partial_Sums (Prob * A)) . n is V28() real ext-real Element of REAL
- ((Partial_Sums (Prob * A)) . n) is V28() real ext-real Element of REAL
exp_R . (- ((Partial_Sums (Prob * A)) . n)) is V28() real ext-real Element of REAL
(Sum ((- (Prob . (A . (n + 1)))) rExpSeq)) * (exp_R . (- ((Partial_Sums (Prob * A)) . n))) is V28() real ext-real Element of REAL
exp_R (- (Prob . (A . (n + 1)))) is V28() real ext-real Element of REAL
exp_R . (- (Prob . (A . (n + 1)))) is V28() real ext-real