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