let V be RealLinearSpace; :: thesis: for u, y, w being VECTOR of V st u # y = u # w holds
y = w
let u, y, w be VECTOR of V; :: thesis: ( u # y = u # w implies y = w )
assume A1: u # y = u # w ; :: thesis: y = w
set p = u # y;
u + y = (u # y) + (u # y) by Def2
.= u + w by A1, Def2 ;
hence y = w by RLVECT_1:8; :: thesis: verum