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