set F = dom2tuple f;
thus rng (dom2tuple f) c= D :: according to RELAT_1:def 19 :: thesis: verum

proof

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

suppose D is empty ; :: thesis: rng (dom2tuple f) c= D

then dom2tuple f = {} by Def5;
then rng (dom2tuple f) = {} ;
hence rng (dom2tuple f) c= D by XBOOLE_1:2; :: thesis: verum

end;

suppose A1: not D is empty ; :: thesis: rng (dom2tuple f) c= D

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (dom2tuple f) or y in D )
assume y in rng (dom2tuple f) ; :: thesis: y in D
then consider x being object such that
A2: x in dom (dom2tuple f) and
A3: (dom2tuple f) . x = y by FUNCT_1:def 3;
dom (dom2tuple f) = 2 -tuples_on D by A1, Def5;
then consider a, b being object such that
A4: ( a in D & b in D ) and
A5: x = <*a,b*> by A2, FINSEQ_2:137;
reconsider a = a, b = b as Element of D by A4;
dom f = [:D,D:] by A1, FUNCT_2:def 1;
then [a,b] in dom f by A1, ZFMISC_1:87;
then (dom2tuple f) . <*a,b*> = f . (a,b) by A1, Def5;
hence y in D by A1, A3, A5; :: thesis: verum

end;

end;

end;