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
consider a being Element of M;
consider b being Element of M such that
A1: u = vect (a,b) by Th55;
u + (vect (b,a)) = vect (a,a) by A1, Th60
.= ID M by Th50 ;
hence ex v being Vector of M st u + v = ID M ; :: thesis: verum