let a be non empty real number ; :: 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 FIB_NUM2:4; :: thesis: verum