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