let i, j be Nat; :: thesis: for X being set
for s being constant sequence of X holds s . i = s . j
let X be set ; :: thesis: for s being constant sequence of X holds s . i = s . j
let s be constant sequence of X; :: thesis: s . i = s . j

per cases ( X is empty or not X is empty ) ;

suppose A1: X is empty ; :: thesis: s . i = s . j

then s . i = {} ;
hence s . i = s . j by A1; :: thesis: verum

end;

suppose not X is empty ; :: thesis: s . i = s . j

then dom s = NAT by FUNCT_2:def 1;
then ( i in dom s & j in dom s ) by ORDINAL1:def 12;
hence s . i = s . j by FUNCT_1:def 10; :: thesis: verum

end;

end;