let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite standard AMI-Struct of N
for F being NAT -defined FinPartState of holds Shift F,0 = F
let S be non empty stored-program IC-Ins-separated definite standard AMI-Struct of N; :: thesis: for F being NAT -defined FinPartState of holds Shift F,0 = F
let F be NAT -defined FinPartState of ; :: thesis: Shift F,0 = F
A1: dom F c= NAT by RELAT_1:def 18;
A2: dom F = { (il. S,(m + 0 )) where m is Element of NAT : il. S,m in dom F }

proof

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

let a be set ; :: thesis: ( a in dom F implies a in { (il. S,(m + 0 )) where m is Element of NAT : il. S,m in dom F } )
assume A3: a in dom F ; :: thesis: a in { (il. S,(m + 0 )) where m is Element of NAT : il. S,m in dom F }
then reconsider l = a as Element of NAT by A1;
consider k being natural number such that
A4: l = il. S,k by AMISTD_1:26;
reconsider k = k as Element of NAT by ORDINAL1:def 13;
a = il. S,(k + 0 ) by A4;
hence a in { (il. S,(m + 0 )) where m is Element of NAT : il. S,m in dom F } by A3; :: thesis: verum

end;

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

end;

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