let IL be non empty set ; :: thesis: for N being with_non-empty_elements set
for S being non empty IC-Ins-separated AMI-Struct of IL,N
for p being FinPartState of S
for l being Instruction-Location of S st l in dom p holds
l in dom (ProgramPart p)
let N be with_non-empty_elements set ; :: thesis: for S being non empty IC-Ins-separated AMI-Struct of IL,N
for p being FinPartState of S
for l being Instruction-Location of S st l in dom p holds
l in dom (ProgramPart p)
let S be non empty IC-Ins-separated AMI-Struct of IL,N; :: thesis: for p being FinPartState of S
for l being Instruction-Location of S st l in dom p holds
l in dom (ProgramPart p)
let p be FinPartState of S; :: thesis: for l being Instruction-Location of S st l in dom p holds
l in dom (ProgramPart p)
let l be Instruction-Location of S; :: thesis: ( l in dom p implies l in dom (ProgramPart p) )
assume A1: l in dom p ; :: thesis: l in dom (ProgramPart p)
dom (ProgramPart p) = (dom p) /\ IL by RELAT_1:90;
hence l in dom (ProgramPart p) by A1, XBOOLE_0:def 4; :: thesis: verum