let a be real number ; :: thesis: a to_power 2 = a ^2

A1: now

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

suppose A2: 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 A2, Th32
.= (a to_power 1) * a by Th30
.= a ^2 by Th30 ; :: thesis: verum

end;

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

thus a to_power 2 = a ^2 by A3, Def2; :: thesis: verum

end;

suppose A4: 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 A4, PREPOWER:54
.= a * (a #Z l) by PREPOWER:45
.= a ^2 by PREPOWER:45 ; :: thesis: verum

end;

end;

end;

thus a to_power 2 = a ^2 by A1; :: thesis: verum