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

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:32
.= (ADD . a,b) + c by A1
.= ADD . (ADD . a,b),c by A1 ; :: thesis: verum

end;

then A2: ADD is associative by BINOP_1:def 3;

now

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 by BINOP_1:def 2;
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