let 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 NAT -defined FinPartState of holds dom F, dom (Shift F,k) are_equipotent
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 dom F, dom (Shift F,k) are_equipotent
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 dom F, dom (Shift F,k) are_equipotent
let F be NAT -defined FinPartState of ; :: thesis: dom F, dom (Shift F,k) are_equipotent
A1: dom F c= NAT by RELAT_1:def 18;
defpred S₁[ set , set ] means ex il being Element of NAT st
( $1 = il & $2 = il. S,(k + (locnum il,S)) );
A2: for e being set st e in dom F holds
ex u being set st S₁[e,u]

proof

let e be set ; :: thesis: ( e in dom F implies ex u being set st S₁[e,u] )
assume e in dom F ; :: thesis: ex u being set st S₁[e,u]
then reconsider e = e as Element of NAT by A1;
take il. S,(k + (locnum e,S)) ; :: thesis: S₁[e, il. S,(k + (locnum e,S))]
take e ; :: thesis: ( e = e & il. S,(k + (locnum e,S)) = il. S,(k + (locnum e,S)) )
thus ( e = e & il. S,(k + (locnum e,S)) = il. S,(k + (locnum e,S)) ) ; :: thesis: verum

end;

consider f being Function such that
A3: dom f = dom F and
A4: for x being set st x in dom F holds
S₁[x,f . x] from CLASSES1:sch 1(A2);
take f ; :: according to WELLORD2:def 4 :: thesis: ( f is one-to-one & proj1 f = dom F & proj2 f = dom (Shift F,k) )

hereby :: according to FUNCT_1:def 8 :: thesis: ( proj1 f = dom F & proj2 f = dom (Shift F,k) )

let x1, x2 be set ; :: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume that
A5: x1 in dom f and
A6: x2 in dom f and
A7: f . x1 = f . x2 ; :: thesis: x1 = x2
consider i1 being Element of NAT such that
A8: x1 = i1 and
A9: f . x1 = il. S,(k + (locnum i1,S)) by A3, A4, A5;
consider i2 being Element of NAT such that
A10: x2 = i2 and
A11: f . x2 = il. S,(k + (locnum i2,S)) by A3, A4, A6;
k + (locnum i1,S) = k + (locnum i2,S) by A7, A9, A11, AMISTD_1:25;
hence x1 = x2 by A8, A10, AMISTD_1:27; :: thesis: verum

end;

thus dom f = dom F by A3; :: thesis: proj2 f = dom (Shift F,k)
A12: dom (Shift F,k) = { (il. S,(m + k)) where m is Element of NAT : il. S,m in dom F } by Def16;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: dom (Shift F,k) c= proj2 f

let y be set ; :: thesis: ( y in rng f implies y in dom (Shift F,k) )
assume y in rng f ; :: thesis: y in dom (Shift F,k)
then consider x being set such that
A13: x in dom f and
A14: f . x = y by FUNCT_1:def 5;
consider il being Element of NAT such that
A15: x = il and
A16: f . x = il. S,(k + (locnum il,S)) by A3, A4, A13;
consider a being natural number such that
A17: il = il. S,a by AMISTD_1:26;
reconsider a = a as Element of NAT by ORDINAL1:def 13;
a = locnum il,S by A17, AMISTD_1:def 13;
hence y in dom (Shift F,k) by A3, A12, A13, A14, A15, A16, A17; :: thesis: verum

end;

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in dom (Shift F,k) or y in proj2 f )
assume y in dom (Shift F,k) ; :: thesis: y in proj2 f
then consider m being Element of NAT such that
A18: y = il. S,(m + k) and
A19: il. S,m in dom F by A12;
consider il being Element of NAT such that
A20: il. S,m = il and
A21: f . (il. S,m) = il. S,(k + (locnum il,S)) by A4, A19;
m = locnum il,S by A20, AMISTD_1:def 13;
hence y in proj2 f by A3, A18, A19, A21, FUNCT_1:def 5; :: thesis: verum