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 that
A1: A1 is convergent and
A2: A2 is convergent ; :: thesis: ( A1 (\) A2 is convergent & lim (A1 (\) A2) = (lim A1) \ (lim A2) )
A3: lim_sup (A1 (\) A2) = (lim A1) \ (lim A2) by A2, Th72;
lim_inf (A1 (\) A2) = (lim_inf A1) \ (lim_inf A2) by A2, Th64
.= (lim A1) \ (lim_inf A2) by A1, KURATO_0:def 5
.= (lim A1) \ (lim A2) by A2, KURATO_0:def 5 ;
hence ( A1 (\) A2 is convergent & lim (A1 (\) A2) = (lim A1) \ (lim A2) ) by A3, KURATO_0:def 5; :: thesis: verum