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 Th35;

u + (ID M) = (vect ( the Element of M,b)) + (vect (b,b)) by A1, Th32

.= u by A1, Th40 ;

hence u + (ID M) = u ; :: thesis: verum

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 Th35;

u + (ID M) = (vect ( the Element of M,b)) + (vect (b,b)) by A1, Th32

.= u by A1, Th40 ;

hence u + (ID M) = u ; :: thesis: verum