let k be Nat; :: thesis:
let y be object ; :: thesis:
assume A1: Seg k = {y} ; :: thesis:

now :: thesis:

per cases ;

suppose k = 0 ; :: thesis:

hence ( k = 1 & y = 1 ) by A1; :: thesis:

end;

suppose k <> 0 ; :: thesis:

then A2: k in Seg k by FINSEQ_1:3;
then 1 <= k by FINSEQ_1:1;
then Seg 1 c= Seg k by FINSEQ_1:5;
then Seg 1 = {y} by A1, ZFMISC_1:33;
hence ( k = 1 & y = 1 ) by A1, A2, FINSEQ_1:2, TARSKI:def 1, ZFMISC_1:3; :: thesis:

end;

end;

end;

hence ( k = 1 & y = 1 ) ; :: thesis: