theorem Th25: :: EC_PF_2:25

for p being Prime
for g2, a, b being Element of (GF p) st g2 = 2 mod p holds
(a + b) |^ 2 = ((a |^ 2) + ((g2 * a) * b)) + (b |^ 2)