defpred S₁[ set , set ] means ex k being Element of NAT st
( $1 = dl. (ds + k) & $2 = D . (k + 1) );
X: for x, y being set st x in the carrier of SCM & S₁[x,y] holds
y in INT by INT_1:def 2;
Y: for x, y1, y2 being set st x in the carrier of SCM & S₁[x,y1] & S₁[x,y2] holds
y1 = y2

proof

let x, y1, y2 be set ; :: thesis: ( x in the carrier of SCM & S₁[x,y1] & S₁[x,y2] implies y1 = y2 )
assume that
x in the carrier of SCM and
W2: S₁[x,y1] and
W3: S₁[x,y2] ; :: thesis: y1 = y2
consider k1 being Element of NAT such that
W4: x = dl. (ds + k1) and
W5: y1 = D . (k1 + 1) by W2;
consider k2 being Element of NAT such that
W6: x = dl. (ds + k2) and
W7: y2 = D . (k2 + 1) by W3;
ds + k1 = ds + k2 by W4, W6, AMI_3:10;
hence y1 = y2 by W7, W5; :: thesis: verum

end;

consider p being PartFunc of SCM,INT such that
W0: for x being set holds
( x in dom p iff ( x in the carrier of SCM & ex y being set st S₁[x,y] ) ) and
W1: for x being set st x in dom p holds
S₁[x,p . x] from PARTFUN1:sch 2(X, Y);
C: p is the carrier of SCM -defined

proof

let e be set ; :: according to TARSKI:def 3,RELAT_1:def 18 :: thesis: ( not e in proj1 p or e in the carrier of SCM )
thus ( not e in proj1 p or e in the carrier of SCM ) by W0; :: thesis: verum

end;

p is the Object-Kind of SCM -compatible

proof

let e be set ; :: according to FUNCT_1:def 14 :: thesis: ( not e in proj1 p or p . e in the Object-Kind of SCM . e )
assume Z: e in dom p ; :: thesis: p . e in the Object-Kind of SCM . e
then AA: ex y being set st S₁[e,y] by W0;
reconsider o = e as Object of SCM by Z, W0;
B: ObjectKind o = INT by AA, AMI_3:11;
consider k being Element of NAT such that
W3: ( o = dl. (ds + k) & p . o = D . (k + 1) ) by W1, Z;
thus p . e in the Object-Kind of SCM . e by B, W3, INT_1:def 2; :: thesis: verum

end;

then reconsider p = p as PartState of SCM by C;
take s = the State of SCM +* p; :: thesis: for k being Element of NAT st k < len D holds
s . (dl. (ds + k)) = D . (k + 1)
let k be Element of NAT ; :: thesis: ( k < len D implies s . (dl. (ds + k)) = D . (k + 1) )
assume k < len D ; :: thesis: s . (dl. (ds + k)) = D . (k + 1)
ex i being Element of NAT st
( dl. (ds + k) = dl. (ds + i) & D . (k + 1) = D . (i + 1) ) ;
then X: dl. (ds + k) in dom p by W0;
then consider i being Element of NAT such that
W2: ( dl. (ds + k) = dl. (ds + i) & p . (dl. (ds + k)) = D . (i + 1) ) by W1;
A: ds + k = ds + i by W2, AMI_3:10;
p c= s by FUNCT_4:25;
hence s . (dl. (ds + k)) = D . (k + 1) by A, W2, X, GRFUNC_1:2; :: thesis: verum