for c being XFinSequence of REAL ex absc being XFinSequence of REAL st
( absc = |.c.| & ( for n being Nat holds (seq_p c) . n <= (seq_p absc) . n ) )