consider s being FinSequence of S such that
L1: FDprobSEQ s = p by AS;
consider CS being non empty Subset of (S * ) such that
L3: CS = Finseq-EQclass s ;
reconsider CS = CS as Element of distribution_family S by defQuot, L3;
take CS ; :: thesis: (GenProbSEQ S) . CS = p
thus (GenProbSEQ S) . CS = p by L1, EQX07, L3; :: thesis: verum