deffunc H₁( Element of Omega) -> Element of ExtREAL = In ((min ((k1 . $1),(k2 . $1))),ExtREAL);
consider f being Function of Omega,ExtREAL such that
A1: for w being Element of Omega holds f . w = H₁(w) from FUNCT_2:sch 4();
take f ; :: thesis: for w being Element of Omega holds f . w = min ((k1 . w),(k2 . w))
let n be Element of Omega; :: thesis: f . n = min ((k1 . n),(k2 . n))
f . n = In ((min ((k1 . n),(k2 . n))),ExtREAL) by A1;
hence f . n = min ((k1 . n),(k2 . n)) ; :: thesis: verum