let X be non empty TopSpace; for Y being non empty compact TopSpace
for x being Point of X
for Z being Subset of [:Y,X:] st Z = [:([#] Y),{x}:] holds
Z is compact
let Y be non empty compact TopSpace; for x being Point of X
for Z being Subset of [:Y,X:] st Z = [:([#] Y),{x}:] holds
Z is compact
let x be Point of X; for Z being Subset of [:Y,X:] st Z = [:([#] Y),{x}:] holds
Z is compact
let Z be Subset of [:Y,X:]; ( Z = [:([#] Y),{x}:] implies Z is compact )
reconsider V = {x} as non empty Subset of X ;
Y,[:Y,(X | V):] are_homeomorphic
by Lm3;
then A1:
[:Y,(X | V):] is compact
by Th14;
assume A2:
Z = [:([#] Y),{x}:]
; Z is compact
then
TopStruct(# the carrier of [:Y,(X | V):], the topology of [:Y,(X | V):] #) = TopStruct(# the carrier of ([:Y,X:] | Z), the topology of ([:Y,X:] | Z) #)
by Lm4;
hence
Z is compact
by A2, A1, COMPTS_1:3; verum