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:27; :: 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 4;
hence f . a,b is Real ; :: thesis: verum

end;

end;