let D be set ; :: thesis: for f being BinOp of D holds dom2tuple f is PartFunc of (D *),D
let f be BinOp of D; :: thesis: dom2tuple f is PartFunc of (D *),D
set F = dom2tuple f;

per cases ( D is empty or not D is empty ) ;

suppose D is empty ; :: thesis: dom2tuple f is PartFunc of (D *),D

then dom2tuple f = {} ;
hence dom2tuple f is PartFunc of (D *),D by XBOOLE_1:2; :: thesis: verum

end;

suppose not D is empty ; :: thesis: dom2tuple f is PartFunc of (D *),D

then A1: dom (dom2tuple f) = 2 -tuples_on D by Def5;
rng (dom2tuple f) c= D ;
hence dom2tuple f is PartFunc of (D *),D by A1, RELSET_1:4, FINSEQ_2:134; :: thesis: verum

end;

end;