defpred S₁[ set , set ] means ex s being FinSequence of S st
( s in $1 & $2 = FDprobSEQ s );
A1: for x being Element of distribution_family S ex y being Element of REAL * st S₁[x,y]

proof

let x be Element of distribution_family S; :: thesis: ex y being Element of REAL * st S₁[x,y]
consider s being FinSequence of S such that
A2: x = Finseq-EQclass s by Def6;
FDprobSEQ s in REAL * by FINSEQ_1:def 11;
hence ex y being Element of REAL * st S₁[x,y] by A2, Th6; :: thesis: verum

end;

consider g being Function of (distribution_family S),(REAL *) such that
A3: for x being Element of distribution_family S holds S₁[x,g . x] from FUNCT_2:sch 3(A1);
take g ; :: thesis: for x being Element of distribution_family S ex s being FinSequence of S st
( s in x & g . x = FDprobSEQ s )
thus for x being Element of distribution_family S ex s being FinSequence of S st
( s in x & g . x = FDprobSEQ s ) by A3; :: thesis: verum