let a be Real; :: thesis: a to_power 2 = a ^2

now :: thesis: a to_power 2 = a ^2

per cases ( a > 0 or a = 0 or a < 0 ) ;

suppose A1: a > 0 ; :: thesis: a to_power 2 = a ^2

thus a to_power 2 = a to_power (1 + 1)
.= (a to_power 1) * (a to_power 1) by A1, Th27
.= (a to_power 1) * a
.= a ^2 ; :: thesis: verum

end;

suppose a = 0 ; :: thesis: a to_power 2 = a ^2

hence a to_power 2 = a ^2 by Def2; :: thesis: verum

end;

suppose A2: a < 0 ; :: thesis: a to_power 2 = a ^2

reconsider l = 1 as Integer ;
thus a to_power 2 = a #Z (l + l) by Def2
.= (a #Z l) * (a #Z l) by A2, PREPOWER:44
.= a * (a #Z l) by PREPOWER:35
.= a ^2 by PREPOWER:35 ; :: thesis: verum

end;

end;

end;

hence a to_power 2 = a ^2 ; :: thesis: verum