set F = H₃(f);

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

suppose f is empty ; :: thesis: dom2tuple f is D * -defined

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

end;

suppose not f is empty ; :: thesis: dom2tuple f is D * -defined

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

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in dom H₃(f) or a in D * )
assume a in dom H₃(f) ; :: thesis: a in D *
then consider x being set such that
A2: x in dom f and
A3: a = <*x*> by A1, FINSEQ_2:135;
reconsider D = D as non empty set by A2;
reconsider x = x as Element of D by A2;
<*x*> is FinSequence of D ;
hence a in D * by A3, FINSEQ_1:def 11; :: thesis: verum

end;

end;

end;