[(2 * n),k] in PFArt n,k by Def2;
hence not PFArt n,k is empty ; :: thesis: verum