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

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 + (vect (b, the Element of M)) = vect ( the Element of M, the Element of M) by A1, Th40

.= ID M by Th32 ;

hence ex v being Vector of M st u + v = ID M ; :: thesis: verum

let u be Vector of M; :: thesis: ex v being Vector of M st u + v = ID M

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 + (vect (b, the Element of M)) = vect ( the Element of M, the Element of M) by A1, Th40

.= ID M by Th32 ;

hence ex v being Vector of M st u + v = ID M ; :: thesis: verum