let Rseq be Function of [:NAT,NAT:],REAL; :: thesis: for Y being non empty Hausdorff TopSpace
for f being Function of [:NAT,NAT:],Y st ( for x being Element of NAT holds lim_filter ((ProjMap1 (f,x)),(Frechet_Filter NAT)) <> {} ) & f = Rseq & Y = R^1 holds
lim_in_cod2 (f,(Frechet_Filter NAT)) = lim_in_cod2 Rseq
let Y be non empty Hausdorff TopSpace; :: thesis: for f being Function of [:NAT,NAT:],Y st ( for x being Element of NAT holds lim_filter ((ProjMap1 (f,x)),(Frechet_Filter NAT)) <> {} ) & f = Rseq & Y = R^1 holds
lim_in_cod2 (f,(Frechet_Filter NAT)) = lim_in_cod2 Rseq
let f be Function of [:NAT,NAT:],Y; :: thesis: ( ( for x being Element of NAT holds lim_filter ((ProjMap1 (f,x)),(Frechet_Filter NAT)) <> {} ) & f = Rseq & Y = R^1 implies lim_in_cod2 (f,(Frechet_Filter NAT)) = lim_in_cod2 Rseq )
assume that
A1: for x being Element of NAT holds lim_filter ((ProjMap1 (f,x)),(Frechet_Filter NAT)) <> {} and
A2: f = Rseq and
A3: Y = R^1 ; :: thesis: lim_in_cod2 (f,(Frechet_Filter NAT)) = lim_in_cod2 Rseq
now :: thesis: ( dom (lim_in_cod2 (f,(Frechet_Filter NAT))) = dom (lim_in_cod2 Rseq) & ( for t being object st t in dom (lim_in_cod2 (f,(Frechet_Filter NAT))) holds
(lim_in_cod2 (f,(Frechet_Filter NAT))) . t = (lim_in_cod2 Rseq) . t ) )
dom (lim_in_cod2 (f,(Frechet_Filter NAT))) = NAT by FUNCT_2:def 1;
hence dom (lim_in_cod2 (f,(Frechet_Filter NAT))) = dom (lim_in_cod2 Rseq) by FUNCT_2:def 1; :: thesis: for t being object st t in dom (lim_in_cod2 (f,(Frechet_Filter NAT))) holds
(lim_in_cod2 (f,(Frechet_Filter NAT))) . t = (lim_in_cod2 Rseq) . t
thus for t being object st t in dom (lim_in_cod2 (f,(Frechet_Filter NAT))) holds
(lim_in_cod2 (f,(Frechet_Filter NAT))) . t = (lim_in_cod2 Rseq) . t :: thesis: verum
proof
let t be object ; :: thesis: ( t in dom (lim_in_cod2 (f,(Frechet_Filter NAT))) implies (lim_in_cod2 (f,(Frechet_Filter NAT))) . t = (lim_in_cod2 Rseq) . t )
assume t in dom (lim_in_cod2 (f,(Frechet_Filter NAT))) ; :: thesis: (lim_in_cod2 (f,(Frechet_Filter NAT))) . t = (lim_in_cod2 Rseq) . t
then reconsider t1 = t as Element of NAT ;
A4: {((lim_in_cod2 (f,(Frechet_Filter NAT))) . t1)} = lim_filter ((ProjMap1 (f,t1)),(Frechet_Filter NAT)) by A1, Def7;
lim_filter ((ProjMap1 (f,t1)),(Frechet_Filter NAT)) = {(lim (ProjMap1 (Rseq,t1)))} by A1, A3, A2, Th73
.= {((lim_in_cod2 Rseq) . t1)} by DBLSEQ_1:def 6 ;
hence (lim_in_cod2 (f,(Frechet_Filter NAT))) . t = (lim_in_cod2 Rseq) . t by A4, ZFMISC_1:3; :: thesis: verum
end;
end;
hence lim_in_cod2 (f,(Frechet_Filter NAT)) = lim_in_cod2 Rseq by FUNCT_1:def 11; :: thesis: verum