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