set s = canFS S;
A1: len (canFS S) = card S by FINSEQ_1:93;
then dom (canFS S) = Seg (card S) by FINSEQ_1:def 3;
then A2: dom (canFS S) = dom (FDprobSEQ (canFS S)) by Def3;
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 A3: 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 A2, Def3
.= (card {n}) / (len (canFS S)) by A3, FINSEQ_5:4
.= 1 / (card S) by A1, CARD_1:30 ;
hence (FDprobSEQ (canFS S)) . n = 1 / (card S) ; :: thesis: verum

end;

hence for b₁ being FinSequence of S st b₁ = canFS S holds
b₁ is uniformly_distributed by A2; :: thesis: verum