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 Th48;
consider y being Vector of M such that
A1: x + y = ID M by Th45;
reconsider T = y as Element of setvect M by Th48;
x + y = W + T by Def13;
hence ex T being Element of setvect M st W + T = ID M by A1; :: thesis: verum