let k be natural number ; :: thesis: (Sgm (Seg (k + 0 ))) | (Seg k) = Sgm (Seg k)
( k + 0 = k & Seg k c= Seg k & card (Seg k) = k ) by FINSEQ_1:78;
then len (Sgm (Seg k)) = k by Th44;
then dom (Sgm (Seg k)) = Seg k by FINSEQ_1:def 3;
hence (Sgm (Seg (k + 0 ))) | (Seg k) = Sgm (Seg k) by RELAT_1:97; :: thesis: verum