reconsider b = a as Element of SCM-Memory by SCMRING2:def 1;
set k = a .--> r;
set f = the Object-Kind of (SCM R);
A1: dom the Object-Kind of (SCM R) = dom (SCM-OK R) by SCMRING2:def 1
.= SCM-Memory by FUNCT_2:def 1 ;
A2: dom (a .--> r) = {a} by FUNCOP_1:19;
A3: {b} is Subset of SCM-Memory ;
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 A4: x in dom (a .--> r) ; :: thesis: (a .--> r) . x in the Object-Kind of (SCM R) . x
then x = a by A2, TARSKI:def 1;
then A5: (a .--> r) . x = r by FUNCOP_1:87;
the Object-Kind of (SCM R) . x = ObjectKind a by A2, A4, TARSKI:def 1
.= the carrier of R by SCMRING3:1 ;
hence (a .--> r) . x in the Object-Kind of (SCM R) . x by A5; :: thesis: verum

end;

hence a .--> r is FinPartState of (SCM R) by A1, A2, A3, CARD_3:def 9; :: thesis: verum