theorem Th78: :: CARDFIL4:99

for X1, X2 being non empty set
for cF1 being Filter of X1
for cF2 being Filter of X2
for Y being non empty Hausdorff regular TopSpace
for f being Function of [:X1,X2:],Y st ( for x being Element of X2 holds lim_filter ((ProjMap2 (f,x)),cF1) <> {} ) holds
lim_filter (f,<.cF1,cF2.)) c= lim_filter ((lim_in_cod1 (f,cF1)),cF2)