let n, k be natural number ; :: thesis: (idseq (n + k)) | (Seg n) = idseq n
( Sgm (Seg (n + k)) = idseq (n + k) & Sgm (Seg n) = idseq n & (Sgm (Seg (n + k))) | (Seg n) = Sgm (Seg n) ) by Lm4, Th54;
hence (idseq (n + k)) | (Seg n) = idseq n ; :: thesis: verum