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
A5: for n, m being Element of NAT holds seq . n = seq . m and
A6: not seq is constant ; :: thesis: contradiction

now

let n be Nat; :: thesis: contradiction
consider n1 being Nat such that
A7: seq . n1 <> seq . n by A6, VALUED_0:def 18;
( n1 in NAT & n in NAT ) by ORDINAL1:def 13;
hence contradiction by A5, A7; :: thesis: verum

end;

hence contradiction ; :: thesis: verum