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

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

suppose f 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 f is empty ; :: thesis: dom2tuple f is PartFunc of (D *),D

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

end;

end;