defpred S₁[ 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₁[W,T] by Th51;
consider o being UnOp of (setvect M) such that
A2: for W being Element of setvect M holds S₁[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