let a, b be Real; :: thesis: (a - b) * (a + b) = (a |^ 2) - (b |^ 2)
(a - b) * (a + b) = (a * a) - (b * b)
.= (a |^ 2) - (b * b) by WSIERP_1:1
.= (a |^ 2) - (b |^ 2) by WSIERP_1:1 ;
hence (a - b) * (a + b) = (a |^ 2) - (b |^ 2) ; :: thesis: verum