let S be finite set ; :: thesis: for s being FinSequence of S st s is uniformly_distributed holds

FDprobSEQ s is constant

let s be FinSequence of S; :: thesis: ( s is uniformly_distributed implies FDprobSEQ s is constant )

assume A1: s is uniformly_distributed ; :: thesis: FDprobSEQ s is constant

let a, b be object ; :: according to FUNCT_1:def 10 :: thesis: ( not a in whole_event or not b in whole_event or (FDprobSEQ s) . a = (FDprobSEQ s) . b )

assume that

A2: a in dom (FDprobSEQ s) and

A3: b in dom (FDprobSEQ s) ; :: thesis: (FDprobSEQ s) . a = (FDprobSEQ s) . b

reconsider na = a, nb = b as Nat by A2, A3;

(FDprobSEQ s) . na = 1 / (card S) by A1, A2

.= (FDprobSEQ s) . nb by A1, A3 ;

hence (FDprobSEQ s) . a = (FDprobSEQ s) . b ; :: thesis: verum

FDprobSEQ s is constant

let s be FinSequence of S; :: thesis: ( s is uniformly_distributed implies FDprobSEQ s is constant )

assume A1: s is uniformly_distributed ; :: thesis: FDprobSEQ s is constant

let a, b be object ; :: according to FUNCT_1:def 10 :: thesis: ( not a in whole_event or not b in whole_event or (FDprobSEQ s) . a = (FDprobSEQ s) . b )

assume that

A2: a in dom (FDprobSEQ s) and

A3: b in dom (FDprobSEQ s) ; :: thesis: (FDprobSEQ s) . a = (FDprobSEQ s) . b

reconsider na = a, nb = b as Nat by A2, A3;

(FDprobSEQ s) . na = 1 / (card S) by A1, A2

.= (FDprobSEQ s) . nb by A1, A3 ;

hence (FDprobSEQ s) . a = (FDprobSEQ s) . b ; :: thesis: verum