theorem Th7: :: FIB_NUM3:7

for a, b being Real holds (a + b) * (a - b) = (a to_power 2) - (b to_power 2)