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 V29()
let s be sequence of X; :: thesis: ( ( for i, j being Nat holds s . i = s . j ) implies s is V29() )
assume for i, j being Nat holds s . i = s . j ; :: thesis: s is V29()
then for x, y being set st x in dom s & y in dom s holds
s . x = s . y ;
hence s is V29() by FUNCT_1:def 10; :: thesis: verum