deffunc H₁( Subset of REAL) -> Element of ExtREAL = inf (Svc $1);
thus for F1, F2 being Function of (bool REAL),ExtREAL st ( for A being Subset of REAL holds F1 . A = H₁(A) ) & ( for A being Subset of REAL holds F2 . A = H₁(A) ) holds
F1 = F2 from BINOP_2:sch 1(); :: thesis: verum