defpred S1[ 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 & S1[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 & S1[x,y1] & S1[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 S1[x,y] ) ) and
A4: for x being object st x in dom p holds
S1[x,p . x] from 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 . e )
assume A6: e in dom p ; :: thesis: p . e in . e
then A7: ex y being object st S1[e,y] by A3;
reconsider o = e as Object of SCM by A6, A3;
A8: Values o = INT by ;
consider k being Element of NAT such that
A9: ( o = dl. k & p . o = D . k ) by A4, A6;
thus p . e in . e by ; :: 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 ;
p c= s by FUNCT_4:25;
hence s . (dl. k) = D . k by ; :: thesis: verum