consider ADD being BinOp of (REAL n) such that

A1: for a, b being Element of REAL n holds ADD . (a,b) = a + b and

( ADD is commutative & ADD is associative ) by Lm1;

take ADD ; :: thesis: for a, b being Element of REAL n holds ADD . (a,b) = a + b

thus for a, b being Element of REAL n holds ADD . (a,b) = a + b by A1; :: thesis: verum

A1: for a, b being Element of REAL n holds ADD . (a,b) = a + b and

( ADD is commutative & ADD is associative ) by Lm1;

take ADD ; :: thesis: for a, b being Element of REAL n holds ADD . (a,b) = a + b

thus for a, b being Element of REAL n holds ADD . (a,b) = a + b by A1; :: thesis: verum