:: deftheorem Def2 defines Prod_real_n SIN_COS:def 2 :
for b₁ being Real_Sequence holds
( b₁ = Prod_real_n iff ( b₁ . 0 = 1 & ( for n being Nat holds b₁ . (n + 1) = (b₁ . n) * (n + 1) ) ) );