A3: dom (Shift p,k) = { (m + k) where m is Element of NAT : m in dom p } by VALUED_1:def 12;
Shift p,k is NAT -defined

proof

let x be set ; :: according to TARSKI:def 3,RELAT_1:def 18 :: thesis: ( not x in dom (Shift p,k) or x in NAT )
assume x in dom (Shift p,k) ; :: thesis: x in NAT
then ex m being Element of NAT st
( x = m + k & m in dom p ) by A3;
hence x in NAT ; :: thesis: verum

end;

hence for b₁ being FinPartState of S st b₁ = Shift p,k holds
b₁ is NAT -defined ; :: thesis: verum