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