let V be RealLinearSpace; :: thesis: for P, Q being Element of V
for a, b being Real st P <> Q & a * (P - Q) = b * (P - Q) holds
a = b
let P, Q be Element of V; :: thesis: for a, b being Real st P <> Q & a * (P - Q) = b * (P - Q) holds
a = b
let a, b be Real; :: thesis: ( P <> Q & a * (P - Q) = b * (P - Q) implies a = b )
assume that
A1: P <> Q and
A2: a * (P - Q) = b * (P - Q) ; :: thesis: a = b
P - Q <> 0. V by A1, RLVECT_1:21;
hence a = b by A2, RLVECT_1:37; :: thesis: verum