set F = H₃(f);

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

suppose f is empty ; :: thesis: dom2tuple f is D -valued

then rng H₃(f) = {} ;
hence rng H₃(f) c= D by XBOOLE_1:2; :: according to RELAT_1:def 19 :: thesis: verum

end;

suppose A1: not f is empty ; :: thesis: dom2tuple f is D -valued

then A2: dom H₃(f) = 1 -tuples_on (dom f) by Def4;
thus rng H₃(f) c= D :: according to RELAT_1:def 19 :: thesis: verum

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng H₃(f) or y in D )
assume y in rng H₃(f) ; :: thesis: y in D
then consider a being object such that
A3: a in dom H₃(f) and
A4: H₃(f) . a = y by FUNCT_1:def 3;
consider x being set such that
A5: x in dom f and
A6: a = <*x*> by A2, A3, FINSEQ_2:135;
A7: H₃(f) . <*x*> = f . x by A1, A5, Def4;
f . x in rng f by A5, FUNCT_1:def 3;
hence y in D by A4, A6, A7; :: thesis: verum

end;

end;

end;