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