theorem Th42: :: WAYBEL25:42

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