:: 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

{} 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)

{ b

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)

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

(S,s) is non empty functional FinSequence-membered Element of K6((S *))

{ b

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

{ b

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)

{ b

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)

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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)

{ b

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)

{ b

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)

{ b

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)

{ b

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)

{ b

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)

{ b

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)

{ b

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)

{ b

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)

{ b

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)

{ b

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)

{ b

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)

{ b

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)

{ b

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)

{ b