deffunc H₁( Element of NAT ) -> Real = max ((f . $1),(g . $1));
consider h being Function of NAT,REAL such that
A1: for n being Element of NAT holds h . n = H₁(n) from FUNCT_2:sch 4();
take h ; :: thesis: for n being Element of NAT holds h . n = max ((f . n),(g . n))
let n be Element of NAT ; :: thesis: h . n = max ((f . n),(g . n))
thus h . n = max ((f . n),(g . n)) by A1; :: thesis: verum