let g1, g2 be Function of X2,Y; :: thesis: ( ( for x being Element of X2 holds {(g1 . x)} = lim_filter ((ProjMap2 (f,x)),cF1) ) & ( for x being Element of X2 holds {(g2 . x)} = lim_filter ((ProjMap2 (f,x)),cF1) ) implies g1 = g2 )
assume that
A1: for x being Element of X2 holds {(g1 . x)} = lim_filter ((ProjMap2 (f,x)),cF1) and
A2: for x being Element of X2 holds {(g2 . x)} = lim_filter ((ProjMap2 (f,x)),cF1) ; :: thesis: g1 = g2

now :: thesis: for x being Element of X2 holds g1 . x = g2 . x

let x be Element of X2; :: thesis: g1 . x = g2 . x
{(g1 . x)} = lim_filter ((ProjMap2 (f,x)),cF1) by A1;
then {(g1 . x)} = {(g2 . x)} by A2;
hence g1 . x = g2 . x by ZFMISC_1:3; :: thesis: verum

end;

hence g1 = g2 by FUNCT_2:def 8; :: thesis: verum