set G = addMagma(# REAL,addreal #);
thus
for h, g, f being Element of addMagma(# REAL,addreal #) holds (h + g) + f = h + (g + f)
RLVECT_1:def 3 addMagma(# REAL,addreal #) is addGroup-like
reconsider e = 0 as Element of addMagma(# REAL,addreal #) by XREAL_0:def 1;
take
e
; GROUP_1A:def 2 for h being Element of addMagma(# REAL,addreal #) holds
( h + e = h & e + h = h & ex g being Element of addMagma(# REAL,addreal #) st
( h + g = e & g + h = e ) )
let h be Element of addMagma(# REAL,addreal #); ( h + e = h & e + h = h & ex g being Element of addMagma(# REAL,addreal #) st
( h + g = e & g + h = e ) )
reconsider A = h as Real ;
thus h + e =
A + 0
by BINOP_2:def 9
.=
h
; ( e + h = h & ex g being Element of addMagma(# REAL,addreal #) st
( h + g = e & g + h = e ) )
thus e + h =
0 + A
by BINOP_2:def 9
.=
h
; ex g being Element of addMagma(# REAL,addreal #) st
( h + g = e & g + h = e )
reconsider g = - A as Element of addMagma(# REAL,addreal #) by XREAL_0:def 1;
take
g
; ( h + g = e & g + h = e )
thus h + g =
A + (- A)
by BINOP_2:def 9
.=
e
; g + h = e
thus g + h =
(- A) + A
by BINOP_2:def 9
.=
e
; verum