let F be NAT -defined total Function; :: thesis: for p being NAT -defined Function
for n being Element of NAT st Shift (p,n) c= F holds
for i being Element of NAT st i in dom p holds
F . (n + i) = p . i
let p be NAT -defined Function; :: thesis: for n being Element of NAT st Shift (p,n) c= F holds
for i being Element of NAT st i in dom p holds
F . (n + i) = p . i
let n be Element of NAT ; :: thesis: ( Shift (p,n) c= F implies for i being Element of NAT st i in dom p holds
F . (n + i) = p . i )
assume A1: Shift (p,n) c= F ; :: thesis: for i being Element of NAT st i in dom p holds
F . (n + i) = p . i
let i be Element of NAT ; :: thesis: ( i in dom p implies F . (n + i) = p . i )
assume A2: i in dom p ; :: thesis: F . (n + i) = p . i
then n + i in dom (Shift (p,n)) by Th24;
hence F . (n + i) = (Shift (p,n)) . (n + i) by A1, GRFUNC_1:2
.= p . i by A2, Def12 ;
:: thesis: verum