dom x = Seg 4 by FINSEQ_2:124;
then len x = 4 by FINSEQ_1:def 3;
hence pi_id x = x by FINSEQ_4:76; :: thesis: verum