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