let X be set ; :: thesis: for A1, A2 being SetSequence of X st ( A1 is convergent or A2 is convergent ) holds
lim_inf (A1 (\+\) A2) c= (lim_inf A1) \+\ (lim_inf A2)
let A1, A2 be SetSequence of X; :: thesis: ( ( A1 is convergent or A2 is convergent ) implies lim_inf (A1 (\+\) A2) c= (lim_inf A1) \+\ (lim_inf A2) )
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: ( A1 is convergent implies lim_inf (A1 (\+\) A2) c= (lim_inf A1) \+\ (lim_inf A2) )
assume A2: A1 is convergent ; :: thesis: lim_inf (A1 (\+\) A2) c= (lim_inf A1) \+\ (lim_inf A2)
thus lim_inf (A1 (\+\) A2) c= (lim_inf A1) \+\ (lim_inf A2) :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in lim_inf (A1 (\+\) A2) or x in (lim_inf A1) \+\ (lim_inf A2) )
assume x in lim_inf (A1 (\+\) A2) ; :: thesis: x in (lim_inf A1) \+\ (lim_inf A2)
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: for k being Nat holds
( ( x in A1 . (n1 + k) & not x in A2 . (n1 + k) ) or ( not x in A1 . (n1 + k) & x in A2 . (n1 + k) ) )

let k be Nat; :: thesis: ( ( x in A1 . (n1 + k) & not x in A2 . (n1 + k) ) or ( not x in A1 . (n1 + k) & x in A2 . (n1 + k) ) )
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: verum

end;

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

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

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

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: verum

end;

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

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: verum

end;

end;

end;

end;

assume A15: ( A1 is convergent or A2 is convergent ) ; :: thesis: lim_inf (A1 (\+\) A2) c= (lim_inf A1) \+\ (lim_inf A2)

per cases ( A1 is convergent or A2 is convergent ) by A15;

suppose A1 is convergent ; :: thesis: lim_inf (A1 (\+\) A2) c= (lim_inf A1) \+\ (lim_inf A2)

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

end;

suppose A2 is convergent ; :: thesis: lim_inf (A1 (\+\) A2) c= (lim_inf A1) \+\ (lim_inf A2)

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

end;

end;