:: deftheorem Def18 defines cos SIN_COS:def 18 :
for b₁ being Function of REAL,REAL holds
( b₁ = cos iff for d being Real holds b₁ . d = Re (Sum ((d * <i>) ExpSeq)) );