let g1, g2 be Function of X1,Y; :: thesis: ( ( for x being Element of X1 holds {(g1 . x)} = lim_filter ((ProjMap1 (f,x)),cF2) ) & ( for x being Element of X1 holds {(g2 . x)} = lim_filter ((ProjMap1 (f,x)),cF2) ) implies g1 = g2 )
assume that
A1: for x being Element of X1 holds {(g1 . x)} = lim_filter ((ProjMap1 (f,x)),cF2) and
A2: for x being Element of X1 holds {(g2 . x)} = lim_filter ((ProjMap1 (f,x)),cF2) ; :: thesis: g1 = g2
now :: thesis: for x being Element of X1 holds g1 . x = g2 . x
let x be Element of X1; :: thesis: g1 . x = g2 . x
{(g1 . x)} = lim_filter ((ProjMap1 (f,x)),cF2) 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