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

( 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

hence
g = h
by FUNCT_2:def 8; :: thesis: verumlet 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;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