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

dom (Intervals (f,r)) = dom f by Def3;

hence dom (Intervals (f,r)) = Seg (len f) by FINSEQ_1:def 3; :: thesis: verum