let F be Function; :: thesis: for k being Element of NAT st k > 0 holds
not 0 in dom (Shift F,k)
let k be Element of NAT ; :: thesis: ( k > 0 implies not 0 in dom (Shift F,k) )
assume that
A1: k > 0 and
A2: 0 in dom (Shift F,k) ; :: thesis: contradiction
dom (Shift F,k) = { (m + k) where m is Element of NAT : m in dom F } by Def12;
then ex m being Element of NAT st
( 0 = m + k & m in dom F ) by A2;
hence contradiction by A1; :: thesis: verum