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