defpred S₁[ object , object ] means ex k being Element of NAT st
( $1 = dl. k & $2 = D . k );
A1: for x, y being object 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 object 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
A3: for x being object holds
( x in dom p iff ( x in the carrier of SCM & ex y being object st S₁[x,y] ) ) and
A4: for x being object st x in dom p holds
S₁[x,p . x] from PARTFUN1:sch 2(A1, A2);
A5: p is the carrier of SCM -defined

proof

let e be object ; :: 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 A3; :: thesis: verum

end;

p is the_Values_of SCM -compatible

proof

let e be object ; :: according to FUNCT_1:def 14 :: thesis: ( not e in proj1 p or p . e in (the_Values_of SCM) . e )
assume A6: e in dom p ; :: thesis: p . e in (the_Values_of SCM) . e
then A7: ex y being object st S₁[e,y] by A3;
reconsider o = e as Object of SCM by A6, A3;
A8: Values o = INT by A7, AMI_3:11;
consider k being Element of NAT such that
A9: ( o = dl. k & p . o = D . k ) by A4, A6;
thus p . e in (the_Values_of SCM) . e by A8, A9, INT_1:def 2; :: thesis: verum

end;

then reconsider p = p as PartState of SCM by A5;
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 A10: dl. k in dom p by A3;
then consider i being Element of NAT such that
A11: ( dl. k = dl. i & p . (dl. k) = D . i ) by A4;
A12: k = i by A11, AMI_3:10;
p c= s by FUNCT_4:25;
hence s . (dl. k) = D . k by A12, A11, A10, GRFUNC_1:2; :: thesis: verum