let S be non empty finite set ; :: thesis: canFS S is_uniformly_distributed
set s = canFS S;
L0: len (canFS S) = card S by UPROOTS:5;
then dom (canFS S) = Seg (card S) by FINSEQ_1:def 3;
then L01: dom (canFS S) = dom (FDprobSEQ (canFS S)) by defFREQDIST;
for n being Nat st n in dom (canFS S) holds
(FDprobSEQ (canFS S)) . n = 1 / (card S)

proof

let n be Nat; :: thesis: ( n in dom (canFS S) implies (FDprobSEQ (canFS S)) . n = 1 / (card S) )
assume ASB: n in dom (canFS S) ; :: thesis: (FDprobSEQ (canFS S)) . n = 1 / (card S)
then (FDprobSEQ (canFS S)) . n = FDprobability ((canFS S) . n),(canFS S) by defFREQDIST, L01
.= (card {n}) / (len (canFS S)) by FINSEQ_5:4, ASB
.= 1 / (card S) by L0, CARD_1:50 ;
hence (FDprobSEQ (canFS S)) . n = 1 / (card S) ; :: thesis: verum

end;

hence canFS S is_uniformly_distributed by defunidistseq, L01; :: thesis: verum