let A, B be Element of distribution_family S; :: thesis: ( ( for s being FinSequence of S holds
( s in A iff s is_uniformly_distributed ) ) & ( for s being FinSequence of S holds
( s in B iff s is_uniformly_distributed ) ) implies A = B )
assume U1: for s being FinSequence of S holds
( s in A iff s is_uniformly_distributed ) ; :: thesis: ( ex s being FinSequence of S st
( ( s in B implies s is_uniformly_distributed ) implies ( s is_uniformly_distributed & not s in B ) ) or A = B )
assume U2: for s being FinSequence of S holds
( s in B iff s is_uniformly_distributed ) ; :: thesis: A = B
N1: for s being set st s in A holds
s in B

proof

let s be set ; :: thesis: ( s in A implies s in B )
assume A1: s in A ; :: thesis: s in B
then reconsider s = s as Element of S * ;
s is_uniformly_distributed by U1, A1;
hence s in B by U2; :: thesis: verum

end;

for s being set st s in B holds
s in A

proof

let s be set ; :: thesis: ( s in B implies s in A )
assume A1: s in B ; :: thesis: s in A
then reconsider s = s as Element of S * ;
s is_uniformly_distributed by U2, A1;
hence s in A by U1; :: thesis: verum

end;

hence A = B by N1, TARSKI:2; :: thesis: verum