let I be Program of SCM+FSA ; :: thesis: for n being Element of NAT holds dom I misses dom (Start-At n,SCM+FSA )
let n be Element of NAT ; :: thesis: dom I misses dom (Start-At n,SCM+FSA )
A1: dom (Start-At n,SCM+FSA ) = {(IC SCM+FSA )} by FUNCOP_1:19;
assume (dom I) /\ (dom (Start-At n,SCM+FSA )) <> {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction
then consider x being set such that
A2: x in (dom I) /\ (dom (Start-At n,SCM+FSA )) by XBOOLE_0:def 1;
( x in dom I & x in dom (Start-At n,SCM+FSA ) ) by A2, XBOOLE_0:def 4;
then ( dom I c= NAT & IC SCM+FSA in dom I ) by A1, RELAT_1:def 18, TARSKI:def 1;
then reconsider l = IC SCM+FSA as Element of NAT ;
l = IC SCM+FSA ;
hence contradiction by AMI_1:48; :: thesis: verum