(1 * (a1 |^ 0)) - (1 * (b1 |^ 0)) = 0 ;
hence (a1 |^ 0) - (b1 |^ 0) = 0 ; :: thesis: verum