let M be MidSp; :: thesis: for W being ATLAS of M
for a being Point of M holds a,(0. W) . W = a
let W be ATLAS of M; :: thesis: for a being Point of M holds a,(0. W) . W = a
let a be Point of M; :: thesis: a,(0. W) . W = a
W . a,a = 0. W by Th39;
hence a,(0. W) . W = a by Th39; :: thesis: verum