let seq be Real_Sequence; :: thesis: ( seq is V54() implies inferior_realsequence seq = seq )
assume seq is V54() ; :: 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