let S be non empty finite set ; :: thesis: for D being Element of distribution_family S
for s being FinSequence of S st s in D holds
D = Finseq-EQclass s
let D be Element of distribution_family S; :: thesis: for s being FinSequence of S st s in D holds
D = Finseq-EQclass s
let s be FinSequence of S; :: thesis: ( s in D implies D = Finseq-EQclass s )
assume A1: s in D ; :: thesis: D = Finseq-EQclass s
consider t being FinSequence of S such that
A2: D = Finseq-EQclass t by DIST_1:def 6;
thus D = Finseq-EQclass s by A2, DIST_1:9, A1, DIST_1:7; :: thesis: verum