consider ADD being BinOp of (REAL n) such that
A1: ( ( for a, b being Element of REAL n holds ADD . a,b = a + b ) & ADD is commutative & ADD is associative ) by Lm1;
thus ( Euclid_add n is commutative & Euclid_add n is associative ) by A1, Def1; :: thesis: verum