:: deftheorem Def5 defines rExpSeq SIN_COS:def 5 :
for a being Real
for b₂ being Real_Sequence holds
( b₂ = a rExpSeq iff for n being Nat holds b₂ . n = (a |^ n) / (n !) );