dom (IncAddr F,k) = dom F by Def15;
hence IncAddr F,k is initial by AFINSQ_1:71; :: thesis: verum