let seq be ExtREAL_sequence; :: thesis: ( seq is convergent implies ( lim seq = lim_inf seq & lim seq = lim_sup seq ) )
set a = lim_inf seq;
assume seq is convergent ; :: thesis: ( lim seq = lim_inf seq & lim seq = lim_sup seq )
then A1: lim_inf seq = lim_sup seq by Th40;
per cases ( lim_inf seq in REAL or lim_inf seq = +infty or lim_inf seq = -infty ) by XXREAL_0:14;
suppose lim_inf seq in REAL ; :: thesis: ( lim seq = lim_inf seq & lim seq = lim_sup seq )
hence ( lim seq = lim_inf seq & lim seq = lim_sup seq ) by A1, Lm7; :: thesis: verum
end;
suppose lim_inf seq = +infty ; :: thesis: ( lim seq = lim_inf seq & lim seq = lim_sup seq )
hence ( lim seq = lim_inf seq & lim seq = lim_sup seq ) by A1, Lm5; :: thesis: verum
end;
suppose lim_inf seq = -infty ; :: thesis: ( lim seq = lim_inf seq & lim seq = lim_sup seq )
hence ( lim seq = lim_inf seq & lim seq = lim_sup seq ) by A1, Lm6; :: thesis: verum
end;
end;