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_{1}( 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_{1}(a,b)
from BINOP_1:sch 4();

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

( ( for a, b being Element of REAL n holds ADD . (a,b) = a + b ) & ADD is commutative & ADD is associative )

deffunc H

consider ADD being BinOp of (REAL n) such that

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

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

then A2:
ADD is associative
;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;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

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

then
ADD is commutative
;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;thus ADD . (a,b) = a + b by A1

.= ADD . (b,a) by A1 ; :: thesis: verum

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