(f | U) . u = f . u by FUNCT_1:49;
hence for b₁ being set st b₁ = ((f | U) . u) \+\ (f . u) holds
b₁ is empty ; :: thesis: verum