let S be COM-Struct ; :: thesis: for i being Instruction of S holds 0 in dom (Load i)
let i be Instruction of S; :: thesis: 0 in dom (Load i)
thus 0 in dom (Load i) by TARSKI:def 1; :: thesis: verum