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