let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom ((SCM-Instr .--> SCM+FSA-Instr ) * (SCM-OK | NAT )) or x in NAT )
A1: dom ((SCM-Instr .--> SCM+FSA-Instr ) * (SCM-OK | NAT )) c= dom (SCM-OK | NAT ) by RELAT_1:44;
assume x in dom ((SCM-Instr .--> SCM+FSA-Instr ) * (SCM-OK | NAT )) ; :: thesis: x in NAT
hence x in NAT by A1, RELAT_1:86; :: thesis: verum