let f be Function; :: thesis: for i, n being Nat st i in dom (Shift (f,n)) holds
ex j being Nat st
( j in dom f & i = j + n )
let i, n be Nat; :: thesis: ( i in dom (Shift (f,n)) implies ex j being Nat st
( j in dom f & i = j + n ) )
A1: dom (Shift (f,n)) = { (m + n) where m is Nat : m in dom f } by Def12;
assume i in dom (Shift (f,n)) ; :: thesis: ex j being Nat st
( j in dom f & i = j + n )
then ex m being Nat st
( i = m + n & m in dom f ) by A1;
hence ex j being Nat st
( j in dom f & i = j + n ) ; :: thesis: verum