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 ; :: thesis: verum