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

s in B

( 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

for s being object st s in A holds
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;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

s in B

proof

hence
A = B
by A4, TARSKI:2; :: thesis: verum
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;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