let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in NAT or x in dom ((SCM-Instr .--> SCM+FSA-Instr) * (SCM-OK | NAT)) )
assume A1: x in NAT ; :: thesis: x in dom ((SCM-Instr .--> SCM+FSA-Instr) * (SCM-OK | NAT))
then x in SCM-Memory ;
then x in dom SCM-OK by FUNCT_2:def 1;
then ( dom (SCM-Instr .--> SCM+FSA-Instr) = {SCM-Instr} & x in dom (SCM-OK | NAT) ) by A1, FUNCOP_1:19, RELAT_1:86;
hence x in dom ((SCM-Instr .--> SCM+FSA-Instr) * (SCM-OK | NAT)) by Lm2, RELAT_1:46; :: thesis: verum