let h, g be Element of G; :: according to RLVECT_1:def 2 :: thesis: h + g = g + h
reconsider A = h, B = g as Real ;
thus h + g = B + A by BINOP_2:def 9
.= g + h by BINOP_2:def 9 ; :: thesis: verum