theorem :: CFDIFF_1:4

for seq being Complex_Sequence holds
( seq is constant iff for n, m being Nat holds seq . n = seq . m )