let a be Real; :: thesis: for V being non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for v, w being Element of V st a <> 0 & a * v = a * w holds
v = w
let V be non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; :: thesis: for v, w being Element of V st a <> 0 & a * v = a * w holds
v = w
let v, w be Element of V; :: thesis: ( a <> 0 & a * v = a * w implies v = w )
assume that
A1: a <> 0 and
A2: a * v = a * w ; :: thesis: v = w
0. V = (a * v) - (a * w) by A2, Def10
.= a * (v - w) by Th34 ;
then v - w = 0. V by A1, Th11;
hence v = w by Th21; :: thesis: verum