let V be RealLinearSpace; :: thesis: for w, y being VECTOR of V
for a being Element of (DTrSpace (V,w,y)) holds a # a = a
let w, y be VECTOR of V; :: thesis: for a being Element of (DTrSpace (V,w,y)) holds a # a = a
let a be Element of (DTrSpace (V,w,y)); :: thesis: a # a = a
reconsider u = a as VECTOR of V ;
u # u = u ;
hence a # a = a by Def8; :: thesis: verum