theorem Th80:
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
lim_filter (
f,
<.cF1,cF2.))
<> {} & ( for
x being
Element of
X1 holds
lim_filter (
(ProjMap1 (f,x)),
cF2)
<> {} ) holds
lim_filter (
f,
<.cF1,cF2.))
= lim_filter (
(lim_in_cod2 (f,cF2)),
cF1)