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