let m be positive Nat; :: thesis:
let k be Nat; :: thesis:
let S be Sierp49FS of m,k; :: thesis:
let q be CR_Sequence; :: thesis:
assume A1: q = PrimeDivisorsFS m ; :: thesis:
deffunc H₁( Integer) -> Element of INT = In (($1 * ($1 + (2 * k))),INT);
consider f being Function of INT,INT such that
A2: for x being Element of INT holds f . x = H₁(x) from FUNCT_2:sch 4();
set X = PrimeDivisors m;
set x0 = (CRT (S,q)) + (1 * (Product q));
take a = ((CRT (S,q)) + (1 * (Product q))) + (2 * k); :: thesis:
take b = (CRT (S,q)) + (1 * (Product q)); :: thesis:
thus 2 * k = a - b ; :: thesis:
len S = len q by A1, Def14;
then A3: dom S = dom q by FINSEQ_3:29;
(CRT (S,q)) + (1 * (Product q)) in INT by INT_1:def 2;
then A4: f . ((CRT (S,q)) + (1 * (Product q))) = H₁((CRT (S,q)) + (1 * (Product q))) by A2;
A5: for i being Nat st i in dom q holds
f . ((CRT (S,q)) + (1 * (Product q))),f . (S . i) are_congruent_mod q . i

let i be Nat; :: thesis:
assume A6: i in dom q ; :: thesis:
S . i in INT by INT_1:def 2;
then A7: f . (S . i) = H₁(S . i) by A2;
CRT (S,q) solves_CRT S,q by A3, Def4;
then (CRT (S,q)) + (1 * (Product q)) solves_CRT S,q by A3, Th30;
then A8: (CRT (S,q)) + (1 * (Product q)),S . i are_congruent_mod q . i by A3, A6;
then ((CRT (S,q)) + (1 * (Product q))) + (2 * k),(S . i) + (2 * k) are_congruent_mod q . i ;
hence f . ((CRT (S,q)) + (1 * (Product q))),f . (S . i) are_congruent_mod q . i by A4, A7, A8, INT_1:18; :: thesis:

end;

let i be Nat; :: thesis:
S . i in INT by INT_1:def 2;
then f . (S . i) = H₁(S . i) by A2;
hence ( i in dom q implies not f . (S . i), 0 are_congruent_mod q . i ) by A1, A3, Def14; :: thesis:

end;

for i being Nat st i in dom q holds
f . ((CRT (S,q)) + (1 * (Product q))),q . i are_coprime

end;

then f . ((CRT (S,q)) + (1 * (Product q))),m * 1 are_coprime by A1, A4, Th53;
hence ( a,m are_coprime & b,m are_coprime & a = ((CRT (S,q)) + (Product q)) + (2 * k) & b = (CRT (S,q)) + (Product q) ) by A4, NEWTON01:41; :: thesis: