let S be non empty finite set ; GenProbSEQ S is one-to-one
now let x1,
x2 be
set ;
( x1 in distribution_family S & x2 in distribution_family S & (GenProbSEQ S) . x1 = (GenProbSEQ S) . x2 implies x1 = x2 )assume that A1:
x1 in distribution_family S
and A2:
x2 in distribution_family S
and A3:
(GenProbSEQ S) . x1 = (GenProbSEQ S) . x2
;
x1 = x2reconsider A1 =
x1 as
Subset of
(S *) by A1;
consider u1 being
FinSequence of
S such that A4:
A1 = Finseq-EQclass u1
by A1, Def6;
reconsider A2 =
x2 as
Subset of
(S *) by A2;
consider u2 being
FinSequence of
S such that A5:
A2 = Finseq-EQclass u2
by A2, Def6;
consider v being
FinSequence of
S such that A6:
v in x2
and A7:
(GenProbSEQ S) . x2 = FDprobSEQ v
by A2, Def7;
consider u being
FinSequence of
S such that A8:
u in x1
and A9:
(GenProbSEQ S) . x1 = FDprobSEQ u
by A1, Def7;
A10:
u,
v -are_prob_equivalent
by A3, A9, A7, Th10;
u1,
u -are_prob_equivalent
by A8, A4, Th7;
then A11:
u1,
v -are_prob_equivalent
by A10, Th6;
v,
u2 -are_prob_equivalent
by A6, A5, Th7;
then
u1,
u2 -are_prob_equivalent
by A11, Th6;
hence
x1 = x2
by A4, A5, Th9;
verum end;
hence
GenProbSEQ S is one-to-one
by FUNCT_2:19; verum