defpred S_{1}[ 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_{1}[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_{1}[x,y1] & S_{1}[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_{1}[x,y] ) )
and

A4: for x being object st x in dom p holds

S_{1}[x,p . x]
from PARTFUN1:sch 2(A1, A2);

A5: p is the carrier of SCM -defined

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

( $1 = dl. k & $2 = D . k );

A1: for x, y being object st x in the carrier of SCM & S

y in INT by INT_1:def 2;

A2: for x, y1, y2 being object st x in the carrier of SCM & S

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

A4: for x being object st x in dom p holds

S

A5: p is the carrier of SCM -defined

proof

p is the_Values_of SCM -compatible
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;thus ( not e in proj1 p or e in the carrier of SCM ) by A3; :: thesis: verum

proof

then reconsider p = p as PartState of SCM by A5;
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_{1}[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;assume A6: e in dom p ; :: thesis: p . e in (the_Values_of SCM) . e

then A7: ex y being object st S

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

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