deffunc H₁( Element of Omega) -> Element of ExtREAL = In ((max ((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 = max ((k1 . w),(k2 . w))
let n be Element of Omega; :: thesis: f . n = max ((k1 . n),(k2 . n))
In ((max ((k1 . n),(k2 . n))),ExtREAL) = max ((k1 . n),(k2 . n)) ;
hence f . n = max ((k1 . n),(k2 . n)) by A1; :: thesis: verum