take len f ; :: according to FINSEQ_1:def 2 :: thesis: proj1 (Intervals (f,r)) = Seg (len f)
dom (Intervals (f,r)) = dom f by Def3;
hence proj1 (Intervals (f,r)) = Seg (len f) by FINSEQ_1:def 3; :: thesis: verum