theorem Th17: :: WALLIS01:20

for A being non empty set
for f being Element of (RAlgebra A) holds
( (- 1) * f = (- 1) (#) (@ f) & @ ((- 1) * f) = - (@ f) & 0. (RAlgebra A) = 0 (#) (@ f) )