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