let m, k be natural number ; :: thesis: for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard AMI-Struct of N
for F being FinPartState of S holds Shift (Shift F,m),k = Shift F,(m + k)
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 FinPartState of S holds Shift (Shift F,m),k = Shift F,(m + k)
let S be non empty stored-program IC-Ins-separated definite standard AMI-Struct of N; :: thesis: for F being FinPartState of S holds Shift (Shift F,m),k = Shift F,(m + k)
let F be FinPartState of S; :: thesis: Shift (Shift F,m),k = Shift F,(m + k)
set A = { (il. S,(l + m)) where l is Element of NAT : il. S,l in dom F } ;
A1: dom (Shift F,m) = { (il. S,(l + m)) where l is Element of NAT : il. S,l in dom F } by Def16;
{ (il. S,(r + k)) where r is Element of NAT : il. S,r in { (il. S,(l + m)) where l is Element of NAT : il. S,l in dom F } } = { (il. S,(q + (m + k))) where q is Element of NAT : il. S,q in dom F }

proof

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

let x be set ; :: thesis: ( x in { (il. S,(r + k)) where r is Element of NAT : il. S,r in { (il. S,(l + m)) where l is Element of NAT : il. S,l in dom F } } implies x in { (il. S,(q + (m + k))) where q is Element of NAT : il. S,q in dom F } )
assume x in { (il. S,(r + k)) where r is Element of NAT : il. S,r in { (il. S,(l + m)) where l is Element of NAT : il. S,l in dom F } } ; :: thesis: x in { (il. S,(q + (m + k))) where q is Element of NAT : il. S,q in dom F }
then consider r being Element of NAT such that
A2: x = il. S,(r + k) and
A3: il. S,r in { (il. S,(l + m)) where l is Element of NAT : il. S,l in dom F } ;
consider l being Element of NAT such that
A4: il. S,r = il. S,(l + m) and
A5: il. S,l in dom F by A3;
r = l + m by A4, AMISTD_1:25;
then x = il. S,(l + (m + k)) by A2;
hence x in { (il. S,(q + (m + k))) where q is Element of NAT : il. S,q in dom F } by A5; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { (il. S,(q + (m + k))) where q is Element of NAT : il. S,q in dom F } or x in { (il. S,(r + k)) where r is Element of NAT : il. S,r in { (il. S,(l + m)) where l is Element of NAT : il. S,l in dom F } } )
assume x in { (il. S,(q + (m + k))) where q is Element of NAT : il. S,q in dom F } ; :: thesis: x in { (il. S,(r + k)) where r is Element of NAT : il. S,r in { (il. S,(l + m)) where l is Element of NAT : il. S,l in dom F } }
then consider q being Element of NAT such that
A6: x = il. S,(q + (m + k)) and
A7: il. S,q in dom F ;
A8: x = il. S,((q + m) + k) by A6;
il. S,(q + m) in { (il. S,(l + m)) where l is Element of NAT : il. S,l in dom F } by A7;
hence x in { (il. S,(r + k)) where r is Element of NAT : il. S,r in { (il. S,(l + m)) where l is Element of NAT : il. S,l in dom F } } by A8; :: thesis: verum

end;

then A9: dom (Shift (Shift F,m),k) = { (il. S,(l + (m + k))) where l is Element of NAT : il. S,l in dom F } by A1, Def16;

now

let l be Element of NAT ; :: thesis: ( il. S,l in dom F implies (Shift (Shift F,m),k) . (il. S,(l + (m + k))) = F . (il. S,l) )
assume A10: il. S,l in dom F ; :: thesis: (Shift (Shift F,m),k) . (il. S,(l + (m + k))) = F . (il. S,l)
then A11: il. S,(l + m) in dom (Shift F,m) by A1;
thus (Shift (Shift F,m),k) . (il. S,(l + (m + k))) = (Shift (Shift F,m),k) . (il. S,((l + m) + k))
.= (Shift F,m) . (il. S,(l + m)) by A11, Def16
.= F . (il. S,l) by A10, Def16 ; :: thesis: verum

end;

hence Shift (Shift F,m),k = Shift F,(m + k) by A9, Def16; :: thesis: verum