1 * (2 |^ (2 |-count a)) = 1 ;
hence a / (2 |^ (2 |-count a)) = a ; :: thesis: verum