theorem Th41: :: WAYBEL25:41

for X being non empty TopSpace
for Y being monotone-convergence T_0-TopSpace
for N being net of ContMaps (X,(Omega Y))
for x being Point of X
for f being Function of X,(Omega Y) st ( for a being Point of X holds commute (N,a,(Omega Y)) is eventually-directed ) & f = "\/" ((rng the mapping of N),((Omega Y) |^ the carrier of X)) holds
f . x = sup (commute (N,x,(Omega Y)))