let a, b be real number ; :: thesis: (a + b) * (a - b) = (a to_power 2) - (b to_power 2)
(a + b) * (a - b) = (a ^2) - (b ^2)
.= (a to_power 2) - (b ^2) by POWER:53
.= (a to_power 2) - (b to_power 2) by POWER:53 ;
hence (a + b) * (a - b) = (a to_power 2) - (b to_power 2) ; :: thesis: verum