let a be non trivial Nat; :: thesis: for s, n being Nat holds (((s ^2) * ((s |^ n) ^2)) - ((((s ^2) - 1) * (Py (a,(n + 1)))) * (s |^ n))) - 1, 0 are_congruent_mod (((2 * a) * s) - (s ^2)) - 1
let s be Nat; :: thesis: for n being Nat holds (((s ^2) * ((s |^ n) ^2)) - ((((s ^2) - 1) * (Py (a,(n + 1)))) * (s |^ n))) - 1, 0 are_congruent_mod (((2 * a) * s) - (s ^2)) - 1
set S = s ^2 ;
defpred S₁[ Nat] means (((s ^2) * ((s |^ $1) ^2)) - ((((s ^2) - 1) * (Py (a,($1 + 1)))) * (s |^ $1))) - 1, 0 are_congruent_mod (((2 * a) * s) - (s ^2)) - 1;
A1: ( Py (a,(0 + 1)) = (Px (a,0)) + ((Py (a,0)) * a) & Py (a,0) = 0 ) by HILB10_1:3, HILB10_1:6;
then A2: Py (a,(0 + 1)) = 1 + (0 * a) by HILB10_1:3;
s |^ 0 = 1 by NEWTON:4;
then A3: (((s ^2) * ((s |^ 0) ^2)) - ((((s ^2) - 1) * (Py (a,(0 + 1)))) * (s |^ 0))) - 1 = (((s ^2) * (1 * 1)) - ((((s ^2) - 1) * 1) * 1)) - 1 by A2, SQUARE_1:def 1
.= 0 ;
A4: for k being Nat st ( for n being Nat st n < k holds
S₁[n] ) holds
S₁[k]

proof

let k be Nat; :: thesis: ( ( for n being Nat st n < k holds
S₁[n] ) implies S₁[k] )
assume A5: for n being Nat st n < k holds
S₁[n] ; :: thesis: S₁[k]
set as2 = (((2 * a) * s) - (s ^2)) - 1;

per cases ( k = 0 or k = 1 or k >= 2 ) by NAT_1:23;

suppose k = 0 ; :: thesis: S₁[k]

hence S₁[k] by A3, INT_1:11; :: thesis: verum

end;

suppose A6: k = 1 ; :: thesis: S₁[k]

A7: Py (a,(0 + 2)) = ((2 * a) * (Py (a,(0 + 1)))) - (Py (a,0)) by HILB10_6:12;
( s |^ 1 = s & s * s = s ^2 ) by SQUARE_1:def 1;
then (((s ^2) * ((s |^ 1) ^2)) - ((((s ^2) - 1) * (Py (a,(1 + 1)))) * (s |^ 1))) - 1 = ((((2 * a) * s) - (s ^2)) - 1) * ((- (s * s)) + 1) by A7, A1, A2;
then (((2 * a) * s) - (s ^2)) - 1 divides ((((s ^2) * ((s |^ 1) ^2)) - ((((s ^2) - 1) * (Py (a,(1 + 1)))) * (s |^ 1))) - 1) - 0 by INT_1:def 3;
hence S₁[k] by A6, INT_1:def 4; :: thesis: verum

end;

suppose k >= 2 ; :: thesis: S₁[k]

