set s = canFS S;
consider CS being non empty Subset of (S *) such that
A1: CS = Finseq-EQclass (canFS S) ;
reconsider CS = CS as Element of distribution_family S by A1, Def6;
take CS ; :: thesis: for s being FinSequence of S holds
( s in CS iff s is uniformly_distributed )
for t being FinSequence of S st t in CS holds
canFS S,t -are_prob_equivalent by A1, Th5;
then for t being FinSequence of S st t in CS holds
t is uniformly_distributed by Th20;
hence for s being FinSequence of S holds
( s in CS iff s is uniformly_distributed ) by A1, Lm4; :: thesis: verum