theorem :: RINFSUP2:6

for seq being ExtREAL_sequence st seq is real-valued holds
seq is Real_Sequence by FUNCT_2:6;