deffunc H₁( Element of Funcs (S,BOOLEAN)) -> Element of REAL = In ((Prob ($1,D)),REAL);
consider f being Function of (Funcs (S,BOOLEAN)),REAL such that
A1: for x being Element of Funcs (S,BOOLEAN) holds f . x = H₁(x) from FUNCT_2:sch 4();
take f ; :: thesis: for judgefunc being Element of Funcs (S,BOOLEAN) holds f . judgefunc = Prob (judgefunc,D)
let x be Element of Funcs (S,BOOLEAN); :: thesis: f . x = Prob (x,D)
f . x = In ((Prob (x,D)),REAL) by A1
.= Prob (x,D) ;
hence f . x = Prob (x,D) ; :: thesis: verum