:: deftheorem Def6 defines lim_in_cod1 CARDFIL4:def 9 :
for X1, X2 being non empty set
for cF1 being Filter of X1
for Y being non empty Hausdorff TopSpace
for f being Function of [:X1,X2:],Y st ( for x being Element of X2 holds lim_filter ((ProjMap2 (f,x)),cF1) <> {} ) holds
for b₆ being Function of X2,Y holds
( b₆ = lim_in_cod1 (f,cF1) iff for x being Element of X2 holds {(b₆ . x)} = lim_filter ((ProjMap2 (f,x)),cF1) );