a |-count ((a |^ b) * 1) = b + (a |-count 1) by NEWTON03:105;
hence a |-count (a |^ b) = b ; :: thesis: verum