defpred S_{1}[ 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_{1}[x,y] )

A4: for x being object st x in X2 holds

S_{1}[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)

( 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

proof

consider g1 being Function of X2, the carrier of Y such that
let x be object ; :: thesis: ( x in X2 implies ex y being object st

( y in the carrier of Y & S_{1}[x,y] ) )

assume x in X2 ; :: thesis: ex y being object st

( y in the carrier of Y & S_{1}[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_{1}[x,y] )

thus y in the carrier of Y by A3; :: thesis: S_{1}[x,y]

thus S_{1}[x,y]
by A3; :: thesis: verum

end;( y in the carrier of Y & S

assume x in X2 ; :: thesis: ex y being object st

( y in the carrier of Y & S

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

thus y in the carrier of Y by A3; :: thesis: S

thus S

A4: for x being object st x in X2 holds

S

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_{1}[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;S

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