deffunc H₁( Nat) -> Element of REAL = In ((max ((f . $1),(g . $1))),REAL);
consider h being sequence of 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 Nat holds h . n = max ((f . n),(g . n))
let n be Nat; :: thesis: h . n = max ((f . n),(g . n))
n in NAT by ORDINAL1:def 12;
then h . n = H₁(n) by A1;
hence h . n = max ((f . n),(g . n)) ; :: thesis: verum