theorem P5: :: REALALG2:15

for F being Field st Char F <> 2 holds
for a being Element of F holds (((a + (1. F)) / (2 '*' (1. F))) ^2) - (((a - (1. F)) / (2 '*' (1. F))) ^2) = a