let a, b be Real; :: thesis: ( ( for s being Element of D holds a = Prob (judgefunc,s) ) & ( for s being Element of D holds b = Prob (judgefunc,s) ) implies a = b )
defpred S₁[ Real] means for s being Element of D holds $1 = Prob (judgefunc,s);
assume A1: S₁[a] ; :: thesis: ( ex s being Element of D st not b = Prob (judgefunc,s) or a = b )
assume A2: S₁[b] ; :: thesis: a = b

now :: thesis: for s being Element of D holds a = b

let s be Element of D; :: thesis: a = b
( a = Prob (judgefunc,s) & b = Prob (judgefunc,s) ) by A1, A2;
hence a = b ; :: thesis: verum

end;

hence a = b ; :: thesis: verum