let a be Int_position ; :: thesis: for k1 being Integer
for I being Program of SCMPDS holds inspos 0 in dom (if>0 a,k1,I)
let k1 be Integer; :: thesis: for I being Program of SCMPDS holds inspos 0 in dom (if>0 a,k1,I)
let I be Program of SCMPDS ; :: thesis: inspos 0 in dom (if>0 a,k1,I)
set ci = card (if>0 a,k1,I);
card (if>0 a,k1,I) = (card I) + 1 by Th15;
hence inspos 0 in dom (if>0 a,k1,I) by SCMPDS_4:1; :: thesis: verum