REAL is non empty V2() non finite set
NAT is non empty V2() V4() V5() V6() non finite cardinal limit_cardinal Element of K6(REAL)
K6(REAL) is non empty V2() non finite set
COMPLEX is non empty V2() non finite set
RAT is non empty V2() non finite set
INT is non empty V2() non finite set
NAT is non empty V2() V4() V5() V6() non finite cardinal limit_cardinal set
K6(NAT) is non empty V2() non finite set
K6(NAT) is non empty V2() non finite set
K7(REAL,REAL) is non empty V2() Relation-like non finite set
K6(K7(REAL,REAL)) is non empty V2() non finite set
K7(COMPLEX,COMPLEX) is non empty V2() Relation-like non finite set
K6(K7(COMPLEX,COMPLEX)) is non empty V2() non finite set
K7(K7(COMPLEX,COMPLEX),COMPLEX) is non empty V2() Relation-like non finite set
K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is non empty V2() non finite set
K7(K7(REAL,REAL),REAL) is non empty V2() Relation-like non finite set
K6(K7(K7(REAL,REAL),REAL)) is non empty V2() non finite set
K7(RAT,RAT) is non empty V2() Relation-like non finite set
K6(K7(RAT,RAT)) is non empty V2() non finite set
K7(K7(RAT,RAT),RAT) is non empty V2() Relation-like non finite set
K6(K7(K7(RAT,RAT),RAT)) is non empty V2() non finite set
K7(INT,INT) is non empty V2() Relation-like non finite set
K6(K7(INT,INT)) is non empty V2() non finite set
K7(K7(INT,INT),INT) is non empty V2() Relation-like non finite set
K6(K7(K7(INT,INT),INT)) is non empty V2() non finite set
K7(NAT,NAT) is non empty V2() Relation-like non finite set
K7(K7(NAT,NAT),NAT) is non empty V2() Relation-like non finite set
K6(K7(K7(NAT,NAT),NAT)) is non empty V2() non finite set
{} is empty V4() V5() V6() V8() V9() V10() Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional finite finite-yielding V25() V33() ext-real non positive non negative V37() V40() V41() V42() V43() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set
the empty V4() V5() V6() V8() V9() V10() Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional finite finite-yielding V25() V33() ext-real non positive non negative V37() V40() V41() V42() V43() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set is empty V4() V5() V6() V8() V9() V10() Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional finite finite-yielding V25() V33() ext-real non positive non negative V37() V40() V41() V42() V43() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set
1 is non empty V4() V5() V6() V10() finite V33() ext-real positive non negative V37() cardinal Element of NAT
{{},1} is non empty finite V25() set
K7(NAT,REAL) is non empty V2() Relation-like non finite set
K6(K7(NAT,REAL)) is non empty V2() non finite set
K6(K6(REAL)) is non empty V2() non finite set
2 is non empty V4() V5() V6() V10() finite V33() ext-real positive non negative V37() cardinal Element of NAT
K222(1,NAT) is M10( NAT )
REAL * is non empty functional FinSequence-membered M10( REAL )
3 is non empty V4() V5() V6() V10() finite V33() ext-real positive non negative V37() cardinal Element of NAT
0 is empty V4() V5() V6() V8() V9() V10() Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional finite finite-yielding V25() V33() ext-real non positive non negative V37() V40() V41() V42() V43() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Element of NAT
<*> REAL is empty proper V4() V5() V6() V8() V9() V10() Relation-like non-empty empty-yielding NAT -defined REAL -valued RAT -valued Function-like one-to-one constant functional finite finite-yielding V25() V33() ext-real non positive non negative V37() V40() V41() V42() V43() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of REAL
Sum (<*> REAL) is V33() ext-real V37() Element of REAL
S is set
S is set
p is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S
dom p is finite V55() set
p " S is finite Element of K6(NAT)
rng p is finite Element of K6(S)
K6(S) is non empty set
p " (rng p) is finite Element of K6(NAT)
S is set
S is set
p is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S
s is set
Coim (p,s) is set
{s} is non empty V2() finite 1 -element set
p " {s} is finite set
dom p is finite V55() set
K6((dom p)) is non empty finite V25() set
S is finite set
p is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S
s is set
(S,p,s) is finite Element of K6((dom p))
dom p is finite V55() set
K6((dom p)) is non empty finite V25() set
{s} is non empty V2() finite 1 -element set
p " {s} is finite set
card (S,p,s) is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
S is set
p is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S
dom p is finite V55() set
s is set
p " S is finite Element of K6(NAT)
p . s is set
t is Element of S
(S,p,t) is finite Element of K6((dom p))
K6((dom p)) is non empty finite V25() set
{t} is non empty V2() finite 1 -element set
p " {t} is finite set
S is set
p is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S
dom p is finite V55() set
card (dom p) is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
len p is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
Seg (len p) is finite len p -element Element of K6(NAT)
{ b1 where b1 is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT : ( 1 <= b1 & b1 <= len p ) } is set
card (Seg (len p)) is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
S is finite set
p is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S
s is set
(S,p,s) is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal set
(S,p,s) is finite Element of K6((dom p))
dom p is finite V55() set
K6((dom p)) is non empty finite V25() set
{s} is non empty V2() finite 1 -element set
p " {s} is finite set
card (S,p,s) is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
len p is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
(S,p,s) / (len p) is V33() ext-real non negative V37() Element of REAL
S is finite set
p is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S
len p is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
s is set
(S,p,s) is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal set
(S,p,s) is finite Element of K6((dom p))
dom p is finite V55() set
K6((dom p)) is non empty finite V25() set
{s} is non empty V2() finite 1 -element set
p " {s} is finite set
card (S,p,s) is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
(S,p,s) is V33() ext-real V37() Element of REAL
(S,p,s) / (len p) is V33() ext-real non negative V37() Element of REAL
(len p) * (S,p,s) is V33() ext-real V37() Element of REAL
S is finite set
card S is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
Seg (card S) is finite card S -element Element of K6(NAT)
{ b1 where b1 is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT : ( 1 <= b1 & b1 <= card S ) } is set
p is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S
canFS S is Relation-like NAT -defined S -valued Function-like one-to-one finite V31(S) FinSequence-like FinSubsequence-like FinSequence of S
s is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal set
(canFS S) . s is set
(S,p,((canFS S) . s)) is V33() ext-real V37() Element of REAL
(S,p,((canFS S) . s)) is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal set
(S,p,((canFS S) . s)) is finite Element of K6((dom p))
dom p is finite V55() set
K6((dom p)) is non empty finite V25() set
{((canFS S) . s)} is non empty V2() finite 1 -element set
p " {((canFS S) . s)} is finite set
card (S,p,((canFS S) . s)) is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
len p is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
(S,p,((canFS S) . s)) / (len p) is V33() ext-real non negative V37() Element of REAL
s is Relation-like NAT -defined REAL -valued Function-like finite V40() V41() V42() FinSequence-like FinSubsequence-like FinSequence of REAL
dom s is finite V55() Element of K6(NAT)
t is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal set
s . t is V33() ext-real V37() set
(canFS S) . t is set
(S,p,((canFS S) . t)) is V33() ext-real V37() Element of REAL
(S,p,((canFS S) . t)) is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal set
(S,p,((canFS S) . t)) is finite Element of K6((dom p))
dom p is finite V55() set
K6((dom p)) is non empty finite V25() set
{((canFS S) . t)} is non empty V2() finite 1 -element set
p " {((canFS S) . t)} is finite set
card (S,p,((canFS S) . t)) is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
len p is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
(S,p,((canFS S) . t)) / (len p) is V33() ext-real non negative V37() Element of REAL
s is Relation-like NAT -defined REAL -valued Function-like finite V40() V41() V42() FinSequence-like FinSubsequence-like FinSequence of REAL
dom s is finite V55() Element of K6(NAT)
t is Relation-like NAT -defined REAL -valued Function-like finite V40() V41() V42() FinSequence-like FinSubsequence-like FinSequence of REAL
dom t is finite V55() Element of K6(NAT)
s is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal set
s . s is V33() ext-real V37() set
(canFS S) . s is set
(S,p,((canFS S) . s)) is V33() ext-real V37() Element of REAL
(S,p,((canFS S) . s)) is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal set
(S,p,((canFS S) . s)) is finite Element of K6((dom p))
dom p is finite V55() set
K6((dom p)) is non empty finite V25() set
{((canFS S) . s)} is non empty V2() finite 1 -element set
p " {((canFS S) . s)} is finite set
card (S,p,((canFS S) . s)) is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
len p is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
(S,p,((canFS S) . s)) / (len p) is V33() ext-real non negative V37() Element of REAL
t . s is V33() ext-real V37() set
len s is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
len t is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
S is finite set
p is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S
s is set
(S,p,s) is V33() ext-real V37() Element of REAL
(S,p,s) is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal set
(S,p,s) is finite Element of K6((dom p))
dom p is finite V55() set
K6((dom p)) is non empty finite V25() set
{s} is non empty V2() finite 1 -element set
p " {s} is finite set
card (S,p,s) is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
len p is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
(S,p,s) / (len p) is V33() ext-real non negative V37() Element of REAL
prob (S,p,s) is V33() ext-real V37() Element of REAL
card (dom p) is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
K103((card (S,p,s)),(card (dom p))) is V33() ext-real non negative V37() set
S is finite set
t is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S
s is set
(S,t,s) is V33() ext-real V37() Element of REAL
(S,t,s) is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal set
(S,t,s) is finite Element of K6((dom t))
dom t is finite V55() set
K6((dom t)) is non empty finite V25() set
{s} is non empty V2() finite 1 -element set
t " {s} is finite set
card (S,t,s) is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
len t is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
(S,t,s) / (len t) is V33() ext-real non negative V37() Element of REAL
t is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S
s is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S
nb is set
(S,s,nb) is V33() ext-real V37() Element of REAL
(S,s,nb) is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal set
(S,s,nb) is finite Element of K6((dom s))
dom s is finite V55() set
K6((dom s)) is non empty finite V25() set
{nb} is non empty V2() finite 1 -element set
s " {nb} is finite set
card (S,s,nb) is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
len s is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
(S,s,nb) / (len s) is V33() ext-real non negative V37() Element of REAL
(S,t,nb) is V33() ext-real V37() Element of REAL
(S,t,nb) is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal set
(S,t,nb) is finite Element of K6((dom t))
dom t is finite V55() set
K6((dom t)) is non empty finite V25() set
t " {nb} is finite set
card (S,t,nb) is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
len t is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
(S,t,nb) / (len t) is V33() ext-real non negative V37() Element of REAL
S is finite set
p is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S
s is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S
t is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S
s is set
(S,p,s) is V33() ext-real V37() Element of REAL
(S,p,s) is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal set
(S,p,s) is finite Element of K6((dom p))
dom p is finite V55() set
K6((dom p)) is non empty finite V25() set
{s} is non empty V2() finite 1 -element set
p " {s} is finite set
card (S,p,s) is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
len p is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
(S,p,s) / (len p) is V33() ext-real non negative V37() Element of REAL
(S,t,s) is V33() ext-real V37() Element of REAL
(S,t,s) is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal set
(S,t,s) is finite Element of K6((dom t))
dom t is finite V55() set
K6((dom t)) is non empty finite V25() set
t " {s} is finite set
card (S,t,s) is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
len t is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
(S,t,s) / (len t) is V33() ext-real non negative V37() Element of REAL
(S,s,s) is V33() ext-real V37() Element of REAL
(S,s,s) is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal set
(S,s,s) is finite Element of K6((dom s))
dom s is finite V55() set
K6((dom s)) is non empty finite V25() set
s " {s} is finite set
card (S,s,s) is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
len s is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
(S,s,s) / (len s) is V33() ext-real non negative V37() Element of REAL
S is finite set
p is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S
{ b1 where b1 is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S : (S,p,b1) } is set
S * is non empty functional FinSequence-membered M10(S)
K6((S *)) is non empty set
s is set
t is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S
S is finite set
p is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S
(S,p) is functional FinSequence-membered Element of K6((S *))
S * is non empty functional FinSequence-membered M10(S)
K6((S *)) is non empty set
{ b1 where b1 is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S : (S,p,b1) } is set
S is finite set
p is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S
s is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S
(S,p) is non empty functional FinSequence-membered Element of K6((S *))
S * is non empty functional FinSequence-membered M10(S)
K6((S *)) is non empty set
{ b1 where b1 is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S : (S,p,b1) } is set
t is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S
S is finite set
p is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S
(S,p) is non empty functional FinSequence-membered Element of K6((S *))
S * is non empty functional FinSequence-membered M10(S)
K6((S *)) is non empty set
{ b1 where b1 is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S : (S,p,b1) } is set
S is finite set
p is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S
s is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S
(S,p) is non empty functional FinSequence-membered Element of K6((S *))
S * is non empty functional FinSequence-membered M10(S)
K6((S *)) is non empty set
{ b1 where b1 is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S : (S,p,b1) } is set
(S,s) is non empty functional FinSequence-membered Element of K6((S *))
{ b1 where b1 is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S : (S,s,b1) } is set
t is set
s is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S
t is set
s is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S
S is finite set
S * is non empty functional FinSequence-membered M10(S)
K6((S *)) is non empty set
K6(K6((S *))) is non empty set
p is Element of K6(K6((S *)))
p is Element of K6(K6((S *)))
s is Element of K6(K6((S *)))
S is finite set
(S) is Element of K6(K6((S *)))
S * is non empty functional FinSequence-membered M10(S)
K6((S *)) is non empty set
K6(K6((S *))) is non empty set
the Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like Element of S * is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like Element of S *
(S, the Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like Element of S * ) is non empty functional FinSequence-membered Element of K6((S *))
{ b1 where b1 is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S : (S, the Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like Element of S * ,b1) } is set
S is finite set
p is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S
s is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S
(S,p) is Relation-like NAT -defined REAL -valued Function-like finite V40() V41() V42() FinSequence-like FinSubsequence-like FinSequence of REAL
(S,s) is Relation-like NAT -defined REAL -valued Function-like finite V40() V41() V42() FinSequence-like FinSubsequence-like FinSequence of REAL
t is set
(S,s,t) is V33() ext-real V37() Element of REAL
(S,s,t) is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal set
(S,s,t) is finite Element of K6((dom s))
dom s is finite V55() set
K6((dom s)) is non empty finite V25() set
{t} is non empty V2() finite 1 -element set
s " {t} is finite set
card (S,s,t) is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
len s is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
(S,s,t) / (len s) is V33() ext-real non negative V37() Element of REAL
(S,p,t) is V33() ext-real V37() Element of REAL
(S,p,t) is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal set
(S,p,t) is finite Element of K6((dom p))
dom p is finite V55() set
K6((dom p)) is non empty finite V25() set
p " {t} is finite set
card (S,p,t) is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
len p is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
(S,p,t) / (len p) is V33() ext-real non negative V37() Element of REAL
canFS S is Relation-like NAT -defined S -valued Function-like one-to-one finite V31(S) FinSequence-like FinSubsequence-like FinSequence of S
rng (canFS S) is finite Element of K6(S)
K6(S) is non empty finite V25() set
dom (canFS S) is finite V55() Element of K6(NAT)
s is set
(canFS S) . s is set
len (canFS S) is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
card S is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
nb is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
Seg (card S) is finite card S -element Element of K6(NAT)
{ b1 where b1 is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT : ( 1 <= b1 & b1 <= card S ) } is set
dom (S,s) is finite V55() Element of K6(NAT)
dom (S,p) is finite V55() Element of K6(NAT)
(S,p) . nb is V33() ext-real V37() set
rng s is finite Element of K6(S)
K6(S) is non empty finite V25() set
s " {t} is finite Element of K6(NAT)
rng p is finite Element of K6(S)
p " {t} is finite Element of K6(NAT)
t is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal set
dom (S,s) is finite V55() Element of K6(NAT)
(S,s) . t is V33() ext-real V37() set
canFS S is Relation-like NAT -defined S -valued Function-like one-to-one finite V31(S) FinSequence-like FinSubsequence-like FinSequence of S
(canFS S) . t is set
(S,s,((canFS S) . t)) is V33() ext-real V37() Element of REAL
(S,s,((canFS S) . t)) is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal set
(S,s,((canFS S) . t)) is finite Element of K6((dom s))
dom s is finite V55() set
K6((dom s)) is non empty finite V25() set
{((canFS S) . t)} is non empty V2() finite 1 -element set
s " {((canFS S) . t)} is finite set
card (S,s,((canFS S) . t)) is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
len s is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
(S,s,((canFS S) . t)) / (len s) is V33() ext-real non negative V37() Element of REAL
(S,p,((canFS S) . t)) is V33() ext-real V37() Element of REAL
(S,p,((canFS S) . t)) is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal set
(S,p,((canFS S) . t)) is finite Element of K6((dom p))
dom p is finite V55() set
K6((dom p)) is non empty finite V25() set
p " {((canFS S) . t)} is finite set
card (S,p,((canFS S) . t)) is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
len p is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
(S,p,((canFS S) . t)) / (len p) is V33() ext-real non negative V37() Element of REAL
card S is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
Seg (card S) is finite card S -element Element of K6(NAT)
{ b1 where b1 is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT : ( 1 <= b1 & b1 <= card S ) } is set
S is finite set
s is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S
p is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S
(S,p) is non empty functional FinSequence-membered Element of K6((S *))
S * is non empty functional FinSequence-membered M10(S)
K6((S *)) is non empty set
{ b1 where b1 is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S : (S,p,b1) } is set
(S,p) is Relation-like NAT -defined REAL -valued Function-like finite V40() V41() V42() FinSequence-like FinSubsequence-like FinSequence of REAL
(S,s) is Relation-like NAT -defined REAL -valued Function-like finite V40() V41() V42() FinSequence-like FinSubsequence-like FinSequence of REAL
t is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S
S is finite set
(S) is non empty Element of K6(K6((S *)))
S * is non empty functional FinSequence-membered M10(S)
K6((S *)) is non empty set
K6(K6((S *))) is non empty set
K7((S),(REAL *)) is non empty Relation-like set
K6(K7((S),(REAL *))) is non empty set
p is Element of (S)
s is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S
(S,s) is non empty functional FinSequence-membered Element of K6((S *))
{ b1 where b1 is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S : (S,s,b1) } is set
(S,s) is Relation-like NAT -defined REAL -valued Function-like finite V40() V41() V42() FinSequence-like FinSubsequence-like FinSequence of REAL
p is Relation-like Function-like V30((S),REAL * ) Element of K6(K7((S),(REAL *)))
s is Element of (S)
p . s is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of REAL *
p is Relation-like Function-like V30((S),REAL * ) Element of K6(K7((S),(REAL *)))
s is Relation-like Function-like V30((S),REAL * ) Element of K6(K7((S),(REAL *)))
t is Element of (S)
s is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S
(S,s) is non empty functional FinSequence-membered Element of K6((S *))
{ b1 where b1 is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S : (S,s,b1) } is set
s . t is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of REAL *
nb is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S
(S,nb) is Relation-like NAT -defined REAL -valued Function-like finite V40() V41() V42() FinSequence-like FinSubsequence-like FinSequence of REAL
p . t is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of REAL *
j is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S
(S,j) is Relation-like NAT -defined REAL -valued Function-like finite V40() V41() V42() FinSequence-like FinSubsequence-like FinSequence of REAL
S is finite set
(S) is Relation-like Function-like V30((S),REAL * ) Element of K6(K7((S),(REAL *)))
(S) is non empty Element of K6(K6((S *)))
S * is non empty functional FinSequence-membered M10(S)
K6((S *)) is non empty set
K6(K6((S *))) is non empty set
K7((S),(REAL *)) is non empty Relation-like set
K6(K7((S),(REAL *))) is non empty set
p is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S
(S,p) is non empty functional FinSequence-membered Element of K6((S *))
{ b1 where b1 is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S : (S,p,b1) } is set
(S) . (S,p) is set
(S,p) is Relation-like NAT -defined REAL -valued Function-like finite V40() V41() V42() FinSequence-like FinSubsequence-like FinSequence of REAL
s is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S
(S,s) is Relation-like NAT -defined REAL -valued Function-like finite V40() V41() V42() FinSequence-like FinSubsequence-like FinSequence of REAL
S is finite set
(S) is Relation-like Function-like V30((S),REAL * ) Element of K6(K7((S),(REAL *)))
(S) is non empty Element of K6(K6((S *)))
S * is non empty functional FinSequence-membered M10(S)
K6((S *)) is non empty set
K6(K6((S *))) is non empty set
K7((S),(REAL *)) is non empty Relation-like set
K6(K7((S),(REAL *))) is non empty set
p is set
s is set
(S) . p is set
(S) . s is set
t is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S
(S,t) is non empty functional FinSequence-membered Element of K6((S *))
{ b1 where b1 is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S : (S,t,b1) } is set
s is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S
(S,s) is non empty functional FinSequence-membered Element of K6((S *))
{ b1 where b1 is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S : (S,s,b1) } is set
nb is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S
(S,nb) is Relation-like NAT -defined REAL -valued Function-like finite V40() V41() V42() FinSequence-like FinSubsequence-like FinSequence of REAL
j is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S
(S,j) is Relation-like NAT -defined REAL -valued Function-like finite V40() V41() V42() FinSequence-like FinSubsequence-like FinSequence of REAL
S is finite set
p is non empty Relation-like NAT -defined REAL -valued Function-like finite V40() V41() V42() FinSequence-like FinSubsequence-like V70() ProbFinS FinSequence of REAL
S * is non empty functional FinSequence-membered M10(S)
K6((S *)) is non empty set
(S) is non empty Element of K6(K6((S *)))
K6(K6((S *))) is non empty set
(S) is Relation-like Function-like one-to-one V30((S),REAL * ) Element of K6(K7((S),(REAL *)))
K7((S),(REAL *)) is non empty Relation-like set
K6(K7((S),(REAL *))) is non empty set
s is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S
(S,s) is Relation-like NAT -defined REAL -valued Function-like finite V40() V41() V42() FinSequence-like FinSubsequence-like FinSequence of REAL
s is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S
(S,s) is Relation-like NAT -defined REAL -valued Function-like finite V40() V41() V42() FinSequence-like FinSubsequence-like FinSequence of REAL
(S,s) is non empty functional FinSequence-membered Element of K6((S *))
{ b1 where b1 is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S : (S,s,b1) } is set
t is Element of (S)
(S) . t is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of REAL *
s is Element of (S)
(S) . s is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of REAL *
t is Element of (S)
(S) . t is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of REAL *
dom (S) is set
S is finite set
card S is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
Seg (card S) is finite card S -element Element of K6(NAT)
{ b1 where b1 is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT : ( 1 <= b1 & b1 <= card S ) } is set
p is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S
len p is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
(S,p) is Relation-like NAT -defined REAL -valued Function-like finite V40() V41() V42() FinSequence-like FinSubsequence-like FinSequence of REAL
canFS S is Relation-like NAT -defined S -valued Function-like one-to-one finite V31(S) FinSequence-like FinSubsequence-like FinSequence of S
rng (canFS S) is finite Element of K6(S)
K6(S) is non empty finite V25() set
s is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal set
(S,p) . s is V33() ext-real V37() set
(len p) * ((S,p) . s) is V33() ext-real V37() Element of REAL
len (canFS S) is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
Seg (len (canFS S)) is finite len (canFS S) -element Element of K6(NAT)
{ b1 where b1 is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT : ( 1 <= b1 & b1 <= len (canFS S) ) } is set
dom (canFS S) is finite V55() Element of K6(NAT)
(canFS S) . s is set
t is Element of S
dom (S,p) is finite V55() Element of K6(NAT)
(S,p,t) is V33() ext-real V37() Element of REAL
(S,p,t) is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal set
(S,p,t) is finite Element of K6((dom p))
dom p is finite V55() set
K6((dom p)) is non empty finite V25() set
{t} is non empty V2() finite 1 -element set
p " {t} is finite set
card (S,p,t) is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
(S,p,t) / (len p) is V33() ext-real non negative V37() Element of REAL
(len p) * (S,p,t) is V33() ext-real V37() Element of REAL
s is Relation-like NAT -defined NAT -valued Function-like finite V40() V41() V42() V43() FinSequence-like FinSubsequence-like FinSequence of NAT
dom s is finite V55() Element of K6(NAT)
t is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal set
s . t is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal set
(S,p) . t is V33() ext-real V37() set
(len p) * ((S,p) . t) is V33() ext-real V37() Element of REAL
s is Relation-like NAT -defined NAT -valued Function-like finite V40() V41() V42() V43() FinSequence-like FinSubsequence-like FinSequence of NAT
dom s is finite V55() Element of K6(NAT)
t is Relation-like NAT -defined NAT -valued Function-like finite V40() V41() V42() V43() FinSequence-like FinSubsequence-like FinSequence of NAT
dom t is finite V55() Element of K6(NAT)
s is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal set
s . s is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal set
(S,p) . s is V33() ext-real V37() set
(len p) * ((S,p) . s) is V33() ext-real V37() Element of REAL
t . s is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal set
len s is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
len t is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
S is non empty finite set
card S is non empty V4() V5() V6() V10() finite V33() ext-real positive non negative V37() cardinal Element of NAT
Seg (card S) is non empty finite card S -element Element of K6(NAT)
{ b1 where b1 is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT : ( 1 <= b1 & b1 <= card S ) } is set
canFS S is non empty Relation-like NAT -defined S -valued Function-like one-to-one finite V31(S) FinSequence-like FinSubsequence-like FinSequence of S
p is non empty Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S
(S,p) is Relation-like NAT -defined NAT -valued Function-like finite V40() V41() V42() V43() FinSequence-like FinSubsequence-like FinSequence of NAT
s is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal set
(S,p) . s is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal set
(canFS S) . s is set
len p is non empty V4() V5() V6() V10() finite V33() ext-real positive non negative V37() cardinal Element of NAT
(S,p) is Relation-like NAT -defined REAL -valued Function-like finite V40() V41() V42() FinSequence-like FinSubsequence-like FinSequence of REAL
(S,p) . s is V33() ext-real V37() set
(len p) * ((S,p) . s) is V33() ext-real V37() Element of REAL
rng (canFS S) is non empty finite Element of K6(S)
K6(S) is non empty finite V25() set
dom (S,p) is finite V55() Element of K6(NAT)
len (canFS S) is non empty V4() V5() V6() V10() finite V33() ext-real positive non negative V37() cardinal Element of NAT
Seg (len (canFS S)) is non empty finite len (canFS S) -element Element of K6(NAT)
{ b1 where b1 is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT : ( 1 <= b1 & b1 <= len (canFS S) ) } is set
dom (canFS S) is non empty finite V55() Element of K6(NAT)
s is Element of S
(S,p,s) is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal set
(S,p,s) is finite Element of K6((dom p))
dom p is non empty finite V55() set
K6((dom p)) is non empty finite V25() set
{s} is non empty V2() finite 1 -element set
p " {s} is finite set
card (S,p,s) is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
dom (S,p) is finite V55() Element of K6(NAT)
(S,p,s) is V33() ext-real V37() Element of REAL
(S,p,s) / (len p) is V33() ext-real non negative V37() Element of REAL
(len p) * (S,p,s) is V33() ext-real V37() Element of REAL
S is finite set
p is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S
(S,p) is Relation-like NAT -defined NAT -valued Function-like finite V40() V41() V42() V43() FinSequence-like FinSubsequence-like FinSequence of NAT
(S,p) is Relation-like NAT -defined REAL -valued Function-like finite V40() V41() V42() FinSequence-like FinSubsequence-like FinSequence of REAL
len p is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
(len p) * (S,p) is Relation-like NAT -defined REAL -valued Function-like finite V40() V41() V42() FinSequence-like FinSubsequence-like FinSequence of REAL
(len p) (#) (S,p) is Relation-like NAT -defined Function-like finite V40() V41() V42() FinSequence-like FinSubsequence-like set
dom ((len p) (#) (S,p)) is finite V55() Element of K6(NAT)
dom (S,p) is finite V55() Element of K6(NAT)
card S is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
Seg (card S) is finite card S -element Element of K6(NAT)
{ b1 where b1 is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT : ( 1 <= b1 & b1 <= card S ) } is set
dom (S,p) is finite V55() Element of K6(NAT)
s is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal set
((len p) (#) (S,p)) . s is V33() ext-real V37() set
(S,p) . s is V33() ext-real V37() set
(len p) * ((S,p) . s) is V33() ext-real V37() Element of REAL
(S,p) . s is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal set
S is finite set
p is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S
(S,p) is Relation-like NAT -defined NAT -valued Function-like finite V40() V41() V42() V43() FinSequence-like FinSubsequence-like FinSequence of NAT
Sum (S,p) is V33() set
len p is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
(S,p) is Relation-like NAT -defined REAL -valued Function-like finite V40() V41() V42() FinSequence-like FinSubsequence-like FinSequence of REAL
Sum (S,p) is V33() ext-real V37() Element of REAL
(len p) * (Sum (S,p)) is V33() ext-real V37() Element of REAL
(len p) * (S,p) is Relation-like NAT -defined REAL -valued Function-like finite V40() V41() V42() FinSequence-like FinSubsequence-like FinSequence of REAL
S is non empty finite set
canFS S is non empty Relation-like NAT -defined S -valued Function-like one-to-one finite V31(S) FinSequence-like FinSubsequence-like FinSequence of S
p is non empty Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S
dom p is non empty finite V55() Element of K6(NAT)
(S,p) is Relation-like NAT -defined NAT -valued Function-like finite V40() V41() V42() V43() FinSequence-like FinSubsequence-like FinSequence of NAT
s is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal set
p . s is set
(S,p,(p . s)) is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal set
(S,p,(p . s)) is finite Element of K6((dom p))
dom p is non empty finite V55() set
K6((dom p)) is non empty finite V25() set
{(p . s)} is non empty V2() finite 1 -element set
p " {(p . s)} is finite set
card (S,p,(p . s)) is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
rng p is non empty finite Element of K6(S)
K6(S) is non empty finite V25() set
rng (canFS S) is non empty finite Element of K6(S)
dom (canFS S) is non empty finite V55() Element of K6(NAT)
s is set
(canFS S) . s is set
nb is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal set
(S,p) . nb is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal set
(canFS S) . nb is set
len (canFS S) is non empty V4() V5() V6() V10() finite V33() ext-real positive non negative V37() cardinal Element of NAT
Seg (len (canFS S)) is non empty finite len (canFS S) -element Element of K6(NAT)
{ b1 where b1 is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT : ( 1 <= b1 & b1 <= len (canFS S) ) } is set
card S is non empty V4() V5() V6() V10() finite V33() ext-real positive non negative V37() cardinal Element of NAT
Seg (card S) is non empty finite card S -element Element of K6(NAT)
{ b1 where b1 is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT : ( 1 <= b1 & b1 <= card S ) } is set
j is Element of S
(S,p,j) is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal set
(S,p,j) is finite Element of K6((dom p))
{j} is non empty V2() finite 1 -element set
p " {j} is finite set
card (S,p,j) is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
S is Relation-like Function-like set
p is set
S | p is Relation-like Function-like set
t is set
s is set
dom (S | p) is set
(S | p) . t is set
S . t is set
(S | p) . s is set
S . s is set
dom (S | p) is set
(S | p) . t is set
(S | p) . s is set
((S | p) . t) /\ ((S | p) . s) is set
(S | p) . s is set
(S | p) . t is set
((S | p) . t) /\ ((S | p) . s) is set
(S | p) . t is set
(S | p) . s is set
(S | p) . t is set
(S | p) . s is set
dom (S | p) is set
S is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal set
p is Relation-like Function-like set
dom p is set
s is Relation-like NAT -defined NAT -valued Function-like finite V40() V41() V42() V43() FinSequence-like FinSubsequence-like FinSequence of NAT
dom s is finite V55() Element of K6(NAT)
S + 1 is non empty V4() V5() V6() V10() finite V33() ext-real positive non negative V37() cardinal Element of NAT
len s is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
Seg S is finite S -element Element of K6(NAT)
{ b1 where b1 is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT : ( 1 <= b1 & b1 <= S ) } is set
p | (Seg S) is Relation-like Function-like finite set
s | S is Relation-like NAT -defined NAT -valued Function-like finite V40() V41() V42() V43() FinSequence-like FinSubsequence-like FinSequence of NAT
s | (Seg S) is Relation-like NAT -defined Seg S -defined NAT -defined NAT -valued RAT -valued Function-like finite V40() V41() V42() V43() FinSubsequence-like set
s is Relation-like NAT -defined NAT -valued Function-like finite V40() V41() V42() V43() FinSequence-like FinSubsequence-like FinSequence of NAT
len s is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
nb is set
Union p is set
rng p is set
union (rng p) is set
j is set
nne is set
p . nne is set
Seg (S + 1) is non empty finite S + 1 -element Element of K6(NAT)
{ b1 where b1 is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT : ( 1 <= b1 & b1 <= S + 1 ) } is set
i is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
Union (p | (Seg S)) is set
rng (p | (Seg S)) is finite set
union (rng (p | (Seg S))) is set
p . (S + 1) is set
(Union (p | (Seg S))) \/ (p . (S + 1)) is set
(dom p) /\ (Seg S) is finite Element of K6(NAT)
dom (p | (Seg S)) is finite set
p . i is set
(p | (Seg S)) . i is set
rng (p | (Seg S)) is finite set
Union (p | (Seg S)) is set
union (rng (p | (Seg S))) is set
p . (S + 1) is set
(Union (p | (Seg S))) \/ (p . (S + 1)) is set
Union (p | (Seg S)) is set
rng (p | (Seg S)) is finite set
union (rng (p | (Seg S))) is set
p . (S + 1) is set
(Union (p | (Seg S))) \/ (p . (S + 1)) is set
Union (p | (Seg S)) is set
rng (p | (Seg S)) is finite set
union (rng (p | (Seg S))) is set
p . (S + 1) is set
(Union (p | (Seg S))) \/ (p . (S + 1)) is set
nb is set
j is set
dom (p | (Seg S)) is finite set
nne is set
(p | (Seg S)) . nne is set
(dom p) /\ (Seg S) is finite Element of K6(NAT)
p . nne is set
dom (p | (Seg S)) is finite set
nb is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal set
(p | (Seg S)) . nb is set
s . nb is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal set
card ((p | (Seg S)) . nb) is V4() V5() V6() cardinal set
(dom p) /\ (Seg S) is finite Element of K6(NAT)
s . nb is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal set
p . nb is set
card (p . nb) is V4() V5() V6() cardinal set
(dom p) /\ (Seg S) is finite Element of K6(NAT)
dom s is finite V55() Element of K6(NAT)
card (Union (p | (Seg S))) is V4() V5() V6() cardinal set
Sum s is V33() set
s /. (len s) is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
<*(s /. (len s))*> is non empty V2() Relation-like NAT -defined REAL -valued Function-like one-to-one constant finite V40() V41() V42() V44() V45() V46() V47() 1 -element FinSequence-like FinSubsequence-like FinSequence of REAL
[1,(s /. (len s))] is set
{1,(s /. (len s))} is non empty finite V25() set
{1} is non empty V2() finite V25() 1 -element set
{{1,(s /. (len s))},{1}} is non empty finite V25() set
{[1,(s /. (len s))]} is non empty V2() Relation-like Function-like constant finite 1 -element set
(s | S) ^ <*(s /. (len s))*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
s . (S + 1) is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal set
<*(s . (S + 1))*> is non empty V2() Relation-like NAT -defined REAL -valued Function-like one-to-one constant finite V40() V41() V42() V44() V45() V46() V47() 1 -element FinSequence-like FinSubsequence-like FinSequence of REAL
[1,(s . (S + 1))] is set
{1,(s . (S + 1))} is non empty finite V25() set
{{1,(s . (S + 1))},{1}} is non empty finite V25() set
{[1,(s . (S + 1))]} is non empty V2() Relation-like Function-like constant finite 1 -element set
s ^ <*(s . (S + 1))*> is non empty Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Seg (len s) is finite len s -element Element of K6(NAT)
{ b1 where b1 is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT : ( 1 <= b1 & b1 <= len s ) } is set
nb is finite set
j is finite set
nb \/ j is finite set
nne is set
i is set
(p | (Seg S)) . i is set
i is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
p . i is set
card ((Union (p | (Seg S))) \/ (p . (S + 1))) is V4() V5() V6() cardinal set
card nb is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
card j is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
(card nb) + (card j) is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
card (Union p) is V4() V5() V6() cardinal set
(Sum s) + (s . (S + 1)) is Element of COMPLEX
Sum s is V33() set
p is Relation-like Function-like set
dom p is set
s is Relation-like NAT -defined NAT -valued Function-like finite V40() V41() V42() V43() FinSequence-like FinSubsequence-like FinSequence of NAT
dom s is finite V55() Element of K6(NAT)
len s is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
Union p is set
rng p is set
union (rng p) is set
card (Union p) is V4() V5() V6() cardinal set
Sum s is V33() set
S is Relation-like Function-like set
dom S is set
Union S is set
rng S is set
union (rng S) is set
card (Union S) is V4() V5() V6() cardinal set
p is Relation-like NAT -defined NAT -valued Function-like finite V40() V41() V42() V43() FinSequence-like FinSubsequence-like FinSequence of NAT
dom p is finite V55() Element of K6(NAT)
len p is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
Sum p is V33() set
s is set
S is Relation-like Function-like set
dom S is set
Union S is set
rng S is set
union (rng S) is set
card (Union S) is V4() V5() V6() cardinal set
p is Relation-like NAT -defined NAT -valued Function-like finite V40() V41() V42() V43() FinSequence-like FinSubsequence-like FinSequence of NAT
dom p is finite V55() Element of K6(NAT)
Sum p is V33() set
len p is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
S is non empty finite set
p is non empty Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S
(S,p) is Relation-like NAT -defined NAT -valued Function-like finite V40() V41() V42() V43() FinSequence-like FinSubsequence-like FinSequence of NAT
Sum (S,p) is V33() set
len p is non empty V4() V5() V6() V10() finite V33() ext-real positive non negative V37() cardinal Element of NAT
canFS S is non empty Relation-like NAT -defined S -valued Function-like one-to-one finite V31(S) FinSequence-like FinSubsequence-like FinSequence of S
len (canFS S) is non empty V4() V5() V6() V10() finite V33() ext-real positive non negative V37() cardinal Element of NAT
card S is non empty V4() V5() V6() V10() finite V33() ext-real positive non negative V37() cardinal Element of NAT
dom (canFS S) is non empty finite V55() Element of K6(NAT)
Seg (card S) is non empty finite card S -element Element of K6(NAT)
{ b1 where b1 is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT : ( 1 <= b1 & b1 <= card S ) } is set
dom (S,p) is finite V55() Element of K6(NAT)
t is set
(canFS S) . t is set
rng (canFS S) is non empty finite Element of K6(S)
K6(S) is non empty finite V25() set
nb is Element of S
{nb} is non empty V2() finite 1 -element set
p " {nb} is finite Element of K6(NAT)
(S,p,nb) is finite Element of K6((dom p))
dom p is non empty finite V55() set
K6((dom p)) is non empty finite V25() set
p " {nb} is finite set
t is Relation-like Function-like set
dom t is set
s is set
nb is set
t . s is set
t . nb is set
(canFS S) . s is set
(canFS S) . nb is set
j is Element of S
(S,p,j) is finite Element of K6((dom p))
dom p is non empty finite V55() set
K6((dom p)) is non empty finite V25() set
{j} is non empty V2() finite 1 -element set
p " {j} is finite set
nne is Element of S
(S,p,nne) is finite Element of K6((dom p))
{nne} is non empty V2() finite 1 -element set
p " {nne} is finite set
s is set
nb is set
t . s is set
t . nb is set
Seg (len p) is non empty finite len p -element Element of K6(NAT)
{ b1 where b1 is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT : ( 1 <= b1 & b1 <= len p ) } is set
Union t is set
rng t is set
union (rng t) is set
s is set
p . s is set
dom p is non empty finite V55() Element of K6(NAT)
rng p is non empty finite Element of K6(S)
K6(S) is non empty finite V25() set
rng (canFS S) is non empty finite Element of K6(S)
j is Element of S
nne is set
(canFS S) . nne is set
t . nne is set
{(p . s)} is non empty V2() finite 1 -element set
i is Element of S
(S,p,i) is finite Element of K6((dom p))
dom p is non empty finite V55() set
K6((dom p)) is non empty finite V25() set
{i} is non empty V2() finite 1 -element set
p " {i} is finite set
s is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal set
t . s is set
(S,p) . s is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal set
card (t . s) is V4() V5() V6() cardinal set
(canFS S) . s is set
(S,p) is Relation-like NAT -defined REAL -valued Function-like finite V40() V41() V42() FinSequence-like FinSubsequence-like FinSequence of REAL
dom (S,p) is finite V55() Element of K6(NAT)
(S,p) . s is V33() ext-real V37() set
(len p) * ((S,p) . s) is V33() ext-real V37() Element of REAL
(S,p,((canFS S) . s)) is V33() ext-real V37() Element of REAL
(S,p,((canFS S) . s)) is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal set
(S,p,((canFS S) . s)) is finite Element of K6((dom p))
dom p is non empty finite V55() set
K6((dom p)) is non empty finite V25() set
{((canFS S) . s)} is non empty V2() finite 1 -element set
p " {((canFS S) . s)} is finite set
card (S,p,((canFS S) . s)) is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
(S,p,((canFS S) . s)) / (len p) is V33() ext-real non negative V37() Element of REAL
(len p) * (S,p,((canFS S) . s)) is V33() ext-real V37() Element of REAL
nb is Element of S
(S,p,nb) is finite Element of K6((dom p))
{nb} is non empty V2() finite 1 -element set
p " {nb} is finite set
nb is set
j is set
t . j is set
(canFS S) . j is set
dom p is non empty finite V55() set
nne is Element of S
(S,p,nne) is finite Element of K6((dom p))
K6((dom p)) is non empty finite V25() set
{nne} is non empty V2() finite 1 -element set
p " {nne} is finite set
s is finite set
card s is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
S is non empty finite set
p is non empty Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S
(S,p) is Relation-like NAT -defined REAL -valued Function-like finite V40() V41() V42() FinSequence-like FinSubsequence-like FinSequence of REAL
Sum (S,p) is V33() ext-real V37() Element of REAL
(S,p) is Relation-like NAT -defined NAT -valued Function-like finite V40() V41() V42() V43() FinSequence-like FinSubsequence-like FinSequence of NAT
Sum (S,p) is V33() set
len p is non empty V4() V5() V6() V10() finite V33() ext-real positive non negative V37() cardinal Element of NAT
(len p) * (Sum (S,p)) is V33() ext-real V37() Element of REAL
(len p) * 1 is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
S is non empty finite set
p is non empty Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S
(S,p) is Relation-like NAT -defined REAL -valued Function-like finite V40() V41() V42() FinSequence-like FinSubsequence-like FinSequence of REAL
dom (S,p) is finite V55() Element of K6(NAT)
s is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
(S,p) . s is V33() ext-real V37() set
canFS S is non empty Relation-like NAT -defined S -valued Function-like one-to-one finite V31(S) FinSequence-like FinSubsequence-like FinSequence of S
(canFS S) . s is set
(S,p,((canFS S) . s)) is V33() ext-real V37() Element of REAL
(S,p,((canFS S) . s)) is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal set
(S,p,((canFS S) . s)) is finite Element of K6((dom p))
dom p is non empty finite V55() set
K6((dom p)) is non empty finite V25() set
{((canFS S) . s)} is non empty V2() finite 1 -element set
p " {((canFS S) . s)} is finite set
card (S,p,((canFS S) . s)) is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
len p is non empty V4() V5() V6() V10() finite V33() ext-real positive non negative V37() cardinal Element of NAT
(S,p,((canFS S) . s)) / (len p) is V33() ext-real non negative V37() Element of REAL
Sum (S,p) is V33() ext-real V37() Element of REAL
S is non empty finite set
card S is non empty V4() V5() V6() V10() finite V33() ext-real positive non negative V37() cardinal Element of NAT
the Element of S is Element of S
<* the Element of S*> is non empty V2() Relation-like NAT -defined S -valued Function-like constant finite 1 -element FinSequence-like FinSubsequence-like FinSequence of S
[1, the Element of S] is set
{1, the Element of S} is non empty finite set
{1} is non empty V2() finite V25() 1 -element set
{{1, the Element of S},{1}} is non empty finite V25() set
{[1, the Element of S]} is non empty V2() Relation-like Function-like constant finite 1 -element set
(S,<* the Element of S*>) is non empty Relation-like NAT -defined REAL -valued Function-like finite V40() V41() V42() FinSequence-like FinSubsequence-like V70() ProbFinS FinSequence of REAL
dom (S,<* the Element of S*>) is non empty finite V55() Element of K6(NAT)
Seg (card S) is non empty finite card S -element Element of K6(NAT)
{ b1 where b1 is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT : ( 1 <= b1 & b1 <= card S ) } is set
len (S,<* the Element of S*>) is non empty V4() V5() V6() V10() finite V33() ext-real positive non negative V37() cardinal Element of NAT
S is non empty finite set
S * is non empty functional FinSequence-membered M10(S)
K6((S *)) is non empty set
(S) is non empty Element of K6(K6((S *)))
K6(K6((S *))) is non empty set
(S) is Relation-like Function-like one-to-one V30((S),REAL * ) Element of K6(K7((S),(REAL *)))
K7((S),(REAL *)) is non empty Relation-like set
K6(K7((S),(REAL *))) is non empty set
p is non empty Relation-like NAT -defined REAL -valued Function-like finite V40() V41() V42() FinSequence-like FinSubsequence-like V70() ProbFinS (S)
(S,p) is Element of (S)
(S) . (S,p) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of REAL *
s is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S
(S,s) is Relation-like NAT -defined REAL -valued Function-like finite V40() V41() V42() FinSequence-like FinSubsequence-like FinSequence of REAL
S is finite set
S is finite set
p is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S
(S,p) is Relation-like NAT -defined REAL -valued Function-like finite V40() V41() V42() FinSequence-like FinSubsequence-like FinSequence of REAL
s is set
dom (S,p) is finite V55() set
t is set
(S,p) . s is V33() ext-real V37() set
(S,p) . t is V33() ext-real V37() set
dom (S,p) is finite V55() Element of K6(NAT)
s is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal set
(S,p) . s is V33() ext-real V37() set
card S is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
1 / (card S) is V33() ext-real non negative V37() Element of REAL
nb is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal set
(S,p) . nb is V33() ext-real V37() set
S is finite set
p is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S
s is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S
(S,p) is Relation-like NAT -defined REAL -valued Function-like finite V40() V41() V42() FinSequence-like FinSubsequence-like FinSequence of REAL
(S,s) is Relation-like NAT -defined REAL -valued Function-like finite V40() V41() V42() FinSequence-like FinSubsequence-like FinSequence of REAL
dom (S,s) is finite V55() Element of K6(NAT)
card S is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
1 / (card S) is V33() ext-real non negative V37() Element of REAL
t is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal set
(S,s) . t is V33() ext-real V37() set
S is finite set
p is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S
s is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S
(S,p) is Relation-like NAT -defined REAL -valued Function-like finite V40() V41() V42() FinSequence-like FinSubsequence-like FinSequence of REAL
dom (S,p) is finite V55() Element of K6(NAT)
card S is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
Seg (card S) is finite card S -element Element of K6(NAT)
{ b1 where b1 is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT : ( 1 <= b1 & b1 <= card S ) } is set
(S,s) is Relation-like NAT -defined REAL -valued Function-like finite V40() V41() V42() FinSequence-like FinSubsequence-like FinSequence of REAL
dom (S,s) is finite V55() Element of K6(NAT)
t is set
(S,p) . t is V33() ext-real V37() set
(S,s) . t is V33() ext-real V37() set
1 / (card S) is V33() ext-real non negative V37() Element of REAL
S is finite set
canFS S is Relation-like NAT -defined S -valued Function-like one-to-one finite V31(S) FinSequence-like FinSubsequence-like FinSequence of S
len (canFS S) is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
card S is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
dom (canFS S) is finite V55() Element of K6(NAT)
Seg (card S) is finite card S -element Element of K6(NAT)
{ b1 where b1 is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT : ( 1 <= b1 & b1 <= card S ) } is set
(S,(canFS S)) is Relation-like NAT -defined REAL -valued Function-like finite V40() V41() V42() FinSequence-like FinSubsequence-like FinSequence of REAL
dom (S,(canFS S)) is finite V55() Element of K6(NAT)
1 / (card S) is V33() ext-real non negative V37() Element of REAL
s is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal set
(S,(canFS S)) . s is V33() ext-real V37() set
(canFS S) . s is set
(S,(canFS S),((canFS S) . s)) is V33() ext-real V37() Element of REAL
(S,(canFS S),((canFS S) . s)) is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal set
(S,(canFS S),((canFS S) . s)) is finite Element of K6((dom (canFS S)))
dom (canFS S) is finite V55() set
K6((dom (canFS S))) is non empty finite V25() set
{((canFS S) . s)} is non empty V2() finite 1 -element set
(canFS S) " {((canFS S) . s)} is finite set
card (S,(canFS S),((canFS S) . s)) is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
(S,(canFS S),((canFS S) . s)) / (len (canFS S)) is V33() ext-real non negative V37() Element of REAL
{s} is non empty V2() finite V25() 1 -element set
card {s} is non empty V4() V5() V6() V10() finite V33() ext-real positive non negative V37() cardinal Element of NAT
(card {s}) / (len (canFS S)) is V33() ext-real non negative V37() Element of REAL
S is finite set
canFS S is Relation-like NAT -defined S -valued Function-like one-to-one finite V31(S) FinSequence-like FinSubsequence-like (S) FinSequence of S
(S,(canFS S)) is non empty functional FinSequence-membered Element of K6((S *))
S * is non empty functional FinSequence-membered M10(S)
K6((S *)) is non empty set
{ b1 where b1 is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S : (S, canFS S,b1) } is set
p is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S
S is finite set
p is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S
(S,p) is non empty functional FinSequence-membered Element of K6((S *))
S * is non empty functional FinSequence-membered M10(S)
K6((S *)) is non empty set
{ b1 where b1 is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S : (S,p,b1) } is set
s is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S
S is finite set
S * is non empty functional FinSequence-membered M10(S)
K6((S *)) is non empty set
(S) is non empty Element of K6(K6((S *)))
K6(K6((S *))) is non empty set
canFS S is Relation-like NAT -defined S -valued Function-like one-to-one finite V31(S) FinSequence-like FinSubsequence-like (S) FinSequence of S
(S,(canFS S)) is non empty functional FinSequence-membered Element of K6((S *))
{ b1 where b1 is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S : (S, canFS S,b1) } is set
s is non empty functional FinSequence-membered Element of K6((S *))
t is Element of (S)
s is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S
s is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S
s is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S
nb is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S
p is Element of (S)
s is Element of (S)
t is set
s is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like Element of S *
t is set
s is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like Element of S *
S is non empty finite set
S * is non empty functional FinSequence-membered M10(S)
canFS S is non empty Relation-like NAT -defined S -valued Function-like one-to-one finite V31(S) FinSequence-like FinSubsequence-like (S) FinSequence of S
p is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like Element of S *
(S,p) is Relation-like NAT -defined REAL -valued Function-like finite V40() V41() V42() FinSequence-like FinSubsequence-like FinSequence of REAL
s is Relation-like NAT -defined REAL -valued Function-like finite V40() V41() V42() FinSequence-like FinSubsequence-like FinSequence of REAL
dom s is finite V55() Element of K6(NAT)
card S is non empty V4() V5() V6() V10() finite V33() ext-real positive non negative V37() cardinal Element of NAT
Seg (card S) is non empty finite card S -element Element of K6(NAT)
{ b1 where b1 is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT : ( 1 <= b1 & b1 <= card S ) } is set
len s is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
S is non empty finite set
canFS S is non empty Relation-like NAT -defined S -valued Function-like one-to-one finite V31(S) FinSequence-like FinSubsequence-like (S) FinSequence of S
(S,(canFS S)) is non empty Relation-like NAT -defined REAL -valued Function-like finite V40() V41() V42() FinSequence-like FinSubsequence-like V70() ProbFinS FinSequence of REAL
S * is non empty functional FinSequence-membered M10(S)
p is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like Element of S *
(S,p) is Relation-like NAT -defined REAL -valued Function-like finite V40() V41() V42() FinSequence-like FinSubsequence-like FinSequence of REAL
dom (S,p) is finite V55() Element of K6(NAT)
card S is non empty V4() V5() V6() V10() finite V33() ext-real positive non negative V37() cardinal Element of NAT
Seg (card S) is non empty finite card S -element Element of K6(NAT)
{ b1 where b1 is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT : ( 1 <= b1 & b1 <= card S ) } is set
len (S,p) is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
S is non empty finite set
(S) is non empty Relation-like NAT -defined REAL -valued Function-like finite V40() V41() V42() FinSequence-like FinSubsequence-like V70() ProbFinS (S)
canFS S is non empty Relation-like NAT -defined S -valued Function-like one-to-one finite V31(S) FinSequence-like FinSubsequence-like (S) FinSequence of S
(S,(canFS S)) is non empty Relation-like NAT -defined REAL -valued Function-like finite V40() V41() V42() FinSequence-like FinSubsequence-like V70() ProbFinS FinSequence of REAL
S is non empty finite set
(S) is Element of (S)
S * is non empty functional FinSequence-membered M10(S)
K6((S *)) is non empty set
(S) is non empty Element of K6(K6((S *)))
K6(K6((S *))) is non empty set
(S) is non empty Relation-like NAT -defined REAL -valued Function-like constant finite V40() V41() V42() FinSequence-like FinSubsequence-like V70() ProbFinS (S)
canFS S is non empty Relation-like NAT -defined S -valued Function-like one-to-one finite V31(S) FinSequence-like FinSubsequence-like (S) FinSequence of S
(S,(canFS S)) is non empty Relation-like NAT -defined REAL -valued Function-like finite V40() V41() V42() FinSequence-like FinSubsequence-like V70() ProbFinS FinSequence of REAL
(S,(S)) is Element of (S)
(S,(canFS S)) is non empty functional FinSequence-membered Element of K6((S *))
{ b1 where b1 is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S : (S, canFS S,b1) } is set
t is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S
t is Relation-like NAT -defined S -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of S
(S) is Relation-like Function-like one-to-one V30((S),REAL * ) Element of K6(K7((S),(REAL *)))
K7((S),(REAL *)) is non empty Relation-like set
K6(K7((S),(REAL *))) is non empty set
(S) . (S,(canFS S)) is set
(S) . (S,(S)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of REAL *
dom (S) is set