theorem :: MATHMORP:57

for n being Element of NAT
for X being non empty Subset of (TOP-REAL n) holds 0 (.) X = {(0. (TOP-REAL n))}