assume not IncAddr (F,k) is empty ; :: thesis: contradiction
then reconsider f = IncAddr (F,k) as non empty Function ;
A1: dom f <> {} ;
dom (IncAddr (F,k)) = dom F by Def9;
hence contradiction by A1; :: thesis: verum