for seq being Real_Sequence st seq is non-zero holds
- seq is non-zero by Th42;