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