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 SCMFSA_2:84; :: thesis: not IC SCM+FSA in dom I
thus not IC SCM+FSA in dom I by A1, COMPOS_1:3; :: thesis: verum