set k = a .--> r;

set f = the_Values_of (SCM R);

reconsider b = a as Element of SCM-Memory by SCMRING2:def 1;

for x being object st x in dom (a .--> r) holds

(a .--> r) . x in (the_Values_of (SCM R)) . x

set f = the_Values_of (SCM R);

reconsider b = a as Element of SCM-Memory by SCMRING2:def 1;

for x being object st x in dom (a .--> r) holds

(a .--> r) . x in (the_Values_of (SCM R)) . x

proof

hence
a .--> r is FinPartState of (SCM R)
by FUNCT_1:def 14; :: thesis: verum
let x be object ; :: thesis: ( x in dom (a .--> r) implies (a .--> r) . x in (the_Values_of (SCM R)) . x )

assume A2: x in dom (a .--> r) ; :: thesis: (a .--> r) . x in (the_Values_of (SCM R)) . x

then x = a by TARSKI:def 1;

then A3: (a .--> r) . x = r by FUNCOP_1:72;

a in Data-Locations by SCMRING2:1;

then A4: a in SCM-Data-Loc by AMI_3:27;

(the_Values_of (SCM R)) . x = Values a by A2, TARSKI:def 1

.= (the_Values_of (SCM R)) . a

.= ((SCM-VAL R) * SCM-OK) . a by SCMRING2:24

.= the carrier of R by A4, SCMRING1:3 ;

hence (a .--> r) . x in (the_Values_of (SCM R)) . x by A3; :: thesis: verum

end;assume A2: x in dom (a .--> r) ; :: thesis: (a .--> r) . x in (the_Values_of (SCM R)) . x

then x = a by TARSKI:def 1;

then A3: (a .--> r) . x = r by FUNCOP_1:72;

a in Data-Locations by SCMRING2:1;

then A4: a in SCM-Data-Loc by AMI_3:27;

(the_Values_of (SCM R)) . x = Values a by A2, TARSKI:def 1

.= (the_Values_of (SCM R)) . a

.= ((SCM-VAL R) * SCM-OK) . a by SCMRING2:24

.= the carrier of R by A4, SCMRING1:3 ;

hence (a .--> r) . x in (the_Values_of (SCM R)) . x by A3; :: thesis: verum