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

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 = 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