set q = PrimeDivisorsFS m;
A1: dom (PrimeDivisorsFS m) = Seg (len (PrimeDivisorsFS m)) by FINSEQ_1:def 3;
defpred S₁[ object , Integer] means not (PrimeDivisorsFS m) . $1 divides $2 * ($2 + (2 * k));
A2: for z being Nat st z in Seg (len (PrimeDivisorsFS m)) holds
ex x being Element of INT st S₁[z,x]

proof

let z be Nat; :: thesis: ( z in Seg (len (PrimeDivisorsFS m)) implies ex x being Element of INT st S₁[z,x] )
assume A3: z in Seg (len (PrimeDivisorsFS m)) ; :: thesis: ex x being Element of INT st S₁[z,x]
for i being Nat st i in dom (PrimeDivisorsFS m) holds
ex x being Integer st not (PrimeDivisorsFS m) . i divides x * (x + (2 * k))

proof

let i be Nat; :: thesis: ( i in dom (PrimeDivisorsFS m) implies ex x being Integer st not (PrimeDivisorsFS m) . i divides x * (x + (2 * k)) )
assume that
A4: i in dom (PrimeDivisorsFS m) and
A5: for x being Integer holds (PrimeDivisorsFS m) . i divides x * (x + (2 * k)) ; :: thesis: contradiction
A6: (PrimeDivisorsFS m) . i is prime by A4, Th47;
A7: ( (PrimeDivisorsFS m) . i divides 1 * (1 + (2 * k)) & (PrimeDivisorsFS m) . i divides (- 1) * ((- 1) + (2 * k)) ) by A5;
then (PrimeDivisorsFS m) . i divides ((2 * k) + 1) + (- ((2 * k) - 1)) by WSIERP_1:4;
then (PrimeDivisorsFS m) . i divides 2 * k by INT_2:2;
then (PrimeDivisorsFS m) . i divides (2 * k) + (- ((2 * k) - 1)) by A7, WSIERP_1:4;
hence contradiction by A6, INT_2:27; :: thesis: verum

end;

then consider x being Integer such that
A8: not (PrimeDivisorsFS m) . z divides x * (x + (2 * k)) by A1, A3;
reconsider x = x as Element of INT by INT_1:def 2;
take x ; :: thesis: S₁[z,x]
thus S₁[z,x] by A8; :: thesis: verum

end;

consider p being FinSequence of INT such that
A9: ( dom p = Seg (len (PrimeDivisorsFS m)) & ( for k being Nat st k in Seg (len (PrimeDivisorsFS m)) holds
S₁[k,p . k] ) ) from FINSEQ_1:sch 5(A2);
take p ; :: thesis: ( len p = len (PrimeDivisorsFS m) & ( for i being object st i in dom p holds
not (PrimeDivisorsFS m) . i divides (p . i) * ((p . i) + (2 * k)) ) )
thus ( len p = len (PrimeDivisorsFS m) & ( for i being object st i in dom p holds
not (PrimeDivisorsFS m) . i divides (p . i) * ((p . i) + (2 * k)) ) ) by A9, FINSEQ_1:def 3; :: thesis: verum