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;