a = 1 by TA1;
hence b to_power a = b ; :: thesis: verum