let a be Element of NAT ; :: thesis: SCM+FSA-OK . a = SCM+FSA-Instr
A1: dom ((SCM-Instr .--> SCM+FSA-Instr ) * (SCM-OK | NAT )) c= dom (SCM-OK | NAT ) by RELAT_1:44;
A2: a in NAT ;
then A3: a in dom ((SCM-Instr .--> SCM+FSA-Instr ) * (SCM-OK | NAT )) by Lm3;
thus SCM+FSA-OK . a = ((SCM-Instr .--> SCM+FSA-Instr ) * (SCM-OK | NAT )) . a by A2, Lm3, FUNCT_4:14
.= (SCM-Instr .--> SCM+FSA-Instr ) . ((SCM-OK | NAT ) . a) by A2, Lm3, FUNCT_1:22
.= (SCM-Instr .--> SCM+FSA-Instr ) . (SCM-OK . a) by A3, A1, FUNCT_1:70
.= (SCM-Instr .--> SCM+FSA-Instr ) . SCM-Instr by AMI_2:11
.= SCM+FSA-Instr by FUNCOP_1:87 ; :: thesis: verum