let M be MidSp; :: thesis: for u being Vector of M ex v being Vector of M st u + v = ID M
let u be Vector of M; :: thesis: ex v being Vector of M st u + v = ID M
set a = the Element of M;
consider b being Element of M such that
A1: u = vect ( the Element of M,b) by Th35;
u + (vect (b, the Element of M)) = vect ( the Element of M, the Element of M) by A1, Th40
.= ID M by Th32 ;
hence ex v being Vector of M st u + v = ID M ; :: thesis: verum