let f be Element of SCM+FSA-Data*-Loc ; :: thesis: (SCM*-VAL * SCM+FSA-OK) . f = INT *
A1: SCM+FSA-OK . f = 2 by Lm6;
f in SCM+FSA-Memory ;
then A2: f in dom SCM+FSA-OK by FUNCT_2:def 1;
thus (SCM*-VAL * SCM+FSA-OK) . f = SCM*-VAL . (SCM+FSA-OK . f) by A2, FUNCT_1:13
.= SCM*-VAL . 2 by A1
.= INT * ; :: thesis: verum