for seq being Real_Sequence st seq is decreasing holds
for n being Nat st 0 < n holds
seq . n < seq . 0 by Th4;