defpred S_{1}[ Element of setvect M, Element of setvect M] means $1 + $2 = ID M;

A1: for W being Element of setvect M ex T being Element of setvect M st S_{1}[W,T]
by Th51;

consider o being UnOp of (setvect M) such that

A2: for W being Element of setvect M holds S_{1}[W,o . W]
from FUNCT_2:sch 3(A1);

take o ; :: thesis: for W being Element of setvect M holds W + (o . W) = ID M

thus for W being Element of setvect M holds W + (o . W) = ID M by A2; :: thesis: verum

A1: for W being Element of setvect M ex T being Element of setvect M st S

consider o being UnOp of (setvect M) such that

A2: for W being Element of setvect M holds S

take o ; :: thesis: for W being Element of setvect M holds W + (o . W) = ID M

thus for W being Element of setvect M holds W + (o . W) = ID M by A2; :: thesis: verum