for f, k being positive Nat holds
( f = k ! iff ex j, h, w being Nat ex n, p, q, z being positive Nat st
( q = ((w * z) + h) + j & z = (f * (h + j)) + h & ((((2 * k) |^ 3) * ((2 * k) + 2)) * ((n + 1) |^ 2)) + 1 is square & p = (n + 1) |^ k & q = (p + 1) |^ n & z = p |^ (k + 1) ) )