let X be set ; :: thesis: for A being Subset of X
for A1 being SetSequence of X st A1 is convergent holds
( A (\+\) A1 is convergent & lim (A (\+\) A1) = A \+\ (lim A1) )
let A be Subset of X; :: thesis: for A1 being SetSequence of X st A1 is convergent holds
( A (\+\) A1 is convergent & lim (A (\+\) A1) = A \+\ (lim A1) )
let A1 be SetSequence of X; :: thesis: ( A1 is convergent implies ( A (\+\) A1 is convergent & lim (A (\+\) A1) = A \+\ (lim A1) ) )
assume A1: A1 is convergent ; :: thesis: ( A (\+\) A1 is convergent & lim (A (\+\) A1) = A \+\ (lim A1) )
then A2: lim_inf (A (\+\) A1) = A \+\ (lim_inf A1) by Th80
.= A \+\ (lim A1) by A1, KURATO_0:def 5 ;
then lim_sup (A (\+\) A1) = lim_inf (A (\+\) A1) by A1, Th87;
hence ( A (\+\) A1 is convergent & lim (A (\+\) A1) = A \+\ (lim A1) ) by A2, KURATO_0:def 5; :: thesis: verum