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