theorem Th27: :: EC_PF_2:27

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