let S be non empty 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 set ; :: 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, Def11
.= (FDprobSEQ s) . nb by A1, A3, Def11 ;
hence (FDprobSEQ s) . a = (FDprobSEQ s) . b ; :: thesis: verum