set IT = { t where t is Element of Funcs X,REAL : ex f, g being Element of Funcs X,REAL st
( f in F & g in G & ( for n being Element of X holds t . n = max (f . n),(g . n) ) ) } ;

A1: now

consider g being set such that
A2: g in G by XBOOLE_0:def 1;
g is Function of X,REAL by A2, FUNCT_2:def 13;
then reconsider g = g as Element of Funcs X,REAL by FUNCT_2:11;
consider f being set such that
A3: f in F by XBOOLE_0:def 1;
f is Function of X,REAL by A3, FUNCT_2:def 13;
then reconsider f = f as Element of Funcs X,REAL by FUNCT_2:11;
defpred S₁[ Element of X, Real] means $2 = max (f . $1),(g . $1);
A4: for x being Element of X ex y being Element of REAL st S₁[x,y] ;
consider t being Function of X,REAL such that
A5: for x being Element of X holds S₁[x,t . x] from FUNCT_2:sch 3(A4);
reconsider t = t as Element of Funcs X,REAL by FUNCT_2:11;
t in { t where t is Element of Funcs X,REAL : ex f, g being Element of Funcs X,REAL st
( f in F & g in G & ( for n being Element of X holds t . n = max (f . n),(g . n) ) ) } by A3, A2, A5;
hence not { t where t is Element of Funcs X,REAL : ex f, g being Element of Funcs X,REAL st
( f in F & g in G & ( for n being Element of X holds t . n = max (f . n),(g . n) ) ) } is empty ; :: thesis: verum

end;

{ t where t is Element of Funcs X,REAL : ex f, g being Element of Funcs X,REAL st
( f in F & g in G & ( for n being Element of X holds t . n = max (f . n),(g . n) ) ) } is functional

proof

let x be set ; :: according to FUNCT_1:def 19 :: thesis: ( not x in { t where t is Element of Funcs X,REAL : ex f, g being Element of Funcs X,REAL st
( f in F & g in G & ( for n being Element of X holds t . n = max (f . n),(g . n) ) ) } or x is set )
assume x in { t where t is Element of Funcs X,REAL : ex f, g being Element of Funcs X,REAL st
( f in F & g in G & ( for n being Element of X holds t . n = max (f . n),(g . n) ) ) } ; :: thesis: x is set
then ex t being Element of Funcs X,REAL st
( x = t & ex f, g being Element of Funcs X,REAL st
( f in F & g in G & ( for n being Element of X holds t . n = max (f . n),(g . n) ) ) ) ;
hence x is set ; :: thesis: verum

end;

then reconsider IT1 = { t where t is Element of Funcs X,REAL : ex f, g being Element of Funcs X,REAL st
( f in F & g in G & ( for n being Element of X holds t . n = max (f . n),(g . n) ) ) } as functional non empty set by A1;

now

let x be Element of IT1; :: thesis: x is Function of X,REAL
x in { t where t is Element of Funcs X,REAL : ex f, g being Element of Funcs X,REAL st
( f in F & g in G & ( for n being Element of X holds t . n = max (f . n),(g . n) ) ) } ;
then ex t being Element of Funcs X,REAL st
( x = t & ex f, g being Element of Funcs X,REAL st
( f in F & g in G & ( for n being Element of X holds t . n = max (f . n),(g . n) ) ) ) ;
hence x is Function of X,REAL ; :: thesis: verum

end;

hence { t where t is Element of Funcs X,REAL : ex f, g being Element of Funcs X,REAL st
( f in F & g in G & ( for n being Element of X holds t . n = max (f . n),(g . n) ) ) } is FUNCTION_DOMAIN of X, REAL by FUNCT_2:def 13; :: thesis: verum