let F be NAT -defined Function; :: thesis: Shift (F,0) = F
A1: dom F c= NAT by RELAT_1:def 18;
A2: dom F = { (m + 0) where m is Element of NAT : m in dom F }

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: { (m + 0) where m is Element of NAT : m in dom F } c= dom F

let a be set ; :: thesis: ( a in dom F implies a in { (m + 0) where m is Element of NAT : m in dom F } )
assume A3: a in dom F ; :: thesis: a in { (m + 0) where m is Element of NAT : m in dom F }
then reconsider l = a as Element of NAT by A1;
a = l + 0 ;
hence a in { (m + 0) where m is Element of NAT : m in dom F } by A3; :: thesis: verum

end;

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { (m + 0) where m is Element of NAT : m in dom F } or a in dom F )
assume a in { (m + 0) where m is Element of NAT : m in dom F } ; :: thesis: a in dom F
then ex m being Element of NAT st
( a = m + 0 & m in dom F ) ;
hence a in dom F ; :: thesis: verum

end;

for m being Element of NAT st m in dom F holds
F . (m + 0) = F . m ;
hence Shift (F,0) = F by A2, Def12; :: thesis: verum