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