theorem :: TOPREAL6:23
for a being Real holds
( |.|[0,a]|.| = |.a.| & |.|[a,0]|.| = |.a.| )