:: deftheorem Def16 defines sin SIN_COS:def 16 :
for b₁ being Function of REAL,REAL holds
( b₁ = sin iff for d being Real holds b₁ . d = Im (Sum ((d * <i>) ExpSeq)) );