set k = a .--> r;
set f = the Object-Kind of (SCM R);
reconsider b = a as Element of SCM-Memory by SCMRING2:def 1;
A1: dom (a .--> r) = {a} by FUNCOP_1:13;
for x being set st x in dom (a .--> r) holds
(a .--> r) . x in the Object-Kind of (SCM R) . x

proof

let x be set ; :: thesis: ( x in dom (a .--> r) implies (a .--> r) . x in the Object-Kind of (SCM R) . x )
assume A2: x in dom (a .--> r) ; :: thesis: (a .--> r) . x in the Object-Kind of (SCM R) . x
then x = a by A1, TARSKI:def 1;
then A3: (a .--> r) . x = r by FUNCOP_1:72;
the Object-Kind of (SCM R) . x = ObjectKind a by A1, A2, TARSKI:def 1
.= the carrier of R by SCMRING3:1 ;
hence (a .--> r) . x in the Object-Kind of (SCM R) . x by A3; :: thesis: verum

end;

hence a .--> r is FinPartState of (SCM R) by FUNCT_1:def 14; :: thesis: verum