let X be set ; :: thesis: for A being Subset of X

for B being SetSequence of X st B is constant & the_value_of B = A holds

( B is convergent & lim B = A & lim_inf B = A & lim_sup B = A )

let A be Subset of X; :: thesis: for B being SetSequence of X st B is constant & the_value_of B = A holds

( B is convergent & lim B = A & lim_inf B = A & lim_sup B = A )

let B be SetSequence of X; :: thesis: ( B is constant & the_value_of B = A implies ( B is convergent & lim B = A & lim_inf B = A & lim_sup B = A ) )

assume A1: ( B is constant & the_value_of B = A ) ; :: thesis: ( B is convergent & lim B = A & lim_inf B = A & lim_sup B = A )

then for n being Nat holds (superior_setsequence B) . n = A by Th39;

then A2: lim_sup B = A by Th11;

for n being Nat holds (inferior_setsequence B) . n = A by A1, Th38;

then lim_inf B = A by Th10;

hence ( B is convergent & lim B = A & lim_inf B = A & lim_sup B = A ) by A2, KURATO_0:def 5; :: thesis: verum

for B being SetSequence of X st B is constant & the_value_of B = A holds

( B is convergent & lim B = A & lim_inf B = A & lim_sup B = A )

let A be Subset of X; :: thesis: for B being SetSequence of X st B is constant & the_value_of B = A holds

( B is convergent & lim B = A & lim_inf B = A & lim_sup B = A )

let B be SetSequence of X; :: thesis: ( B is constant & the_value_of B = A implies ( B is convergent & lim B = A & lim_inf B = A & lim_sup B = A ) )

assume A1: ( B is constant & the_value_of B = A ) ; :: thesis: ( B is convergent & lim B = A & lim_inf B = A & lim_sup B = A )

then for n being Nat holds (superior_setsequence B) . n = A by Th39;

then A2: lim_sup B = A by Th11;

for n being Nat holds (inferior_setsequence B) . n = A by A1, Th38;

then lim_inf B = A by Th10;

hence ( B is convergent & lim B = A & lim_inf B = A & lim_sup B = A ) by A2, KURATO_0:def 5; :: thesis: verum