deffunc H_{1}( 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_{1}(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

consider f being Function of Omega,ExtREAL such that

A1: for w being Element of Omega holds f . w = H

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