then reconsider n = k - 2 as Nat by NAT_1:21;
set Sn = s |^ n;
A8: Py (a,((n + 1) + 2)) = ((2 * a) * (Py (a,((n + 1) + 1)))) - (Py (a,(n + 1))) by HILB10_6:12;
A9: (- ((s ^2) * ((s |^ n) ^2))) + 1,(- ((s ^2) * ((s |^ n) ^2))) + 1 are_congruent_mod (((2 * a) * s) - (s ^2)) - 1 by INT_1:11;
A10: - (s ^2), - (s ^2) are_congruent_mod (((2 * a) * s) - (s ^2)) - 1 by INT_1:11;
A11: (- ((s ^2) * ((s |^ (n + 1)) ^2))) + 1,(- ((s ^2) * ((s |^ (n + 1)) ^2))) + 1 are_congruent_mod (((2 * a) * s) - (s ^2)) - 1 by INT_1:11;
A12: (2 * a) * s,(2 * a) * s are_congruent_mod (((2 * a) * s) - (s ^2)) - 1 by INT_1:11;
A13: (- ((((s |^ n) ^2) * (s ^2)) * (s ^2))) + 1,(- ((((s |^ n) ^2) * (s ^2)) * (s ^2))) + 1 are_congruent_mod (((2 * a) * s) - (s ^2)) - 1 by INT_1:11;
A14: ( s |^ ((n + 1) + 1) = (s |^ (n + 1)) * s & s |^ (n + 1) = (s |^ n) * s & s ^2 = s * s ) by NEWTON:6, SQUARE_1:def 1;
A15: n + 1 < (n + 1) + 1 by NAT_1:13;
then (((s ^2) * ((s |^ (n + 1)) ^2)) - ((((s ^2) - 1) * (Py (a,((n + 1) + 1)))) * (s |^ (n + 1)))) - 1, 0 are_congruent_mod (((2 * a) * s) - (s ^2)) - 1 by A5;
then ((((s ^2) * ((s |^ (n + 1)) ^2)) - ((((s ^2) - 1) * (Py (a,k))) * (s |^ (n + 1)))) - 1) + ((- ((s ^2) * ((s |^ (n + 1)) ^2))) + 1),0 + ((- ((s ^2) * ((s |^ (n + 1)) ^2))) + 1) are_congruent_mod (((2 * a) * s) - (s ^2)) - 1 by A11, INT_1:16;
then A16: (- ((((s ^2) - 1) * (Py (a,k))) * (s |^ (n + 1)))) * ((2 * a) * s),(1 - ((s ^2) * ((s |^ (n + 1)) ^2))) * ((2 * a) * s) are_congruent_mod (((2 * a) * s) - (s ^2)) - 1 by A12, INT_1:18;
n < k by A15, NAT_1:13;
then (((s ^2) * ((s |^ n) ^2)) - ((((s ^2) - 1) * (Py (a,(n + 1)))) * (s |^ n))) - 1, 0 are_congruent_mod (((2 * a) * s) - (s ^2)) - 1 by A5;
then ((((s ^2) * ((s |^ n) ^2)) - ((((s ^2) - 1) * (Py (a,(n + 1)))) * (s |^ n))) - 1) + ((- ((s ^2) * ((s |^ n) ^2))) + 1),0 + ((- ((s ^2) * ((s |^ n) ^2))) + 1) are_congruent_mod (((2 * a) * s) - (s ^2)) - 1 by A9, INT_1:16;
then A17: (- ((((s ^2) - 1) * (Py (a,(n + 1)))) * (s |^ n))) * (- (s ^2)),(1 - ((s ^2) * ((s |^ n) ^2))) * (- (s ^2)) are_congruent_mod (((2 * a) * s) - (s ^2)) - 1 by A10, INT_1:18;
((s ^2) * ((s |^ k) ^2)) - 1,((s ^2) * ((s |^ k) ^2)) - 1 are_congruent_mod (((2 * a) * s) - (s ^2)) - 1 by INT_1:11;
then (((s ^2) * ((s |^ k) ^2)) - 1) + ((((s ^2) - 1) * (Py (a,(n + 1)))) * (s |^ k)),(((s ^2) * ((s |^ k) ^2)) - 1) + ((1 - ((s ^2) * ((s |^ n) ^2))) * (- (s ^2))) are_congruent_mod (((2 * a) * s) - (s ^2)) - 1 by A14, A17, INT_1:16;
then A18: ((((s ^2) * ((s |^ k) ^2)) - 1) + ((((s ^2) - 1) * (Py (a,(n + 1)))) * (s |^ k))) + (- ((((s ^2) - 1) * ((2 * a) * (Py (a,k)))) * (s |^ k))),((((s ^2) * ((s |^ k) ^2)) - 1) + ((1 - ((s ^2) * ((s |^ n) ^2))) * (- (s ^2)))) + ((1 - ((s ^2) * ((s |^ (n + 1)) ^2))) * ((2 * a) * s)) are_congruent_mod (((2 * a) * s) - (s ^2)) - 1 by A16, A14, INT_1:16;
s |^ k = (s |^ n) * (s * s) by A14;
then A19: (s |^ k) ^2 = ((s |^ n) ^2) * ((s * s) ^2) by SQUARE_1:9
.= ((s |^ n) ^2) * ((s ^2) * (s ^2)) by SQUARE_1:9 ;
A20: (s |^ (n + 1)) ^2 = ((s |^ n) ^2) * (s ^2) by A14, SQUARE_1:9;
(((2 * a) * s) - (s ^2)) - 1, 0 are_congruent_mod (((2 * a) * s) - (s ^2)) - 1 by INT_1:12;
then ((- ((((s |^ n) ^2) * (s ^2)) * (s ^2))) + 1) * ((((2 * a) * s) - (s ^2)) - 1),0 * ((- ((((s |^ n) ^2) * (s ^2)) * (s ^2))) + 1) are_congruent_mod (((2 * a) * s) - (s ^2)) - 1 by A13, INT_1:18;
hence S₁[k] by A8, A20, A19, A18, INT_1:15; :: thesis: verum

end;

end;

end;

for n being Nat holds S₁[n] from NAT_1:sch 4(A4);
hence for n being Nat holds (((s ^2) * ((s |^ n) ^2)) - ((((s ^2) - 1) * (Py (a,(n + 1)))) * (s |^ n))) - 1, 0 are_congruent_mod (((2 * a) * s) - (s ^2)) - 1 ; :: thesis: verum