let Rseq be Function of [:NAT,NAT:],REAL; :: thesis: ( lim_filter ((# Rseq),<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) <> {} implies ex x being Real st lim_filter ((# Rseq),<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) = {x} )
assume A1: lim_filter ((# Rseq),<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) <> {} ; :: thesis: ex x being Real st lim_filter ((# Rseq),<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) = {x}
reconsider s1 = Rseq as Function of [:NAT,NAT:], the carrier of R^1 ;
consider x being object such that
A2: lim_filter ((# Rseq),<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) = {x} by A1, ZFMISC_1:131;
x in lim_filter ((# Rseq),<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) by A2, TARSKI:def 1;
hence ex x being Real st lim_filter ((# Rseq),<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) = {x} by A2; :: thesis: verum