ex ADD being BinOp of (REAL n) st
( ( for a, b being Element of REAL n holds ADD . (a,b) = a + b ) & ADD is commutative & ADD is associative ) by Lm1;
hence ( Euclid_add n is commutative & Euclid_add n is associative ) by Def1; :: thesis: verum