theorem :: SCMPDS_6:57

for a being Int_position
for k1 being Integer
for I being Program of holds
( (if<>0 (a,k1,I)) . 0 = (a,k1) <>0_goto 2 & (if<>0 (a,k1,I)) . 1 = goto ((card I) + 1) ) by Lm10;