set s = canFS S;
consider CS being non empty Subset of (S *) such that
A2: CS = Finseq-EQclass (canFS S) ;
reconsider CS = CS as Element of distribution_family S by A2, 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 A2, Th7;
then for t being FinSequence of S st t in CS holds
t is uniformly_distributed by Th24;
hence for s being FinSequence of S holds
( s in CS iff s is uniformly_distributed ) by A2, Lm3; :: thesis: verum