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

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

hence
g1 = g2
by FUNCT_2:def 8; :: thesis: verumlet 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;{(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