let M be MidSp; :: thesis: for u being Vector of M holds u + (ID M) = u
let u be Vector of M; :: thesis: u + (ID M) = u
set a = the Element of M;
consider b being Element of M such that
A1: u = vect ( the Element of M,b) by Th55;
u + (ID M) = (vect ( the Element of M,b)) + (vect (b,b)) by A1, Th50
.= u by A1, Th60 ;
hence u + (ID M) = u ; :: thesis: verum