theorem Th9: :: HILB10_1:6

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