let k be Nat; :: thesis: for y being object st Seg k = {y} holds
( k = 1 & y = 1 )
let y be object ; :: thesis: ( Seg k = {y} implies ( k = 1 & y = 1 ) )
assume A1: Seg k = {y} ; :: thesis: ( k = 1 & y = 1 )

now :: thesis: ( k = 1 & y = 1 )

per cases ( k = 0 or k <> 0 ) ;

suppose k = 0 ; :: thesis: ( k = 1 & y = 1 )

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

end;

suppose k <> 0 ; :: thesis: ( k = 1 & y = 1 )

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: verum

end;

end;

end;

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