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