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