theorem Th12: :: HILB10_6:12

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