for M being MidSp
for W being ATLAS of M
for a being Point of M holds (a,(0. W)) . W = a