for r being Real holds r * <e1> = |[r,0,0]|