theorem Th13: :: WALLIS01:16

for A being non empty set
for f, g being Element of (RAlgebra A) holds
( f * g = (@ f) (#) (@ g) & @ (f * g) = (@ f) (#) (@ g) ) by FUNCSDOM:29;