theorem Th26: :: WAYBEL25:26

for X being non empty TopSpace
for Y being T_0-TopSpace
for N being net of ContMaps (X,(Omega Y)) st ( for x being Point of X holds ex_sup_of commute (N,x,(Omega Y)) ) holds
ex_sup_of rng the mapping of N,(Omega Y) |^ the carrier of X