let S be non empty finite set ; :: thesis: for A being Element of distribution_family S holds not A is empty
let A be Element of distribution_family S; :: thesis: not A is empty
ex s being FinSequence of S st A = Finseq-EQclass s by DIST_1:def 6;
hence not A is empty ; :: thesis: verum