theorem Th19: :: WALLIS01:22

for f, g being Element of (RAlgebra REAL) holds f - g = (@ f) - (@ g)