theorem Th25: :: HILB10_6:25

for n being Nat
for a being non trivial Nat holds Py (a,(2 * n)) = (2 * (Py (a,n))) * (Px (a,n))