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