let seq be Real_Sequence; :: thesis: ( seq is non-decreasing implies inferior_realsequence seq = seq )
assume seq is non-decreasing ; :: thesis: inferior_realsequence seq = seq
then for n being Element of NAT holds (inferior_realsequence seq) . n = seq . n by Lm2;
hence inferior_realsequence seq = seq by FUNCT_2:63; :: thesis: verum