let X1, X2 be non empty set ; :: thesis: 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)

let cF1 be Filter of X1; :: thesis: 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)

let cF2 be Filter of X2; :: thesis: 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)

let Y be non empty Hausdorff regular TopSpace; :: thesis: 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)

let f be Function of [:X1,X2:],Y; :: thesis: ( lim_filter (f,<.cF1,cF2.)) <> {} & ( for x being Element of X1 holds lim_filter ((ProjMap1 (f,x)),cF2) <> {} ) implies lim_filter (f,<.cF1,cF2.)) = lim_filter ((lim_in_cod2 (f,cF2)),cF1) )

assume that

A1: lim_filter (f,<.cF1,cF2.)) <> {} and

A2: for x being Element of X1 holds lim_filter ((ProjMap1 (f,x)),cF2) <> {} ; :: thesis: lim_filter (f,<.cF1,cF2.)) = lim_filter ((lim_in_cod2 (f,cF2)),cF1)

consider y being object such that

A3: lim_filter (f,<.cF1,cF2.)) = {y} by A1, ZFMISC_1:131;

A4: y in lim_filter (f,<.cF1,cF2.)) by A3, TARSKI:def 1;

A5: lim_filter (f,<.cF1,cF2.)) c= lim_filter ((lim_in_cod2 (f,cF2)),cF1) by A2, Th79;

( not lim_filter ((lim_in_cod2 (f,cF2)),cF1) is empty & lim_filter ((lim_in_cod2 (f,cF2)),cF1) is trivial ) by A3, A5;

then ex z being object st lim_filter ((lim_in_cod2 (f,cF2)),cF1) = {z} by ZFMISC_1:131;

hence lim_filter (f,<.cF1,cF2.)) = lim_filter ((lim_in_cod2 (f,cF2)),cF1) by A3, A5, A4, TARSKI:def 1; :: thesis: verum

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)

let cF1 be Filter of X1; :: thesis: 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)

let cF2 be Filter of X2; :: thesis: 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)

let Y be non empty Hausdorff regular TopSpace; :: thesis: 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)

let f be Function of [:X1,X2:],Y; :: thesis: ( lim_filter (f,<.cF1,cF2.)) <> {} & ( for x being Element of X1 holds lim_filter ((ProjMap1 (f,x)),cF2) <> {} ) implies lim_filter (f,<.cF1,cF2.)) = lim_filter ((lim_in_cod2 (f,cF2)),cF1) )

assume that

A1: lim_filter (f,<.cF1,cF2.)) <> {} and

A2: for x being Element of X1 holds lim_filter ((ProjMap1 (f,x)),cF2) <> {} ; :: thesis: lim_filter (f,<.cF1,cF2.)) = lim_filter ((lim_in_cod2 (f,cF2)),cF1)

consider y being object such that

A3: lim_filter (f,<.cF1,cF2.)) = {y} by A1, ZFMISC_1:131;

A4: y in lim_filter (f,<.cF1,cF2.)) by A3, TARSKI:def 1;

A5: lim_filter (f,<.cF1,cF2.)) c= lim_filter ((lim_in_cod2 (f,cF2)),cF1) by A2, Th79;

( not lim_filter ((lim_in_cod2 (f,cF2)),cF1) is empty & lim_filter ((lim_in_cod2 (f,cF2)),cF1) is trivial ) by A3, A5;

then ex z being object st lim_filter ((lim_in_cod2 (f,cF2)),cF1) = {z} by ZFMISC_1:131;

hence lim_filter (f,<.cF1,cF2.)) = lim_filter ((lim_in_cod2 (f,cF2)),cF1) by A3, A5, A4, TARSKI:def 1; :: thesis: verum