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