let I be Program of SCM+FSA ; :: thesis: ( not intloc 0 in dom I & not IC SCM+FSA in dom I )
A1: dom I c= NAT by RELAT_1:def 18;
hence not intloc 0 in dom I by Lm1; :: thesis: not IC SCM+FSA in dom I
thus not IC SCM+FSA in dom I by A1, Lm2; :: thesis: verum