set x = the Element of S;
reconsider sx = <* the Element of S*> as FinSequence of S ;
reconsider sx = sx as Element of S * by FINSEQ_1:def 11;
reconsider Dx = Finseq-EQclass sx as Element of distribution_family S by DIST_1:def 6;
reconsider z = {} as Element of S * by FINSEQ_1:49;
not {} in Dx
proof
assume {} in Dx ; :: thesis: contradiction
then reconsider z = {} as Element of Dx ;
A1: ( len sx = 1 & rng sx = { the Element of S} ) by FINSEQ_1:39;
len sx = card (rng sx) by A1, CARD_1:30;
then A2: sx is one-to-one by FINSEQ_4:62;
A3: the Element of S in rng sx by A1, TARSKI:def 1;
FDprobability ( the Element of S,sx) = FDprobability ( the Element of S,z) by DIST_1:def 4, DIST_1:7;
hence contradiction by A3, A1, A2, FINSEQ_4:73; :: thesis: verum
end;
then Dx is well-distributed by SETFAM_1:def 8;
hence ex b1 being Element of distribution_family S st b1 is well-distributed ; :: thesis: verum