defpred S₁[ set , set ] means ex k being Element of NAT st
( $1 = dl. k & $2 = D . k );
A1: for x, y being set st x in the carrier of SCM & S₁[x,y] holds
y in INT by INT_1:def 2;
A2: for x, y1, y2 being set st x in the carrier of SCM & S₁[x,y1] & S₁[x,y2] holds
y1 = y2 by AMI_3:10;
consider p being PartFunc of SCM,INT such that
A9: 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
A10: for x being set st x in dom p holds
S₁[x,p . x] from PARTFUN1:sch 2(A1, A2);
A11: 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 A9; :: thesis: verum

end;

p is the_Values_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_Values_of SCM) . e )
assume A12: e in dom p ; :: thesis: p . e in (the_Values_of SCM) . e
then A13: ex y being set st S₁[e,y] by A9;
reconsider o = e as Object of SCM by A12, A9;
A14: Values o = INT by A13, AMI_3:11;
consider k being Element of NAT such that
A15: ( o = dl. k & p . o = D . k ) by A10, A12;
thus p . e in (the_Values_of SCM) . e by A14, A15, INT_1:def 2; :: thesis: verum

end;

then reconsider p = p as PartState of SCM by A11;
take s = the State of SCM +* p; :: thesis: for k being Element of NAT st k < len D holds
s . (dl. k) = D . k
let k be Element of NAT ; :: thesis: ( k < len D implies s . (dl. k) = D . k )
assume k < len D ; :: thesis: s . (dl. k) = D . k
ex i being Element of NAT st
( dl. k = dl. i & D . k = D . i ) ;
then A16: dl. k in dom p by A9;
then consider i being Element of NAT such that
A17: ( dl. k = dl. i & p . (dl. k) = D . i ) by A10;
A18: k = i by A17, AMI_3:10;
p c= s by FUNCT_4:25;
hence s . (dl. k) = D . k by A18, A17, A16, GRFUNC_1:2; :: thesis: verum