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

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