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