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 :: thesis: 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
consider g being object such that
A2: g in G by XBOOLE_0:def 1;
g is Function of X,REAL by A2, FUNCT_2:def 12;
then reconsider g = g as Element of Funcs (X,REAL) by FUNCT_2:8;
consider f being object such that
A3: f in F by XBOOLE_0:def 1;
f is Function of X,REAL by A3, FUNCT_2:def 12;
then reconsider f = f as Element of Funcs (X,REAL) by FUNCT_2:8;
defpred S1[ 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 S1[x,y]
proof
let x be Element of X; :: thesis: ex y being Element of REAL st S1[x,y]
consider y being Real such that
A5: S1[x,y] ;
reconsider y = y as Element of REAL by XREAL_0:def 1;
take y ; :: thesis: S1[x,y]
thus S1[x,y] by A5; :: thesis: verum
end;
consider t being Function of X,REAL such that
A6: for x being Element of X holds S1[x,t . x] from FUNCT_2:sch 3(A4);
reconsider t = t as Element of Funcs (X,REAL) by FUNCT_2:8;
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, A6;
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 object ; :: according to FUNCT_1:def 13 :: 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 non empty functional set by A1;
now :: thesis: for x being Element of IT1 holds x is Function of X,REAL
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 12; :: thesis: verum