let n be Nat; :: thesis: 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 )
deffunc H₁( Element of REAL n, Element of REAL n) -> Element of REAL n = $1 + $2;
consider ADD being BinOp of (REAL n) such that
A1: for a, b being Element of REAL n holds ADD . (a,b) = H₁(a,b) from BINOP_1:sch 4();

now :: thesis: for a, b, c being Element of REAL n holds ADD . (a,(ADD . (b,c))) = ADD . ((ADD . (a,b)),c)

let a, b, c be Element of REAL n; :: thesis: ADD . (a,(ADD . (b,c))) = ADD . ((ADD . (a,b)),c)
reconsider a1 = a, b1 = b, c1 = c as Element of n -tuples_on REAL by EUCLID:def 1;
thus ADD . (a,(ADD . (b,c))) = a + (ADD . (b,c)) by A1
.= a + (b + c) by A1
.= (a1 + b1) + c1 by RVSUM_1:15
.= (ADD . (a,b)) + c by A1
.= ADD . ((ADD . (a,b)),c) by A1 ; :: thesis: verum

end;

then A2: ADD is associative ;

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

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

end;

then ADD is commutative ;
hence 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 A1, A2; :: thesis: verum