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