let X1, X2 be 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) <> {} ) & ( for x being Element of X2 holds lim_filter ((ProjMap2 (f,x)),cF1) <> {} ) holds
lim_filter ((lim_in_cod2 (f,cF2)),cF1) = lim_filter ((lim_in_cod1 (f,cF1)),cF2)
let cF1 be 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) <> {} ) & ( for x being Element of X2 holds lim_filter ((ProjMap2 (f,x)),cF1) <> {} ) holds
lim_filter ((lim_in_cod2 (f,cF2)),cF1) = lim_filter ((lim_in_cod1 (f,cF1)),cF2)
let cF2 be 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) <> {} ) & ( for x being Element of X2 holds lim_filter ((ProjMap2 (f,x)),cF1) <> {} ) holds
lim_filter ((lim_in_cod2 (f,cF2)),cF1) = lim_filter ((lim_in_cod1 (f,cF1)),cF2)
let Y be 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) <> {} ) & ( for x being Element of X2 holds lim_filter ((ProjMap2 (f,x)),cF1) <> {} ) holds
lim_filter ((lim_in_cod2 (f,cF2)),cF1) = lim_filter ((lim_in_cod1 (f,cF1)),cF2)
let f be Function of [:X1,X2:],Y; ( lim_filter (f,<.cF1,cF2.)) <> {} & ( for x being Element of X1 holds lim_filter ((ProjMap1 (f,x)),cF2) <> {} ) & ( for x being Element of X2 holds lim_filter ((ProjMap2 (f,x)),cF1) <> {} ) implies lim_filter ((lim_in_cod2 (f,cF2)),cF1) = lim_filter ((lim_in_cod1 (f,cF1)),cF2) )
assume that
A1:
lim_filter (f,<.cF1,cF2.)) <> {}
and
A2:
for x being Element of X1 holds lim_filter ((ProjMap1 (f,x)),cF2) <> {}
and
A3:
for x being Element of X2 holds lim_filter ((ProjMap2 (f,x)),cF1) <> {}
; lim_filter ((lim_in_cod2 (f,cF2)),cF1) = lim_filter ((lim_in_cod1 (f,cF1)),cF2)
lim_filter (f,<.cF1,cF2.)) = lim_filter ((lim_in_cod1 (f,cF1)),cF2)
by A1, A3, Th81;
hence
lim_filter ((lim_in_cod2 (f,cF2)),cF1) = lim_filter ((lim_in_cod1 (f,cF1)),cF2)
by A1, A2, Th80; verum