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 Th32;

hence (a,(0. W)) . W = a by Th32; :: thesis: verum

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 Th32;

hence (a,(0. W)) . W = a by Th32; :: thesis: verum