now :: thesis: for x1, x2 being object st x1 in distribution_family S & x2 in distribution_family S & (GenProbSEQ S) . x1 = (GenProbSEQ S) . x2 holds
x1 = x2

let x1, x2 be object ; :: thesis: ( 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 ; :: thesis: x1 = x2
reconsider 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; :: thesis: verum

end;

hence GenProbSEQ S is one-to-one by FUNCT_2:19; :: thesis: verum