for r being Real holds |.[**r,0**].| = |.r.| ;