let k be natural number ; :: thesis: (Sgm (Seg (k + 0))) | (Seg k) = Sgm (Seg k)
card (Seg k) = k by FINSEQ_1:57;
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:68; :: thesis: verum