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

now

let n be Nat; :: thesis: contradiction
consider n1 being Nat such that
A3: seq . n1 <> seq . n by A2, VALUED_0:def 18;
( n1 in NAT & n in NAT ) by ORDINAL1:def 12;
hence contradiction by A1, A3; :: thesis: verum

end;

hence contradiction ; :: thesis: verum