let a, b be Real; :: 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:46
.= (a to_power 2) - (b to_power 2) by POWER:46 ;
hence (a + b) * (a - b) = (a to_power 2) - (b to_power 2) ; :: thesis: verum