:: DIST_1 semantic presentation

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

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 )

3 is non empty V4() V5() V6() V10() finite V33() ext-real positive non negative V37() cardinal Element of NAT

Sum () is V33() ext-real V37() Element of REAL
S is set
S is set

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

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

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

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

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

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

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

s is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal set
() . 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

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
() . t is set
(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
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

dom s is finite V55() Element of K6(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 V33() ext-real V37() set
() . 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
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

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

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

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

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

{ 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

S is finite set

(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

(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

(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

(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

t is set

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

{ } is set
S is finite set

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

rng () is finite Element of K6(S)
K6(S) is non empty finite V25() set
dom () is finite V55() Element of K6(NAT)
s is set
() . s is set
len () 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

() . 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
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,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
(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),()) is non empty Relation-like set
K6(K7((S),())) is non empty set
p is Element 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

p is Relation-like Function-like V30((S),REAL * ) Element of K6(K7((S),()))
s is Element of (S)

p is Relation-like Function-like V30((S),REAL * ) Element of K6(K7((S),()))
s is Relation-like Function-like V30((S),REAL * ) Element of K6(K7((S),()))
t is Element 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 is finite set
(S) is Relation-like Function-like V30((S),REAL * ) Element of K6(K7((S),()))
(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),()) is non empty Relation-like set
K6(K7((S),())) is non empty set

(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 is finite set
(S) is Relation-like Function-like V30((S),REAL * ) Element of K6(K7((S),()))
(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),()) is non empty Relation-like set
K6(K7((S),())) is non empty set
p is set
s is set
(S) . p is set
(S) . s is set

(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,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 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
(S) is Relation-like Function-like one-to-one V30((S),REAL * ) Element of K6(K7((S),()))
K7((S),()) is non empty Relation-like set
K6(K7((S),())) is non empty 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 Element of (S)

s is Element of (S)

t is Element of (S)

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

len p is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT

rng () 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 () is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT
Seg (len ()) is finite len () -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 () ) } is set
dom () is finite V55() Element of K6(NAT)
() . 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

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

dom s is finite V55() Element of K6(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

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
() . 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) . s is V33() ext-real V37() set
(len p) * ((S,p) . s) is V33() ext-real V37() Element of REAL
rng () 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 () is non empty V4() V5() V6() V10() finite V33() ext-real positive non negative V37() cardinal Element of NAT
Seg (len ()) is non empty finite len () -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 () ) } is set
dom () 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

len p is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT

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

Sum (S,p) is V33() set
len p is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal Element of NAT

Sum (S,p) is V33() ext-real V37() Element of REAL
(len p) * (Sum (S,p)) is V33() ext-real V37() Element of REAL

S is non empty finite set

dom p is non empty finite V55() Element of K6(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 () is non empty finite Element of K6(S)
dom () is non empty finite V55() Element of K6(NAT)
s is set
() . 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
() . nb is set
len () is non empty V4() V5() V6() V10() finite V33() ext-real positive non negative V37() cardinal Element of NAT
Seg (len ()) is non empty finite len () -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 () ) } 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

p is 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

dom p is set

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

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

[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 + 1) is V4() V5() V6() V10() finite V33() ext-real non negative V37() cardinal set

[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

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 () is V4() V5() V6() cardinal set
(Sum s) + (s . (S + 1)) is Element of COMPLEX
Sum s is V33() set

dom p is set

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 () is V4() V5() V6() cardinal set
Sum s is V33() set

dom S is set
Union S is set
rng S is set
union (rng S) is set
card () is V4() V5() V6() cardinal set

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

dom S is set
Union S is set
rng S is set
union (rng S) is set
card () is V4() V5() V6() cardinal set

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

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 () 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 () 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
() . t is set
rng () 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

dom t is set
s is set
nb is set
t . s is set
t . nb is set
() . s is set
() . 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 () is non empty finite Element of K6(S)
j is Element of S
nne is set
() . 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
() . s is set

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,(() . 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 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
(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
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
() . 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

Sum (S,p) is V33() ext-real V37() Element of REAL

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

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

() . 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 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
len p is non empty V4() V5() V6() V10() finite V33() ext-real positive non negative V37() cardinal Element of NAT
(S,p,(() . 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

[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),()))
K7((S),()) is non empty Relation-like set
K6(K7((S),())) is non empty set

(S,p) is Element of (S)

S is finite set
S is finite set

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

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

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()