let k be positive Nat; for t being Nat holds k divides card (NatDivisors ((Sierp53Seq k) . t))
let t be Nat; k divides card (NatDivisors ((Sierp53Seq k) . t))
A2:
(ArProg ((2 |^ (k -' 1)),(2 |^ k))) . t = (2 |^ (k -' 1)) + ((2 |^ k) * t)
by NUMBER06:7;
A1:
k >= 0 + 1
by NAT_1:13;
reconsider n = ((2 |^ k) * t) + (2 |^ (k -' 1)) as non zero Nat ;
k divides card (NatDivisors n)
by A1, PreProb53;
hence
k divides card (NatDivisors ((Sierp53Seq k) . t))
by A2; verum