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 )) )
A1: dom (SCM-Instr .--> SCM+FSA-Instr ) = {SCM-Instr } by FUNCOP_1:19;
assume A2: 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 x in dom (SCM-OK | NAT ) by A2, RELAT_1:86;
hence x in dom ((SCM-Instr .--> SCM+FSA-Instr ) * (SCM-OK | NAT )) by A1, Lm2, RELAT_1:46; :: thesis: verum