set XX = X addw (D,num);
set f = (D,num) addw X;
set Y = rng ((D,num) addw X);
reconsider ff = (D,num) addw X as sequence of (rng ((D,num) addw X)) by FUNCT_2:6;
ff . 0 = X by Def71;
then X c= X addw (D,num) by ZFMISC_1:74;
hence for b₁ being set st b₁ = X \ (X addw (D,num)) holds
b₁ is empty ; :: thesis: verum