let seq be Complex_Sequence; :: thesis: ( seq is constant iff for n, m being Nat holds seq . n = seq . m )
thus ( seq is constant implies for n, m being Nat holds seq . n = seq . m ) by VALUED_0:23; :: thesis: ( ( for n, m being Nat holds seq . n = seq . m ) implies seq is constant )
assume that
A1: for n, m being Nat holds seq . n = seq . m and
A2: not seq is constant ; :: thesis: contradiction

now :: thesis: for n being Nat holds contradiction

let n be Nat; :: thesis: contradiction
consider n1 being Nat such that
A3: seq . n1 <> seq . n by A2, VALUED_0:def 18;
thus contradiction by A1, A3; :: thesis: verum

end;

hence contradiction ; :: thesis: verum