let a be Real; :: thesis: a to_power 2 = (- a) to_power 2
2 = 1 * 2 ;
then 2 is even by ABIAN:def 2;
hence a to_power 2 = (- a) to_power 2 by POWER:47; :: thesis: verum