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

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