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

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