let M be MidSp; :: thesis: for W being Element of setvect M ex T being Element of setvect M st W + T = ID M
let W be Element of setvect M; :: thesis: ex T being Element of setvect M st W + T = ID M
reconsider x = W as Vector of M by Th71;
consider y being Vector of M such that
A1: x + y = ID M by Th65;
reconsider T = y as Element of setvect M by Th71;
x + y = W + T by Def14;
hence ex T being Element of setvect M st W + T = ID M by A1; :: thesis: verum