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 A4: 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 A5: for s being FinSequence of S holds
( s in B iff s is_uniformly_distributed ) ; :: thesis: A = B
A6: 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 A7: s in B ; :: thesis: s in A
then reconsider s = s as Element of S * ;
s is_uniformly_distributed by A5, A7;
hence s in A by A4; :: thesis: verum

end;

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 A8: s in A ; :: thesis: s in B
then reconsider s = s as Element of S * ;
s is_uniformly_distributed by A4, A8;
hence s in B by A5; :: thesis: verum

end;

hence A = B by A6, TARSKI:1; :: thesis: verum