defpred S_{1}[ 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_{1}[x,y]

A3: for x being Element of distribution_family S holds S_{1}[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

( s in $1 & $2 = FDprobSEQ s );

A1: for x being Element of distribution_family S ex y being Element of REAL * st S

proof

consider g being Function of (distribution_family S),(REAL *) such that
let x be Element of distribution_family S; :: thesis: ex y being Element of REAL * st S_{1}[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_{1}[x,y]
by A2, Th6; :: thesis: verum

end;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

A3: for x being Element of distribution_family S holds S

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