:: deftheorem defines @ WALLIS01:def 3 :
for A being set
for f being Element of (RAlgebra A) holds @ f = f;