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 = (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 = (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 S₁[ Element of X, Real] means $2 = (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: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 = (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 = (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 = (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 = (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 = (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 = (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 = (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 = (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 = (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 = (f . n) + (g . n) ) ) } is FUNCTION_DOMAIN of X, REAL by FUNCT_2:def 12; :: thesis: verum