let X be set ; :: thesis:
let A1, A2 be SetSequence of X; :: thesis:
A1: for A1, A2 being SetSequence of X st A1 is convergent holds
lim_inf (A1 (\+\) A2) c= (lim_inf A1) \+\ (lim_inf A2)

proof

let A1, A2 be SetSequence of X; :: thesis:
assume A2: A1 is convergent ; :: thesis:
thus lim_inf (A1 (\+\) A2) c= (lim_inf A1) \+\ (lim_inf A2) :: thesis:

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in lim_inf (A1 (\+\) A2) ; :: thesis:
then consider n1 being Nat such that
A3: for k being Nat holds x in (A1 (\+\) A2) . (n1 + k) by KURATO_0:4;

A4: now :: thesis:

let k be Nat; :: thesis:
x in (A1 (\+\) A2) . (n1 + k) by A3;
then x in (A1 . (n1 + k)) \+\ (A2 . (n1 + k)) by Def4;
hence ( ( x in A1 . (n1 + k) & not x in A2 . (n1 + k) ) or ( not x in A1 . (n1 + k) & x in A2 . (n1 + k) ) ) by XBOOLE_0:1; :: thesis:

end;

assume A5: not x in (lim_inf A1) \+\ (lim_inf A2) ; :: thesis:

per cases by A5, XBOOLE_0:1;

suppose A6: ( not x in lim_inf A1 & not x in lim_inf A2 ) ; :: thesis:

then not x in lim_sup A1 by A2, KURATO_0:def 5;
then consider n2 being Nat such that
A7: for k being Nat holds not x in A1 . (n2 + k) by KURATO_0:5;
consider k1 being Nat such that
A8: not x in A2 . ((n1 + n2) + k1) by A6, KURATO_0:4;
A9: ( ( x in A1 . (n1 + (n2 + k1)) & not x in A2 . (n1 + (n2 + k1)) ) or ( not x in A1 . (n1 + (n2 + k1)) & x in A2 . (n1 + (n2 + k1)) ) ) by A4;
not x in A1 . (n2 + (n1 + k1)) by A7;
hence contradiction by A8, A9; :: thesis:

end;

suppose A10: ( x in lim_inf A1 & x in lim_inf A2 ) ; :: thesis:

then consider n3 being Nat such that
A11: for k being Nat holds x in A2 . (n3 + k) by KURATO_0:4;
consider n2 being Nat such that
A12: for k being Nat holds x in A1 . (n2 + k) by A10, KURATO_0:4;
A13: ( ( x in A1 . (n1 + (n2 + n3)) & not x in A2 . (n1 + (n2 + n3)) ) or ( not x in A1 . (n1 + (n2 + n3)) & x in A2 . (n1 + (n2 + n3)) ) ) by A4;
A14: x in A2 . (n3 + (n1 + n2)) by A11;
x in A1 . (n2 + (n1 + n3)) by A12;
hence contradiction by A14, A13; :: thesis:

end;

end;

end;

end;

assume A15: ( A1 is convergent or A2 is convergent ) ; :: thesis:

per cases by A15;

suppose A1 is convergent ; :: thesis:

hence lim_inf (A1 (\+\) A2) c= (lim_inf A1) \+\ (lim_inf A2) by A1; :: thesis:

end;

suppose A2 is convergent ; :: thesis:

hence lim_inf (A1 (\+\) A2) c= (lim_inf A1) \+\ (lim_inf A2) by A1; :: thesis:

end;

end;