let k be Nat; :: 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 Th37;
then dom (Sgm (Seg k)) = Seg k by FINSEQ_1:def 3;
hence (Sgm (Seg (k + 0))) | (Seg k) = Sgm (Seg k) ; :: thesis: verum