let Rseq be Function of ,REAL; :: thesis: for Y being non empty Hausdorff TopSpace
for f being Function of ,Y st ( for x being Element of NAT holds lim_filter ((ProjMap2 (f,x)),) <> {} ) & f = Rseq & Y = R^1 holds
lim_in_cod1 (f,) = lim_in_cod1 Rseq

let Y be non empty Hausdorff TopSpace; :: thesis: for f being Function of ,Y st ( for x being Element of NAT holds lim_filter ((ProjMap2 (f,x)),) <> {} ) & f = Rseq & Y = R^1 holds
lim_in_cod1 (f,) = lim_in_cod1 Rseq

let f be Function of ,Y; :: thesis: ( ( for x being Element of NAT holds lim_filter ((ProjMap2 (f,x)),) <> {} ) & f = Rseq & Y = R^1 implies lim_in_cod1 (f,) = lim_in_cod1 Rseq )
assume that
A1: for x being Element of NAT holds lim_filter ((ProjMap2 (f,x)),) <> {} and
A2: f = Rseq and
A3: Y = R^1 ; :: thesis: lim_in_cod1 (f,) = lim_in_cod1 Rseq
now :: thesis: ( dom (lim_in_cod1 (f,)) = dom (lim_in_cod1 Rseq) & ( for t being object st t in dom (lim_in_cod1 (f,)) holds
(lim_in_cod1 (f,)) . t = (lim_in_cod1 Rseq) . t ) )
dom (lim_in_cod1 (f,)) = NAT by FUNCT_2:def 1;
hence dom (lim_in_cod1 (f,)) = dom (lim_in_cod1 Rseq) by FUNCT_2:def 1; :: thesis: for t being object st t in dom (lim_in_cod1 (f,)) holds
(lim_in_cod1 (f,)) . t = (lim_in_cod1 Rseq) . t

thus for t being object st t in dom (lim_in_cod1 (f,)) holds
(lim_in_cod1 (f,)) . t = (lim_in_cod1 Rseq) . t :: thesis: verum
proof
let t be object ; :: thesis: ( t in dom (lim_in_cod1 (f,)) implies (lim_in_cod1 (f,)) . t = (lim_in_cod1 Rseq) . t )
assume t in dom (lim_in_cod1 (f,)) ; :: thesis: (lim_in_cod1 (f,)) . t = (lim_in_cod1 Rseq) . t
then reconsider t1 = t as Element of NAT ;
A4: {((lim_in_cod1 (f,)) . t1)} = lim_filter ((ProjMap2 (f,t1)),) by ;
lim_filter ((ProjMap2 (f,t1)),) = {(lim (ProjMap2 (Rseq,t1)))} by A1, A3, A2, Th74
.= {((lim_in_cod1 Rseq) . t1)} by DBLSEQ_1:def 5 ;
hence (lim_in_cod1 (f,)) . t = (lim_in_cod1 Rseq) . t by ; :: thesis: verum
end;
end;
hence lim_in_cod1 (f,) = lim_in_cod1 Rseq by FUNCT_1:def 11; :: thesis: verum