let n be Nat; 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 H1( 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) = H1(a,b)
from BINOP_1:sch 4();
now 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;
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
;
verum end;
then A2:
ADD is associative
;
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; verum