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