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 AS: s is_uniformly_distributed ; :: thesis: FDprobSEQ s is constant
let a, b be set ; :: according to FUNCT_1:def 16 :: thesis: ( not a in whole_event or not b in whole_event or (FDprobSEQ s) . a = (FDprobSEQ s) . b )
assume a: ( a in dom (FDprobSEQ s) & b in dom (FDprobSEQ s) ) ; :: thesis: (FDprobSEQ s) . a = (FDprobSEQ s) . b
then reconsider na = a, nb = b as Nat ;
(FDprobSEQ s) . na = 1 / (card S) by a, AS, defunidistseq
.= (FDprobSEQ s) . nb by a, AS, defunidistseq ;
hence (FDprobSEQ s) . a = (FDprobSEQ s) . b ; :: thesis: verum