consider s being FinSequence of S such that
A1: s = canFS S ;
consider CS being non empty Subset of (S * ) such that
A2: CS = Finseq-EQclass 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 )
A3: s is_uniformly_distributed by A1, Th26;
for t being FinSequence of S st t in CS holds
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 A3, Th24;
hence for s being FinSequence of S holds
( s in CS iff s is_uniformly_distributed ) by A3, A2, Lm3; :: thesis: verum