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

proof

set A = (a ^2) -' 1;
set B = (b ^2) -' 1;
( (a ^2) -' 1 = (a ^2) - 1 & (b ^2) -' 1 = (b ^2) - 1 ) by NAT_1:14, XREAL_1:233;
then ((a ^2) -' 1) - ((b ^2) -' 1) = (a - b) * (a + b) ;
then A3: (a ^2) -' 1,(b ^2) -' 1 are_congruent_mod a - b by INT_1:def 5;
a - b = 1 * (a - b) ;
then A4: a,b are_congruent_mod a - b by INT_1:def 5;
let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A5: S₁[n] ; :: thesis: S₁[n + 1]
A6: ( Px (a,(n + 1)) = ((Px (a,n)) * a) + ((Py (a,n)) * ((a ^2) -' 1)) & Px (b,(n + 1)) = ((Px (b,n)) * b) + ((Py (b,n)) * ((b ^2) -' 1)) ) by Th9;
A7: (Py (a,n)) * ((a ^2) -' 1),(Py (b,n)) * ((b ^2) -' 1) are_congruent_mod a - b by A5, A3, INT_1:18;
(Px (a,n)) * a,(Px (b,n)) * b are_congruent_mod a - b by A5, A4, INT_1:18;
hence Px (a,(n + 1)), Px (b,(n + 1)) are_congruent_mod a - b by A6, A7, INT_1:16; :: thesis: Py (a,(n + 1)), Py (b,(n + 1)) are_congruent_mod a - b
A8: ( Py (a,(n + 1)) = (Px (a,n)) + ((Py (a,n)) * a) & Py (b,(n + 1)) = (Px (b,n)) + ((Py (b,n)) * b) ) by Th9;
(Py (a,n)) * a,(Py (b,n)) * b are_congruent_mod a - b by A4, A5, INT_1:18;
hence Py (a,(n + 1)), Py (b,(n + 1)) are_congruent_mod a - b by A8, A5, INT_1:16; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A2);
hence ( Px (a,n), Px (b,n) are_congruent_mod a - b & Py (a,n), Py (b,n) are_congruent_mod a - b ) ; :: thesis: verum