let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for I being Program of S holds 0 in dom (I +* (Start-At (0,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 0 in dom (I +* (Start-At (0,S)))
let I be Program of S; :: thesis: 0 in dom (I +* (Start-At (0,S)))
A2: 0 in dom I by AFINSQ_1:69;
dom (I +* (Start-At (0,S))) = (dom I) \/ (dom (Start-At (0,S))) by FUNCT_4:def 1;
hence 0 in dom (I +* (Start-At (0,S))) by A2, XBOOLE_0:def 3; :: thesis: verum