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