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] )
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 FUNCT_2:sch 1(A2);
reconsider g2 = g1 as Function of X2,Y ;
take
g2
; for x being Element of X2 holds {(g2 . x)} = lim_filter ((ProjMap2 (f,x)),cF1)
hereby verum
let x be
Element of
X2;
{(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 A5, A6, A7, TARSKI:def 1;
verum
end;