let N be non empty with_non-empty_elements set ; :: thesis: for n being Element of NAT
for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for I being Program of S holds dom I misses dom (Start-At (n,S))
let n be Element of NAT ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for I being Program of S holds dom I misses dom (Start-At (n,S))
let S be non empty stored-program IC-Ins-separated definite realistic COM-Struct of N; :: thesis: for I being Program of S holds dom I misses dom (Start-At (n,S))
let I be Program of S; :: thesis: dom I misses dom (Start-At (n,S))
A1: dom (Start-At (n,S)) = {(IC S)} by FUNCOP_1:19;
assume (dom I) /\ (dom (Start-At (n,S))) <> {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction
then consider x being set such that
A2: x in (dom I) /\ (dom (Start-At (n,S))) by XBOOLE_0:def 1;
( x in dom I & x in dom (Start-At (n,S)) ) by A2, XBOOLE_0:def 4;
then ( dom I c= NAT & IC S in dom I ) by A1, TARSKI:def 1;
then reconsider l = IC S as Element of NAT ;
l = IC S ;
hence contradiction by Th3; :: thesis: verum