set CS = { f where f is Function of the carrier of X, the carrier of T : ( f is continuous & ex Y being non empty Subset of X st
( Y is compact & Cl (support f) c= Y ) ) } ;
A1: { f where f is Function of the carrier of X, the carrier of T : ( f is continuous & ex Y being non empty Subset of X st
( Y is compact & Cl (support f) c= Y ) ) } c= Funcs ( the carrier of X, the carrier of T)

proof

for x being object st x in { f where f is Function of the carrier of X, the carrier of T : ( f is continuous & ex Y being non empty Subset of X st
( Y is compact & Cl (support f) c= Y ) ) } holds
x in Funcs ( the carrier of X, the carrier of T)

proof

let x be object ; :: thesis: ( x in { f where f is Function of the carrier of X, the carrier of T : ( f is continuous & ex Y being non empty Subset of X st
( Y is compact & Cl (support f) c= Y ) ) } implies x in Funcs ( the carrier of X, the carrier of T) )
assume x in { f where f is Function of the carrier of X, the carrier of T : ( f is continuous & ex Y being non empty Subset of X st
( Y is compact & Cl (support f) c= Y ) ) } ; :: thesis: x in Funcs ( the carrier of X, the carrier of T)
then ex f being Function of the carrier of X, the carrier of T st
( x = f & f is continuous & ex Y being non empty Subset of X st
( Y is compact & Cl (support f) c= Y ) ) ;
hence x in Funcs ( the carrier of X, the carrier of T) by FUNCT_2:8; :: thesis: verum

end;

hence { f where f is Function of the carrier of X, the carrier of T : ( f is continuous & ex Y being non empty Subset of X st
( Y is compact & Cl (support f) c= Y ) ) } c= Funcs ( the carrier of X, the carrier of T) ; :: thesis: verum

end;

not { f where f is Function of the carrier of X, the carrier of T : ( f is continuous & ex Y being non empty Subset of X st
( Y is compact & Cl (support f) c= Y ) ) } is empty

proof

set g = X --> (0. T);
reconsider g = X --> (0. T) as Function of the carrier of X, the carrier of T ;
ex Y being non empty Subset of X st
( Y is compact & Cl (support g) c= Y )

proof

set PX = the Point of X;
reconsider S = { the Point of X} as non empty Subset of X ;
reconsider K = S as Subset of X ;
take S ; :: thesis: ( S is compact & Cl (support g) c= S )
thus S is compact ; :: thesis: Cl (support g) c= S
support g = {}

proof

assume A4: not support g = {} ; :: thesis: contradiction
set p = the Element of support g;
A5: the Element of support g in support g by A4;
( the Element of support g in dom g & g /. the Element of support g <> 0. T ) by A4, Def10;
then g . the Element of support g <> 0. T by PARTFUN1:def 6;
hence contradiction by A5, FUNCOP_1:7; :: thesis: verum

end;

hence Cl (support g) c= S by PRE_TOPC:22; :: thesis: verum

end;

then g in { f where f is Function of the carrier of X, the carrier of T : ( f is continuous & ex Y being non empty Subset of X st
( Y is compact & Cl (support f) c= Y ) ) } ;
hence not { f where f is Function of the carrier of X, the carrier of T : ( f is continuous & ex Y being non empty Subset of X st
( Y is compact & Cl (support f) c= Y ) ) } is empty ; :: thesis: verum

end;

hence { f where f is Function of the carrier of X, the carrier of T : ( f is continuous & ex Y being non empty Subset of X st
( Y is compact & Cl (support f) c= Y ) ) } is non empty Subset of (RealVectSpace ( the carrier of X,T)) by A1; :: thesis: verum