per cases ( ( a in [.0,1.] & b in [.0,1.] ) or not a in [.0,1.] or not b in [.0,1.] ) ;

suppose ( a in [.0,1.] & b in [.0,1.] ) ; :: thesis: f . (a,b) is real

then f . (a,b) in [.0,1.] by BINOP_1:17;
hence f . (a,b) is real ; :: thesis: verum

end;

suppose ( not a in [.0,1.] or not b in [.0,1.] ) ; :: thesis: f . (a,b) is real

then not [a,b] in dom f by ZFMISC_1:87;
hence f . (a,b) is real by FUNCT_1:def 2; :: thesis: verum

end;

end;