let CS1, CS2 be Element of distribution_family S; :: thesis: ( (GenProbSEQ S) . CS1 = p & (GenProbSEQ S) . CS2 = p implies CS1 = CS2 )
assume A3: (GenProbSEQ S) . CS1 = p ; :: thesis: ( not (GenProbSEQ S) . CS2 = p or CS1 = CS2 )
then A4: CS1 in dom (GenProbSEQ S) by FUNCT_1:def 2;
assume A5: (GenProbSEQ S) . CS2 = p ; :: thesis: CS1 = CS2
then CS2 in dom (GenProbSEQ S) by FUNCT_1:def 2;
hence CS1 = CS2 by A3, A5, A4, FUNCT_1:def 4; :: thesis: verum