let F be Function; :: thesis: for k being Nat st k > 0 holds
not 0 in dom (Shift (F,k))
let k be 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 Nat : m in dom F } by Def12;
then ex m being Nat st
( 0 = m + k & m in dom F ) by A2;
hence contradiction by A1; :: thesis: verum