set F = H₃(f);

now :: thesis: dom H₃(f) c= 1 -tuples_on D

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

suppose f is empty ; :: thesis: dom H₃(f) c= 1 -tuples_on D

then dom H₃(f) = {} ;
hence dom H₃(f) c= 1 -tuples_on D by XBOOLE_1:2; :: thesis: verum

end;

suppose not f is empty ; :: thesis: dom H₃(f) c= 1 -tuples_on D

then A1: dom H₃(f) = 1 -tuples_on (dom f) by Def4;
thus dom H₃(f) c= 1 -tuples_on D :: thesis: verum

proof

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

end;

end;

end;

end;

hence dom2tuple f is homogeneous by COMPUT_1:16; :: thesis: verum