let X be set ; :: thesis: for A1, A2 being SetSequence of X st A1 is convergent & A2 is convergent holds
( A1 (/\) A2 is convergent & lim (A1 (/\) A2) = (lim A1) /\ (lim A2) )
let A1, A2 be SetSequence of X; :: thesis: ( A1 is convergent & A2 is convergent implies ( A1 (/\) A2 is convergent & lim (A1 (/\) A2) = (lim A1) /\ (lim A2) ) )
assume A1: ( A1 is convergent & A2 is convergent ) ; :: thesis: ( A1 (/\) A2 is convergent & lim (A1 (/\) A2) = (lim A1) /\ (lim A2) )
A2: lim_inf (A1 (/\) A2) = (lim_inf A1) /\ (lim_inf A2) by Th60
.= (lim A1) /\ (lim_inf A2) by A1, KURATO_2:def 7
.= (lim A1) /\ (lim A2) by A1, KURATO_2:def 7 ;
lim_sup (A1 (/\) A2) = (lim_sup A1) /\ (lim_sup A2) by A1, Th71
.= (lim A1) /\ (lim A2) ;
hence ( A1 (/\) A2 is convergent & lim (A1 (/\) A2) = (lim A1) /\ (lim A2) ) by A2, KURATO_2:def 7; :: thesis: verum