defpred S₁[ set , set ] means ex s being FinSequence of S st
( s in $1 & $2 = FDprobSEQ s );
P0: 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]
reconsider A = x as Subset of (S * ) ;
consider s being FinSequence of S such that
P02: A = Finseq-EQclass s by defQuot;
FDprobSEQ s in REAL * by FINSEQ_1:def 11;
hence ex y being Element of REAL * st S₁[x,y] by EQX03, P02; :: thesis: verum

end;

consider g being Function of (distribution_family S),(REAL * ) such that
P1: for x being Element of distribution_family S holds S₁[x,g . x] from FUNCT_2:sch 3(P0);
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 P1; :: thesis: verum