let M be MidSp; :: thesis: for W, W1, W2 being Element of setvect M st W + W1 = ID M & W + W2 = ID M holds
W1 = W2
let W, W1, W2 be Element of setvect M; :: thesis: ( W + W1 = ID M & W + W2 = ID M implies W1 = W2 )
assume that
A1: W + W1 = ID M and
A2: W + W2 = ID M ; :: thesis: W1 = W2
reconsider x = W, y1 = W1, y2 = W2 as Vector of M by Th71;
x + y1 = W + W2 by A1, A2, Def14
.= x + y2 by Def14 ;
hence W1 = W2 by Th67; :: thesis: verum