let X be non empty set ; :: thesis: for s being sequence of X st ( for i, j being Nat holds s . i = s . j ) holds
s is constant
let s be sequence of X; :: thesis: ( ( for i, j being Nat holds s . i = s . j ) implies s is constant )
assume for i, j being Nat holds s . i = s . j ; :: thesis: s is constant
then for x, y being set st x in dom s & y in dom s holds
s . x = s . y ;
hence s is constant by FUNCT_1:def 10; :: thesis: verum