let n be Nat; :: thesis: 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)) )
let a be non trivial Nat; :: thesis: ( 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)) )
set n1 = n + 1;
set d = (a ^2) -' 1;
( a * a >= 0 + 1 & a * a = a ^2 ) by INT_1:7, SQUARE_1:def 1;
then A1: (a ^2) -' 1 = (a * a) - 1 by XREAL_1:233;
A2: ( 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) ) by HILB10_1:6;
A3: ( Px (a,((n + 1) + 1)) = ((Px (a,(n + 1))) * a) + ((Py (a,(n + 1))) * ((a ^2) -' 1)) & Py (a,((n + 1) + 1)) = (Px (a,(n + 1))) + ((Py (a,(n + 1))) * a) ) by HILB10_1:6;
A4: (a * (Px (a,(n + 1)))) - (((a ^2) -' 1) * (Py (a,(n + 1)))) = Px (a,n) by A1, A2;
(a * (Py (a,(n + 1)))) - (Px (a,(n + 1))) = Py (a,n) by A1, A2;
hence ( 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)) ) by A4, A3; :: thesis: verum