:: deftheorem defines Phi E_TRANS1:def 10 :
for f being Element of the carrier of (Polynom-Ring INT.Ring) holds Phi f = exp_R1 (#) ('F' f);