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 A1: ( W + W1 = ID M & W + W2 = ID M ) ; :: thesis: W1 = W2
reconsider x = W, y1 = W1, y2 = W2 as Vector of M by Th48;
x + y1 = W + W2 by A1, Def13
.= x + y2 by Def13 ;
hence W1 = W2 by Th47; :: thesis: verum