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