for a, b being Real holds
( a + b = a + b & - a = - a & a - b = a - b & a * b = a * b ) ;