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 A2: 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 A3: for s being FinSequence of S holds
( s in B iff s is uniformly_distributed ) ; :: thesis: A = B
A4: for s being object st s in B holds
s in A

proof

let s be object ; :: thesis: ( s in B implies s in A )
assume A5: s in B ; :: thesis: s in A
then reconsider s = s as Element of S * ;
s is uniformly_distributed by A3, A5;
hence s in A by A2; :: thesis: verum

end;

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

proof

let s be object ; :: thesis: ( s in A implies s in B )
assume A6: s in A ; :: thesis: s in B
then reconsider s = s as Element of S * ;
s is uniformly_distributed by A2, A6;
hence s in B by A3; :: thesis: verum

end;

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