for seq being Real_Sequence st seq is V96() holds
inferior_realsequence seq is V54() by Th48;