let n be Nat; :: thesis: for a being non trivial Nat holds Px (a,n), Py (a,n) are_coprime
let a be non trivial Nat; :: thesis: Px (a,n), Py (a,n) are_coprime
defpred S₁[ Nat] means (Px (a,$1)) gcd (Py (a,$1)) = 1;
( Px (a,0) = 1 & Py (a,0) = 0 ) by Th6;
then A1: S₁[ 0 ] ;
A2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

set A = (a ^2) -' 1;
A3: (a ^2) -' 1 = (a ^2) - 1 by NAT_1:14, XREAL_1:233;
let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A4: S₁[n] ; :: thesis: S₁[n + 1]
A5: ( 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 Th9;
thus 1 = ((Px (a,n)) + ((Py (a,n)) * a)) gcd (Py (a,n)) by A4, EULER_1:8
.= (Py (a,(n + 1))) gcd (- (Py (a,n))) by A5, NEWTON02:1
.= ((- (Py (a,n))) + (a * (Py (a,(n + 1))))) gcd (Py (a,(n + 1))) by NEWTON02:5
.= (Px (a,(n + 1))) gcd (Py (a,(n + 1))) by A3, A5 ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A2);
then (Px (a,n)) gcd (Py (a,n)) = 1 ;
hence Px (a,n), Py (a,n) are_coprime by INT_2:def 3; :: thesis: verum