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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { f where f is Function of the carrier of X,COMPLEX : ( f is continuous & ex Y being non empty Subset of X st
( Y is compact & ( for A being Subset of X st A = support f holds
Cl A is Subset of Y ) ) ) } or x in Funcs ( the carrier of X,COMPLEX) )
assume x in { f where f is Function of the carrier of X,COMPLEX : ( f is continuous & ex Y being non empty Subset of X st
( Y is compact & ( for A being Subset of X st A = support f holds
Cl A is Subset of Y ) ) ) } ; :: thesis: x in Funcs ( the carrier of X,COMPLEX)
then ex f being Function of the carrier of X,COMPLEX st
( x = f & f is continuous & ex Y being non empty Subset of X st
( Y is compact & ( for A being Subset of X st A = support f holds
Cl A is Subset of Y ) ) ) ;
hence x in Funcs ( the carrier of X,COMPLEX) by FUNCT_2:8; :: thesis: verum

end;

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

proof

set g = the carrier of X --> 0c;
reconsider g = the carrier of X --> 0c as Function of the carrier of X,COMPLEX ;
A2: g is continuous

proof

for P being Subset of COMPLEX st P is closed holds
g " P is closed

proof

let P be Subset of COMPLEX; :: thesis: ( P is closed implies g " P is closed )
assume P is closed ; :: thesis: g " P is closed
set F = the carrier of X --> 0;
set H = the carrier of X;
set HX = [#] X;

per cases ( 0 in P or not 0 in P ) ;

suppose 0 in P ; :: thesis: g " P is closed

then g " P = [#] X by FUNCOP_1:14;
hence g " P is closed ; :: thesis: verum

end;

suppose not 0 in P ; :: thesis: g " P is closed

then ( the carrier of X --> 0) " P = {} X by FUNCOP_1:16;
hence g " P is closed ; :: thesis: verum

end;

end;

end;

hence g is continuous ; :: thesis: verum

end;

A3: ex Y being non empty Subset of X st
( Y is compact & ( for A being Subset of X st A = support g holds
Cl A is Subset of Y ) )

proof

set S = the non empty compact Subset of X;
for A being Subset of X st A = support g holds
Cl A is Subset of the non empty compact Subset of X

proof

let A be Subset of X; :: thesis: ( A = support g implies Cl A is Subset of the non empty compact Subset of X )
assume A4: A = support g ; :: thesis: Cl A is Subset of the non empty compact Subset of X
A5: A = {}

proof

assume A6: not A = {} ; :: thesis: contradiction
set p = the Element of support g;
A7: the Element of support g in A by A6, A4;
then g . the Element of support g <> 0 by A4, PRE_POLY:def 7;
hence contradiction by A7, FUNCOP_1:7; :: thesis: verum

end;

Cl ({} X) = {} by PRE_TOPC:22;
hence Cl A is Subset of the non empty compact Subset of X by A5, XBOOLE_1:2; :: thesis: verum

end;

hence ex Y being non empty Subset of X st
( Y is compact & ( for A being Subset of X st A = support g holds
Cl A is Subset of Y ) ) ; :: thesis: verum

end;

g in { f where f is Function of the carrier of X,COMPLEX : ( f is continuous & ex Y being non empty Subset of X st
( Y is compact & ( for A being Subset of X st A = support f holds
Cl A is Subset of Y ) ) ) } by A2, A3;
hence not { f where f is Function of the carrier of X,COMPLEX : ( f is continuous & ex Y being non empty Subset of X st
( Y is compact & ( for A being Subset of X st A = support f holds
Cl A is Subset of Y ) ) ) } is empty ; :: thesis: verum

end;

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