A1: dom F = { (m + 0) where m is Nat : m in dom F }
proof
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: { (m + 0) where m is Nat : m in dom F } c= dom F
let a be object ; :: thesis: ( a in dom F implies a in { (m + 0) where m is Nat : m in dom F } )
assume A2: a in dom F ; :: thesis: a in { (m + 0) where m is Nat : m in dom F }
then reconsider l = a as Element of NAT ;
a = l + 0 ;
hence a in { (m + 0) where m is Nat : m in dom F } by A2; :: thesis: verum
end;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { (m + 0) where m is Nat : m in dom F } or a in dom F )
assume a in { (m + 0) where m is Nat : m in dom F } ; :: thesis: a in dom F
then ex m being Nat st
( a = m + 0 & m in dom F ) ;
hence a in dom F ; :: thesis: verum
end;
for m being Nat st m in dom F holds
F . (m + 0) = F . m ;
hence Shift (F,0) = F by A1, Def12; :: thesis: verum