:: deftheorem Def8 defines Shift SIN_COS:def 8 :
for seq, b₂ being Complex_Sequence holds
( b₂ = Shift seq iff ( b₂ . 0 = 0 & ( for k being Nat holds b₂ . (k + 1) = seq . k ) ) );