theorem Th14: :: WALLIS01:17

for A being non empty set
for a being Element of REAL
for f being Element of (RAlgebra A) holds a (#) (@ f) = a * f by FUNCSDOM:30;