let n be even Nat; :: thesis: for k being Nat st k > 1 holds
4 divides n |^ k
let k be Nat; :: thesis: ( k > 1 implies 4 divides n |^ k )
assume k > 1 ; :: thesis: 4 divides n |^ k
then 1 + 1 <= k by NAT_1:13;
then A2: n |^ 2 divides n |^ k by NEWTON:89;
4 divides n |^ 2 by NEWTON05:84;
hence 4 divides n |^ k by A2, INT_2:9; :: thesis: verum