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 ) ;
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 = {} 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