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

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