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
proof
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;
hence a .--> r is FinPartState of (SCM R) by FUNCT_1:def 14; :: thesis: verum