let S be SetSequence of T; :: thesis: ( S is constant implies ( S is convergent & S is V53() & S is V52() ) )
assume S is constant ; :: thesis: ( S is convergent & S is V53() & S is V52() )
then consider A being Subset of T such that
A1: for n being Nat holds S . n = A by VALUED_0:def 18;
A2: now :: thesis: for n being Nat holds S . (n + 1) c= S . n
let n be Nat; :: thesis: S . (n + 1) c= S . n
S . n = A by A1;
hence S . (n + 1) c= S . n by A1; :: thesis: verum
end;
A3: now :: thesis: for n being Nat holds S . n c= S . (n + 1)
let n be Nat; :: thesis: S . n c= S . (n + 1)
S . n = A by A1;
hence S . n c= S . (n + 1) by A1; :: thesis: verum
end;
( lim_sup S = A & lim_inf S = A ) by A1, Th14, Th15;
hence ( S is convergent & S is V53() & S is V52() ) by A3, A2; :: thesis: verum