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