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

hence
GenProbSEQ S is one-to-one
by FUNCT_2:19; :: thesis: verumx1 = 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;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