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