set s = the Element of D;
take Prob (judgefunc, the Element of D) ; :: thesis: for s being Element of D holds Prob (judgefunc, the Element of D) = Prob (judgefunc,s)
thus for s being Element of D holds Prob (judgefunc, the Element of D) = Prob (judgefunc,s) by Th17; :: thesis: verum