:: deftheorem Def22 defines exp_R SIN_COS:def 22 :
for b₁ being Function of REAL,REAL holds
( b₁ = exp_R iff for d being Real holds b₁ . d = Sum (d rExpSeq) );