theorem Th18: :: WALLIS01:21

for A being non empty set
for f, g being Element of (RAlgebra A) holds f + g = (@ f) + (@ g) by FUNCSDOM:28;