now for x1, x2 being object st x1 in distribution_family S & x2 in distribution_family S & (GenProbSEQ S) . x1 = (GenProbSEQ S) . x2 holds
x1 = x2let x1,
x2 be
object ;
( 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 xx1 =
x1,
xx2 =
x2 as
set by TARSKI:1;
consider u1 being
FinSequence of
S such that A4:
x1 = Finseq-EQclass u1
by A1, Def6;
consider u2 being
FinSequence of
S such that A5:
x2 = Finseq-EQclass u2
by A2, Def6;
consider v being
FinSequence of
S such that A6:
v in xx2
and A7:
(GenProbSEQ S) . x2 = FDprobSEQ v
by A2, Def7;
consider u being
FinSequence of
S such that A8:
u in xx1
and A9:
(GenProbSEQ S) . x1 = FDprobSEQ u
by A1, Def7;
A10:
u,
v -are_prob_equivalent
by A3, A9, A7, Th8;
u1,
u -are_prob_equivalent
by A8, A4, Th5;
then A11:
u1,
v -are_prob_equivalent
by A10, Th4;
v,
u2 -are_prob_equivalent
by A6, A5, Th5;
then
u1,
u2 -are_prob_equivalent
by A11, Th4;
hence
x1 = x2
by A4, A5, Th7;
verum end;
hence
GenProbSEQ S is one-to-one
by FUNCT_2:19; verum