let g, h be Function of (distribution_family S),(REAL *); :: thesis: ( ( for x being Element of distribution_family S ex s being FinSequence of S st
( s in x & g . x = FDprobSEQ s ) ) & ( for x being Element of distribution_family S ex s being FinSequence of S st
( s in x & h . x = FDprobSEQ s ) ) implies g = h )
assume A4: for x being Element of distribution_family S ex s being FinSequence of S st
( s in x & g . x = FDprobSEQ s ) ; :: thesis: ( ex x being Element of distribution_family S st
for s being FinSequence of S holds
( not s in x or not h . x = FDprobSEQ s ) or g = h )
assume A5: for x being Element of distribution_family S ex s being FinSequence of S st
( s in x & h . x = FDprobSEQ s ) ; :: thesis: g = h

now :: thesis: for x being Element of distribution_family S holds g . x = h . x

let x be Element of distribution_family S; :: thesis: g . x = h . x
consider u being FinSequence of S such that
A6: x = Finseq-EQclass u by Def6;
consider t being FinSequence of S such that
A7: t in x and
A8: h . x = FDprobSEQ t by A5;
A9: t,u -are_prob_equivalent by A6, A7, Th5;
consider s being FinSequence of S such that
A10: s in x and
A11: g . x = FDprobSEQ s by A4;
u,s -are_prob_equivalent by A6, A10, Th5;
then t,s -are_prob_equivalent by A9, Th4;
hence g . x = h . x by A11, A8, Th8; :: thesis: verum

end;

hence g = h by FUNCT_2:def 8; :: thesis: verum