let S be COM-Struct ; :: thesis: for x being set
for i being Instruction of S holds
( x in dom (Load i) iff x = 0 )
let x be set ; :: thesis: for i being Instruction of S holds
( x in dom (Load i) iff x = 0 )
let i be Instruction of S; :: thesis: ( x in dom (Load i) iff x = 0 )
dom (Load i) = {0} by FUNCOP_1:13;
hence ( x in dom (Load i) iff x = 0 ) by TARSKI:def 1; :: thesis: verum