consider s being FinSequence of S such that
A2: FDprobSEQ s = p by A1;
consider CS being non empty Subset of (S *) such that
A3: CS = Finseq-EQclass s ;
reconsider CS = CS as Element of distribution_family S by A3, Def6;
take CS ; :: thesis: (GenProbSEQ S) . CS = p
thus (GenProbSEQ S) . CS = p by A2, A3, Th12; :: thesis: verum