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)_{1} being FinSequence of S st b_{1} = canFS S holds

b_{1} is uniformly_distributed
by A2; :: thesis: verum

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

hence
for b
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;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

b