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