deffunc H₁( object ) -> object = max ((f . (In ($1,X))),(g . (In ($1,X))));
A1: for x being object st x in X holds
H₁(x) in REAL by XREAL_0:def 1;
consider h being Function of X,REAL such that
A2: for x being object st x in X holds
h . x = H₁(x) from FUNCT_2:sch 2(A1);
take h ; :: thesis: for x being Element of X holds h . x = max ((f . x),(g . x))
let x be Element of X; :: thesis: h . x = max ((f . x),(g . x))
h . x = max ((f . x),(g . (In (x,X)))) by A2
.= max ((f . x),(g . x)) ;
hence h . x = max ((f . x),(g . x)) ; :: thesis: verum