defpred S1[ 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 & S1[x,y] )
proof
let x be object ; :: thesis: ( x in X1 implies ex y being object st
( y in the carrier of Y & S1[x,y] ) )

assume x in X1 ; :: thesis: ex y being object st
( y in the carrier of Y & S1[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 & 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 X1, the carrier of Y such that
A4: for x being object st x in X1 holds
S1[x,g1 . x] from 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)
S1[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 ; :: thesis: verum
end;