defpred S₁[ 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 & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in X2 implies ex y being object st
( y in the carrier of Y & S₁[x,y] ) )
assume x in X2 ; :: thesis: ex y being object st
( y in the carrier of Y & S₁[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 & S₁[x,y] )
thus y in the carrier of Y by A3; :: thesis: S₁[x,y]
thus S₁[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
S₁[x,g1 . x] from FUNCT_2:sch 1(A2);
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)
S₁[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 A5, A6, A7, TARSKI:def 1; :: thesis: verum

end;