per cases ( n in dom F or not n in dom F ) ;
suppose n in dom F ; :: thesis: F . n is interval Subset of REAL
then F . n in Family_of_Intervals by PARTFUN1:4;
then ex I being Interval st F . n = I by MEASUR10:def 1;
hence F . n is interval Subset of REAL ; :: thesis: verum
end;
suppose not n in dom F ; :: thesis: F . n is interval Subset of REAL
then ( F . n = {} & {} c= REAL ) by FUNCT_1:def 2;
hence F . n is interval Subset of REAL ; :: thesis: verum
end;
end;