let i be Nat; :: thesis: for k being Element of Seg i holds (idseq i) . k = k
let k be Element of Seg i; :: thesis: (idseq i) . k = k

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

suppose i <> 0 ; :: thesis: (idseq i) . k = k

hence (idseq i) . k = k by FUNCT_1:35; :: thesis: verum

end;

suppose A2: i = 0 ; :: thesis: (idseq i) . k = k

then A1: k = 0 by SUBSET_1:def 2;
dom (idseq i) = 0 by A2;
hence (idseq i) . k = k by A1, FUNCT_1:def 4; :: thesis: verum

end;

end;