defpred S₁[ Element of setvect M, Element of setvect M, Element of setvect M] means $3 = $1 + $2;
A1: for u1, v1 being Element of setvect M ex W being Element of setvect M st S₁[u1,v1,W] ;
consider o being BinOp of (setvect M) such that
A2: for u1, v1 being Element of setvect M holds S₁[u1,v1,o . (u1,v1)] from BINOP_1:sch 3(A1);
take o ; :: thesis: for u1, v1 being Element of setvect M holds o . (u1,v1) = u1 + v1
thus for u1, v1 being Element of setvect M holds o . (u1,v1) = u1 + v1 by A2; :: thesis: verum