let X be set ; :: thesis: for A1, A2 being SetSequence of X st A1 is convergent & A2 is convergent holds
lim_inf (A1 (\+\) A2) = (lim_inf A1) \+\ (lim_inf A2)
let A1, A2 be SetSequence of X; :: thesis: ( A1 is convergent & A2 is convergent implies lim_inf (A1 (\+\) A2) = (lim_inf A1) \+\ (lim_inf A2) )
assume that
A1: A1 is convergent and
A2: A2 is convergent ; :: thesis: lim_inf (A1 (\+\) A2) = (lim_inf A1) \+\ (lim_inf A2)
thus lim_inf (A1 (\+\) A2) c= (lim_inf A1) \+\ (lim_inf A2) by A1, Th65; :: according to XBOOLE_0:def 10 :: thesis: (lim_inf A1) \+\ (lim_inf A2) c= lim_inf (A1 (\+\) A2)
thus (lim_inf A1) \+\ (lim_inf A2) c= lim_inf (A1 (\+\) A2) :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (lim_inf A1) \+\ (lim_inf A2) or x in lim_inf (A1 (\+\) A2) )
assume A3: x in (lim_inf A1) \+\ (lim_inf A2) ; :: thesis: x in lim_inf (A1 (\+\) A2)

per cases ( ( x in lim_inf A1 & not x in lim_inf A2 ) or ( not x in lim_inf A1 & x in lim_inf A2 ) ) by A3, XBOOLE_0:1;

suppose A4: ( x in lim_inf A1 & not x in lim_inf A2 ) ; :: thesis: x in lim_inf (A1 (\+\) A2)

then not x in lim_sup A2 by A2, KURATO_0:def 5;
then consider n2 being Nat such that
A5: for k being Nat holds not x in A2 . (n2 + k) by KURATO_0:5;
consider n1 being Nat such that
A6: for k being Nat holds x in A1 . (n1 + k) by A4, KURATO_0:4;

now :: thesis: for k being Nat holds x in (A1 (\+\) A2) . ((n1 + n2) + k)

let k be Nat; :: thesis: x in (A1 (\+\) A2) . ((n1 + n2) + k)
( x in A1 . (n1 + (n2 + k)) & not x in A2 . (n2 + (n1 + k)) ) by A6, A5;
then x in (A1 . ((n1 + n2) + k)) \+\ (A2 . ((n1 + n2) + k)) by XBOOLE_0:1;
hence x in (A1 (\+\) A2) . ((n1 + n2) + k) by Def4; :: thesis: verum

end;

hence x in lim_inf (A1 (\+\) A2) by KURATO_0:4; :: thesis: verum

end;

suppose A7: ( not x in lim_inf A1 & x in lim_inf A2 ) ; :: thesis: x in lim_inf (A1 (\+\) A2)

then not x in lim_sup A1 by A1, KURATO_0:def 5;
then consider n3 being Nat such that
A8: for k being Nat holds not x in A1 . (n3 + k) by KURATO_0:5;
consider n4 being Nat such that
A9: for k being Nat holds x in A2 . (n4 + k) by A7, KURATO_0:4;

now :: thesis: for k being Nat holds x in (A1 (\+\) A2) . ((n3 + n4) + k)

let k be Nat; :: thesis: x in (A1 (\+\) A2) . ((n3 + n4) + k)
( not x in A1 . (n3 + (n4 + k)) & x in A2 . (n4 + (n3 + k)) ) by A8, A9;
then x in (A1 . ((n3 + n4) + k)) \+\ (A2 . ((n3 + n4) + k)) by XBOOLE_0:1;
hence x in (A1 (\+\) A2) . ((n3 + n4) + k) by Def4; :: thesis: verum

end;

hence x in lim_inf (A1 (\+\) A2) by KURATO_0:4; :: thesis: verum

end;

end;

end;