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

now

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:5;
then 1 <= k by FINSEQ_1:3;
then Seg 1 c= Seg k by FINSEQ_1:7;
then Seg 1 = {y} by A1, ZFMISC_1:39;
hence ( k = 1 & y = 1 ) by A1, A2, FINSEQ_1:4, TARSKI:def 1, ZFMISC_1:6; :: thesis: verum

end;

end;

end;

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