for seq being Real_Sequence st seq is V55() holds
superior_realsequence seq = seq