defpred S1[ object , object ] means ex x being Element of X2 ex y being Element of Y st
( x = \$1 & y = \$2 & \$2 in lim_filter ((ProjMap2 (f,x)),cF1) );
A2: for x being object st x in X2 holds
ex y being object st
( y in the carrier of Y & S1[x,y] )
proof
let x be object ; :: thesis: ( x in X2 implies ex y being object st
( y in the carrier of Y & S1[x,y] ) )

assume x in X2 ; :: thesis: ex y being object st
( y in the carrier of Y & S1[x,y] )

then reconsider x2 = x as Element of X2 ;
not lim_filter ((ProjMap2 (f,x2)),cF1) is empty by A1;
then consider y being object such that
A3: y in lim_filter ((ProjMap2 (f,x2)),cF1) ;
take y ; :: thesis: ( y in the carrier of Y & S1[x,y] )
thus y in the carrier of Y by A3; :: thesis: S1[x,y]
thus S1[x,y] by A3; :: thesis: verum
end;
consider g1 being Function of X2, the carrier of Y such that
A4: for x being object st x in X2 holds
S1[x,g1 . x] from reconsider g2 = g1 as Function of X2,Y ;
take g2 ; :: thesis: for x being Element of X2 holds {(g2 . x)} = lim_filter ((ProjMap2 (f,x)),cF1)
hereby :: thesis: verum
let x be Element of X2; :: thesis: {(g2 . x)} = lim_filter ((ProjMap2 (f,x)),cF1)
S1[x,g2 . x] by A4;
then consider x2 being Element of X2, y1 being Element of Y such that
A5: x = x2 and
A6: g2 . x = y1 and
A7: y1 in lim_filter ((ProjMap2 (f,x2)),cF1) ;
( not lim_filter ((ProjMap2 (f,x)),cF1) is empty & lim_filter ((ProjMap2 (f,x)),cF1) is trivial ) by A1;
then ex z being object st lim_filter ((ProjMap2 (f,x)),cF1) = {z} by ZFMISC_1:131;
hence {(g2 . x)} = lim_filter ((ProjMap2 (f,x)),cF1) by ; :: thesis: verum
end;