defpred S₁[ object , object ] means ex x being Element of X1 ex y being Element of Y st
( x = $1 & y = $2 & $2 in lim_filter ((ProjMap1 (f,x)),cF2) );
A2: for x being object st x in X1 holds
ex y being object st
( y in the carrier of Y & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in X1 implies ex y being object st
( y in the carrier of Y & S₁[x,y] ) )
assume x in X1 ; :: thesis: ex y being object st
( y in the carrier of Y & S₁[x,y] )
then reconsider x1 = x as Element of X1 ;
not lim_filter ((ProjMap1 (f,x1)),cF2) is empty by A1;
then consider y being object such that
A3: y in lim_filter ((ProjMap1 (f,x1)),cF2) ;
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 X1, the carrier of Y such that
A4: for x being object st x in X1 holds
S₁[x,g1 . x] from FUNCT_2:sch 1(A2);
reconsider g2 = g1 as Function of X1,Y ;
take g2 ; :: thesis: for x being Element of X1 holds {(g2 . x)} = lim_filter ((ProjMap1 (f,x)),cF2)

hereby :: thesis: verum

let x be Element of X1; :: thesis: {(g2 . x)} = lim_filter ((ProjMap1 (f,x)),cF2)
S₁[x,g2 . x] by A4;
then consider x1 being Element of X1, y1 being Element of Y such that
A5: x = x1 and
A6: g2 . x = y1 and
A7: y1 in lim_filter ((ProjMap1 (f,x1)),cF2) ;
( not lim_filter ((ProjMap1 (f,x)),cF2) is empty & lim_filter ((ProjMap1 (f,x)),cF2) is trivial ) by A1;
then ex z being object st lim_filter ((ProjMap1 (f,x)),cF2) = {z} by ZFMISC_1:131;
hence {(g2 . x)} = lim_filter ((ProjMap1 (f,x)),cF2) by A5, A6, A7, TARSKI:def 1; :: thesis: verum

end;