let b be Element of SCM+FSA-Data-Loc ; :: thesis: SCM+FSA-OK . b = INT
b in SCM-Data-Loc ;
then b in SCM-Memory ;
then A2: b in dom SCM-OK by FUNCT_2:def 1;
ex x, y being set st
( x in {1} & y in NAT & b = [x,y] ) by ZFMISC_1:103;
then b is not Element of NAT ;
then not b in dom ((SCM-Instr .--> SCM+FSA-Instr ) * (SCM-OK | NAT )) by Lm1;
hence SCM+FSA-OK . b = ((SCM+FSA-Memory --> (INT * )) +* SCM-OK ) . b by FUNCT_4:12
.= SCM-OK . b by A2, FUNCT_4:14
.= INT by AMI_2:10 ;
:: thesis: verum