per cases ( [a,b] in dom f or not [a,b] in dom f ) ;

suppose [a,b] in dom f ; :: thesis: f . (a,b) is Real

hence f . (a,b) is Real by PARTFUN1:4; :: thesis: verum

end;

suppose not [a,b] in dom f ; :: thesis: f . (a,b) is Real

then f . (a,b) = 0 by FUNCT_1:def 2;
hence f . (a,b) is Real ; :: thesis: verum

end;

end;