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